Peter Dybjer (Göteborg)

History and meaning of the identity type.

Content:
Lawvere's equality in hyperdoctrines. Howard's treatment of identity.
Martin-Löf's identity in his theory of iterated inductive definitions. The
different identity types in versions of type theory. The meaning
explanations for the identity type. Identity type vs identity judgement.
My own experience of proving coherence of monoidal categories using type
theory as a metalanguage. My own view of identity in type theory
justifying extensional identity types.