# Contents

## Idea

Just as there are two notions of judgmental equality in dependent type theory, judgmental equality of terms and judgmental equality of types, there are two types in dependent type theory which could be considered typal equality:

In type universes $U$, this means that small types $A:U$ have two notions of typal equality, one from the identity type between small types, and the other from the equivalence type between small types, and the univalence axiom states that these two types are equivalent (i.e. typally equal) to each other.

## Parallels between judgmental equality and typal equality

The parallels between the structural rules for judgmental equality and typal equality are shown below:

judgmental equalitytypal equality
judgmental equality of termsidentification
reflexivity of judgmental equality of termsidentity identification
symmetry of judgmental equality of termsinverse identification
transitivity of judgmental equality of termscomposition of identifications
judgmental equality of typesequivalence
reflexivity of judgmental equality of typesidentity equivalence
symmetry of judgmental equality of typesinverse equivalence
transitivity of judgmental equality of typescomposition of equivalences
principle of substitutiontransport
variable conversion rulesubstitution of evaluation of inverse equivalence

## Homogeneous and heterogeneous typal equality

homogeneous identificationheterogeneous identificationhomogeneous equivalenceheterogeneous equivalence
type$a =_A b$$x =_B^p y$$A \simeq B$$A \simeq B$
identity term$\mathrm{refl}_A(a):a =_A a$$\mathrm{apd}_B^p(f):f(a) =_B^p f(b)$$\mathrm{id}_A:A \simeq A$$\mathrm{tr}_B^p:B(a) \simeq B(b)$