|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-level 1-type/h-prop|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
the homotopy fiber
We say is an equivalence if is an inhabited type.
Three variations of this definition are, informally:
is an equivalence if there is a map and homotopies and (a homotopy equivalence)
is an equivalence if there are maps and homotopies and (sometimes called a homotopy isomorphism).
By formalizing these, we obtain types , , and . All four of these types are co-inhabited: we have a function from any one of them to any of the others. Moreover, at least if we assume function extensionality, the types and are themselves equivalent to , and all three are h-propositions.
This is not true for , which is not in general an h-prop even with function extensionality. However, often the most convenient way to show that is an equivalence is by exhibiting a term in (although such a term could just as well be interpreted to lie in with ).
We discuss the categorical semantics of equivalences in homotopy type theory.
Let be a locally cartesian closed category which is a model category, in which the (acyclic cofibration, fibration) weak factorization system has stable path objects, and acyclic cofibrations are preserved by pullback along fibrations between fibrant objects. (We ignore questions of coherence, which are not important for this discussion.) For instance could be a type-theoretic model category.
precisely when in this factorization, the fibration is an acyclic fibration. (See for instance (Shulman, page 49) for more details.)
But by the 2-out-of-3 property, this is equivalent to being a weak equivalence — and hence a homotopy equivalence, since it is a map between fibrant-cofibrant objects.
In the above we fixed one function . But the type is actually a dependent type
is the composite left vertical morphism in
An introduction to equivalence in homotopy type theory is in
Coq code for homotopy equivalences is at