Notes on Propositional Equality

25 May 2021 • Type Theory

Table of Contents

Inductively-Defined Equality

In most modern proof assistants, the equality type and its constructor is defined as an inductive type.

data _≑_ {A : Type} (a : A) : A β†’ Type where
  refl : a ≑ a

A proof of equality (i.e. a term whose type is a propositional equality) can then be eliminated by the usual construct for deconstructing inductive data.

          Ξ“ ⊒ p : a ≑ {A} b
          Ξ“ (y : A) (x : a ≑ y) ⊒ P : Type
          Ξ“ ⊒ d : P[y ↦ a][x ↦ refl]
─────────────────────────────────────────────────────────
    match p in _ ≑ y as x return P with
Ξ“ ⊒ | refl β‡’ d                          : P[y ↦ b][x ↦ p]
    end

In the motive P, the target is bound to x and the right side of the equality is bound as an index to y. Note that the left side is inferred from the type of p since it is a parameter. In a core language with only indices and no parameters, the constructor would have more arguments.

data Eq : (A : Type) β†’ A β†’ A β†’ Type where
  refl : (A : Type) β†’ (a : A) β†’ Eq A a a

This is reflected accordingly in the structure of the match expression.

    Ξ“ ⊒ p : Eq A a b
    Ξ“ (X : Type) (y : A) (z : A) (x : Eq X y z) ⊒ P : Type
    Ξ“ (A : Type) (a : A) ⊒ d : P[X ↦ A][y ↦ a][z ↦ a][x ↦ refl A a]
──────────────────────────────────────────────────────────────────────────
    match p in Eq X y z as x return P with
Ξ“ ⊒ | refl A a β‡’ d                         : P[X ↦ A][y ↦ a][z ↦ b][x ↦ p]
    end

The J Eliminator

In a type theory without inductive data types, propositional equality can be defined in terms of formation, introduction, elimination, and computation rules.

Ξ“ ⊒ a : A
Ξ“ ⊒ b : A
──────────────── ≑-form
Ξ“ ⊒ a ≑ b : Type

Ξ“ ⊒ a : A
────────────────── ≑-intro
Ξ“ ⊒ refl a : a ≑ a


Ξ“ ⊒ p : a ≑ b
Ξ“ ⊒ a : A
Ξ“ ⊒ b : A
Ξ“ ⊒ P : (y : A) β†’ a ≑ y β†’ Type
Ξ“ ⊒ d : P a (refl a)
────────────────────────────── J-elim
Ξ“ ⊒ J P d p : P b p

────────────────────── J-comp
Ξ“ ⊒ J P d (refl a) ⊳ d

Notice that J treats the left side of the equality as a β€œparameter”. An alternate formulation that doesn’t do this would type P as (x y : A) β†’ x ≑ y β†’ Type. J can also be treated as a function rather than a construct that takes a fixed number of arguments; in that case, its type would be:

J' : (A : Type) β†’ (a b : A) β†’
     (P : (y : A) β†’ a ≑ y β†’ Type) β†’
     (d : P a (refl a)) β†’ (p : a ≑ b) β†’ P b p

Uniqueness Rule for J

This section is adapted from the nLab article.

Some constructs also have an Ξ·-conversion or uniqueness rule; for equality, this resembles a computation rule where the branch is a function application and the target need not have the canonical refl form.

Ξ“ ⊒ p : a ≑ b
Ξ“ ⊒ a : A
Ξ“ ⊒ b : A
Ξ“ ⊒ P : (y : A) β†’ a ≑ y β†’ Type
Ξ“ ⊒ e : (x : A) β†’ (p : a ≑ x) β†’ P x p
──────────────────────────────────────── J-uniq
Ξ“ ⊒ J P (e a (refl a)) p β‰ˆ e b p : P b p

(Note that this rule is mostly only useful if e is a neutral form.) However, adding this rule is dangerous, because we can now derive the following chain of conversions (below the dashed bar) under the appropriate assumptions (above the solid bar) and definitions (between the two bars):

A : Type
a b : A
p : a ≑ b
────────────────────────────────
l (_ : A) (_ : a ≑ y) : A ≔ a
r (y : A) (_ : a ≑ y) : A ≔ y
P (_ : A) (_ : a ≑ y) : Type ≔ A
--------------------------------
a β‰ˆ l b p                   by reduction
  β‰ˆ J P (l a (refl a)) p    by uniq
  β‰ˆ J P a p                 by reduction
  β‰ˆ J P (r a (refl a)) p    by reduction
  β‰ˆ r b p                   by uniq
  β‰ˆ b : A                   by reduction

In short, given a propositional equality a ≑ b, we are able to derive a definitional equality between a and b. This is equality reflection, making the type theory extensional, and is known to cause undecidable type checking.

The K Eliminator

A complementary eliminator that we can add is the K eliminator, which eliminates equalities with definitionally equal sides. The it cannot be derived from J or the match expression, nor can it derive J.

Ξ“ ⊒ p : a ≑ a
Ξ“ ⊒ a : A
Ξ“ ⊒ P : a ≑ a β†’ Type
Ξ“ ⊒ d : P (refl a)
──────────────────── K-elim
Ξ“ ⊒ K P d p : P p

────────────────────── K-comp
Ξ“ ⊒ K P d (refl a) ⊳ d

UIP from K

K can be used to prove that all equalities on a are equal to refl a (RIP), and together they prove that all equalities of the same type are equal, known as the unicity or uniqueness of identity proofs (UIP). (We treat RIP as a function whose parameters are the assumptions above the solid bar.) UIP in turn, of course, directly implies RIP.

A : Type
a : A
q : a ≑ a
────────────────────────────────── RIP
P (p : a ≑ a) : Type ≔ refl a ≑ p
----------------------------------
K P (refl (refl a)) q : refl a ≑ q

A : Type
a b : A
p q : a ≑ b
────────────────────────────────────────────────── UIP
P (b : A) (p : a ≑ b) : Type ≔ (q : a ≑ b) β†’ p ≑ q
--------------------------------------------------
J P (RIP A a) p q : p ≑ q

A : Type
a : A
q : a ≑ a
────────────────────────────────── RIP'
UIP A a a (refl a) q : refl a ≑ q

Heterogeneous Equality

The formation rule asserts that both sides of the equality must have the same type. We can loosen this condition to create heterogeneous or John Major equality, as coined by Conor McBride. The eliminator is then adjusted accordingly. Just as for the usual homogeneous equality with J, this could also be equivalently defined as a inductive type.

Ξ“ ⊒ a : A
Ξ“ ⊒ b : B
──────────────── β‰…-form
Ξ“ ⊒ a β‰… b : Type

Ξ“ ⊒ a : A
─────────────────── β‰…-intro
Ξ“ ⊒ refl* a : a β‰… a

Ξ“ ⊒ p : a β‰… b
Ξ“ ⊒ a : A
Ξ“ ⊒ b : B
Ξ“ ⊒ P : (Y : Type) β†’ (y : Y) β†’ a β‰… y β†’ Type
Ξ“ ⊒ d : P A a (refl* a)
─────────────────────────────────────────── J*-elim
Ξ“ ⊒ J* P d p : P B b p

─────────────────────── J*-comp
Ξ“ ⊒ J* P d (refl a) ⊳ d

UIP from J*

Interestingly, UIP can be derived from J* alone, since the types of the equalities on both sides of RIP need no longer be the same.

A B : Type
a : A
b : B
q : a β‰… b
───────────────────────────────────────────────────── RIP*
P (B : Type) (b : B) (p : a β‰… b) : Type ≔ refl* a β‰… p
-----------------------------------------------------
J* P (refl* (refl* a)) q : refl* a β‰… q

A B : Type
a : A
b : B
p q : a β‰… b
────────────────────────────────────────────────── UIP*
P (b : A) (p : a β‰… b) : Type ≔ (q : a β‰… b) β†’ p β‰… q
--------------------------------------------------
J* P (RIP* A B a b) p q : p β‰… q

J and K from J*

We cannot derive the usual J or K from J*. Intuitively, it seems like we should be able to prove K by substituting its motive over RIP*, but the problem is that J*’s motive abstracts over the type while K’s doesn’t, leading to the proof getting β€œstuck” at ? below. We see a similar problem with trying to derive J where J’s motive also doesn’t abstract over the type.

A : Type
a b : A
p : a β‰… b
P : (A : Type) β†’ A β†’ Type
─────────────────────────────────────────────────────── subst*
Q (B : Type) (b : B) (_ : a β‰… b) : Type ≔ P A a β†’ P B b
id (pa : P A a) : P A a ≔ pa
-------------------------------------------------------
J* Q id p : P A a β†’ P B b

A : Type
a : A
P : a β‰… a β†’ Type
d : P (refl* a)
p : a β‰… a
───────────────────────────────────────────────────── K?
subst* (a β‰… a) (refl* a) p (RIP* A A a a p) ? d : P p

A : Type
a b : A
P : (y : A) β†’ a β‰… y β†’ Type
d : P a (refl a)
p : a β‰… b
────────────────────────── J?
J* ? d p : P b p

Substitution and Contractibility of Singletons

This section takes material from this discussion.

The J eliminator can be thought of as the induction principle for equality, where the motive depends on the equality being eliminated. We can split the induction principle into a recursion principle, substitution, whose motive does not depend on the equality, and a uniqueness principle, the contractibility of singletons.

The idea behind substitution is that given some equality between a and b, within some proposition P, we can substitute a for b. As in the last section, we can derive this from the J eliminator.

A : Type
a b : A
P : A β†’ Type
p : a ≑ b
──────────────────────────────────────── subst'
Q (y : A) (_ : a ≑ y) : Type ≔ P a β†’ P y
id (pa : P a) : P a ≔ pa
----------------------------------------
J Q id p : P a β†’ P b

A singleton is a type with (propositionally provably) only one inhabitant. Contractibility then states that the only proof of singletonness is reflexivity.

A : Type
a : A
p : (b : A) Γ— (a ≑ b)
─────────────────────────────────────────────────── cos'
P (y : A) (q : a ≑ y) : Type ≔ ⟨a, refl a⟩ ≑ ⟨y, q⟩
---------------------------------------------------
J P (refl ⟨a, refl a⟩) (snd p) : ⟨a, refl a⟩ ≑ p

Alternatively, we can define these as the built-in eliminators for equality.

Ξ“ ⊒ p : a ≑ b
Ξ“ ⊒ a b : A
Ξ“ ⊒ P : A β†’ Type
───────────────────────── subst-elim
Ξ“ ⊒ subst P p : P a β†’ P b

──────────────────────────── subst-comp
Ξ“ ⊒ subst P (refl a) pa ⊳ pa

Ξ“ ⊒ p : (b : A) Γ— (a ≑ b)
Ξ“ ⊒ a : A
───────────────────────── cos-elim
Ξ“ ⊒ cos p : ⟨a, refl a⟩ ≑ p

────────────────────────────────────── cos-comp
Ξ“ ⊒ cos ⟨a, refl a⟩ ⊳ refl ⟨a, refl a⟩

J and K by Substitution

The following proof is adapted from Martin Hofmann’s dissertation, Extensional Concepts in Intensional Type Theory.

We can derive all of the nice properties of equality from substitution and cos as we do from J (such as symmetry, transitivity, and congruence), as well as J itself. The idea is that given P a (refl a), we can substitute across cos ⟨a, p⟩ to obtain a P a p, then substitute once more across p to obtain P b p.

A : Type
a b : A
P : (y : A) β†’ a ≑ y β†’ Type
d : P a (refl a)
p : a ≑ b
───────────────────────────────────────────────── J'
Q (y : A) : Type ≔ (p : a ≑ y) β†’ P y p
R (y : A) Γ— (p : a ≑ y) : Type ≔ P y p
e (p : a ≑ a) : P a p ≔ subst R (cos ⟨a, p⟩) d
-------------------------------------------------
subst Q p e p : P b p

Alternatively, if we have RIP, we can substitute across that to get P a p from P a (refl a).

A : Type
a b : A
P : (y : A) β†’ a ≑ y β†’ Type
d : P a (refl a)
p : a ≑ b
───────────────────────────────────────────────── J'
Q (y : A) : Type ≔ (p : a ≑ y) β†’ P y p
e (p : a ≑ a) : P a p ≔ subst (P a) (RIP A a p) d
-------------------------------------------------
subst Q p e p : P b p

Suppose now that we only have RIP or UIP with no K. We can then easily recover K with a single application of substitution.

A : Type
a : A
P : a ≑ a β†’ Type
d : P (refl a)
p : a ≑ a
─────────────────────────── K'
subst P (RIP A a p) d : P p

Congruence and Coercion

Congruence of equality and coercion of a term along an equality of types can both be proven from substitution alone.

A B : Type
a b : A
f : A β†’ B
p : a ≑ b
────────────────────────────────── cong'
P (y : A) : Type ≔ f a ≑ f y
----------------------------------
subst P p (refl (f a)) : f a ≑ f b

A B : Type
p : A ≑ B
a : A
──────────────────────── coe'
id (T : Type) : Type ≔ T
------------------------
subst id p a : B

On the other hand, we could define these two properties as built-in eliminators for equality. If we deal only in homogeneous equality, then the function applied in congruence must be non-dependent, but it can be dependent if we instead typed it as a heterogeneous equality.

Ξ“ ⊒ p : a ≑ b
Ξ“ ⊒ a : A
Ξ“ ⊒ b : A
Ξ“ ⊒ f : A β†’ B
──────────────────────── cong-elim
Ξ“ ⊒ cong f p : f a ≑ f b

Ξ“ ⊒ p : A ≑ B
Ξ“ ⊒ A : Type
Ξ“ ⊒ B : Type
───────────────── coe-elim
Ξ“ ⊒ coe p : A β†’ B

──────────────────────────────── cong-comp
Ξ“ ⊒ cong f (refl a) ⊳ refl (f a)

────────────────────── coe-comp
Ξ“ ⊒ coe (refl A) a ⊳ a

These two, in turn, can be used to define substitution.

A : Type
a b : A
P : A β†’ Type
p : a ≑ b
────────────────────────── subst'
coe (cong P p) : P a β†’ P b

Congruence with Dependent Functions

When using homogeneous equality, the function applied in congruence must be nondependent for both sides of the equality to have the same type. If we use heterogeneous equality, we can allow dependent functions. Alternatively, since we already have the proof of equality of the elements that the function is applied over, surely their types must be equal as well. We can then use substitution to β€œfix” the type of one side of the resultant equality. Instead of calling it dependent congruence, we’ll call it apd in the HoTT tradition.

Ξ“ ⊒ P : A β†’ Type
Ξ“ ⊒ p : a ≑ b
Ξ“ ⊒ a : A
Ξ“ ⊒ b : A
Ξ“ ⊒ f : (x : A) β†’ P x
───────────────────────────────────── apd-elim
Ξ“ ⊒ apd P f p : subst P p (f a) ≑ f b

───────────────────────────────── apd-comp
Ξ“ ⊒ apd P f (refl a) ⊳ refl (f a)

We can also prove apd directly from J. Since substitution and cos prove J, this means that apd could also be proven that way.

A : Type
a b : A
P : A β†’ Type
f : (x : A) β†’ P x
p : a ≑ b
──────────────────────────────────────────────────── apd'
Q (y : A) (p : a ≑ y) : Type ≔ subst P p (f a) ≑ f y
----------------------------------------------------
J Q (refl (f a)) p : subst P p (f a) ≑ f b

Regularity

Notice that congruence and coercion compute only on reflexivity. We may want to also compute congruence when f is constant with respect to its argument, making both sides of its type definitionally equal. Similarly, we may want to also compute coercion when both sides of the type of p are definitional equal, regardless of whether p itself is reflexivity or not. (Of course, with UIP, p would be propositionally equal to reflexivity.) We can then add regularity rules allowing them to compute this way. If applied to the variants of coercion and congruence that carried all of the relevant types with them, as is the case with cong' and coe', we can avoid type checking in the premises as well.

Ξ“ ⊒ p : a ≑ b
Ξ“ ⊒ a : A
Ξ“ ⊒ b : A
Ξ“ ⊒ f : A β†’ B
Ξ“ ⊒ f a β‰ˆ f b
───────────────────────────────────── cong-reg
Ξ“ ⊒ cong f p ⊳ refl (f a) : f a ≑ f b

Ξ“ ⊒ f a β‰ˆ f b
────────────────────────────────── cong'-reg
Ξ“ ⊒ cong' A B a b f p ⊳ refl (f a)

Ξ“ ⊒ p : A ≑ B
Ξ“ ⊒ a : A
Ξ“ ⊒ A β‰ˆ B
─────────────────── coe-reg
Ξ“ ⊒ coe p a ⊳ a : B

Ξ“ ⊒ A β‰ˆ B
─────────────────── coe'-reg
Ξ“ ⊒ coe A B p a ⊳ a

If substitution is defined by coercion and congruence, then subst P p on an equality p : a ≑ b will also compute when the motive P is constant with respect to a and b. Furthermore, J defined using substition will compute this way as well. Note that this is orthogonal to UIP: congruence applied to an equality p : a ≑ a not (yet) definitionally equal to refl a will not compute without this rule even with RIP.

Mid-Summary

Below summarizes the various relationships among J, K, substitution, and RIP/UIP. If you have the left side of the turnstile, then you may derive the right side.

J          ⊒ subst, cos
K          ⊒ RIP
RIP, J     ⊒ UIP
UIP        ⊒ RIP
subst, cos ⊒ J
subst, RIP ⊒ K
J*         ⊒ RIP*, UIP*, subst*
J*         ⊬ J, K
subst      ⊒ coe, cong
coe, cong  ⊒ subst
J          ⊒ apd

Equality also satisfies the two other properties of equivalence relations: symmetry and transitivity. We prove them here with substitution, but they can be proven directly using J as well.

A : Type
a b : A
p : a ≑ b
────────────────────────── sym
P (y : A) : Type ≔ y ≑ a
--------------------------
subst P p (refl a) : b ≑ a

A : Type
a b c : A
p : a ≑ b
q : b ≑ c
──────────────────────── trans
P (y : A) : Type ≔ a ≑ y
------------------------
subst P q p : a ≑ c

Extensional Equality

The following is also lifted from Hofmann’s Extensional Concepts in Intensional Type Theory.

TODO: Add blurb about extensional equality

Extensional equality is characterized by the combination of two rules: equality reflection, where a propositional equality yields a definitional one, and a definitional form of UIP.

Ξ“ ⊒ a : A
Ξ“ ⊒ b : A
Ξ“ ⊒ p : a ≑ b
───────────── ≑-reflect
Ξ“ ⊒ a β‰ˆ b : A

Ξ“ ⊒ a : A
Ξ“ ⊒ b : A
Ξ“ ⊒ q : a ≑ b
────────────────────── ≑-RIP
Ξ“ ⊒ refl a β‰ˆ q : a ≑ b

In ≑-RIP, the type of refl a correctly converts to a ≑ b via reflection of p itself. Then with reflection and RIP, we can derive contractibility of singletons, while coercion and congruence requires only reflection, and therefore the J eliminator can be derived as well. On the other hand, if we already had the J eliminator, we can derive RIP via equality reflection. (Thanks to @plt_amy for pointing this out.)

A : Type
a b : A
q : a ≑ b
───────────────────────────────────────── RIP''
P (b : A) (p : a ≑ b) : Type ≔ refl a ≑ p
-----------------------------------------
J P (refl (refl a)) q : refl a ≑ q

In the type of the body of P, refl a has type a ≑ b by reflection of p, and the application of J is well-typed by reflection of q. Since J is derivable from the combination of coercion, congruence, and contractibility of singletons, and the first two are derivable from reflection, the missing piece is really only contractibility of singletons, which in essence yields a form of uniqueness of identity proofs anyway.

Function Extensionality

There are often more equalities that we wish to be able to express than can be proven with just reflexivity and its eliminators. One of these is function extensionality, which equates two functions when they return the same output for each input. In other words, functions are then pointwise or observationally equal. Without extensionality, functions are only provably equal when they are implemented in definitionally equal ways.

Ξ“ ⊒ f : (x : A) β†’ B x
Ξ“ ⊒ g : (x : A) β†’ B x
Ξ“ ⊒ h : (x : A) β†’ f x ≑ g x
─────────────────────────── funext
Ξ“ ⊒ funext f g h : f ≑ g

Unfortunately, there’s no satisfactory way of computing on the equality from function extensionality, because our eliminators only compute on reflexivity. In other words, adding function extensionality breaks canonicity, because the canonical proof of equality, reflexivity, is no longer the only closed proof of equality.

On the other hand, we can derive function extensionality from equality reflection using Ξ·-conversion of functions. Let Ξ“ = (f g : (x : A) β†’ B x) (h : (x : A) β†’ f x ≑ g x). The following derivation tree sketches out how a proof of f ≑ g can be derived using h.

         Ξ“ ⊒ h : (x : A) β†’ f x ≑ g x
         ─────────────────────────── β†’-elim
         Ξ“ (x : A) ⊒ h x : f x ≑ g x
         ─────────────────────────── ≑-reflect
            Ξ“ (x : A) ⊒ f x β‰ˆ g x
───────────────────────────────────────────── β†’-intro, β†’-uniq
Ξ“ ⊒ f β‰ˆ Ξ» (x : A) β‡’ f x β‰ˆ Ξ» (x : A) β‡’ g x β‰ˆ g
───────────────────────────────────────────── ≑-intro, conv
             Ξ“ ⊒ refl f : f ≑ g

The converse of function extensionality, that equal functions are pointwise equal, can easily be proven by substitution.

A : Type
B : A β†’ Type
f g : (x : A) β†’ B x
p : f ≑ g
────────────────────────────────────────────────── happly
P (g : (x : A) β†’ B x) : Type ≔ (x : A) β†’ f x ≑ g x
d (x : A) : f x ≑ f x ≔ refl (f x)
--------------------------------------------------
subst P p d : (x : A) β†’ f x ≑ g x

Propositional Truncation/Squash Types

Sometimes we would like to treat proofs of a certain proposition as being irrelevant so that they are all propositionally equal. This can be done by truncating or squashing the type and its term(s), and restricting manipulating the terms in ways that do not allow us to distinguish among them. Given some function f from A to an output type that only depends on the squashed input, we can β€œlift” that function to one that takes a squashed β€–Aβ€– as input instead.

Ξ“ ⊒ A : Type
────────────── sq-form
Ξ“ ⊒ β€–Aβ€– : Type

Ξ“ ⊒ a : A
───────────── sq-intro
Ξ“ ⊒ |a| : β€–Aβ€–

Ξ“ ⊒ a : A
Ξ“ ⊒ b : A
──────────────────────── sq-ax
Ξ“ ⊒ sqax a b : |a| ≑ |b|

Ξ“ ⊒ P : β€–Aβ€– β†’ Type
Ξ“ ⊒ f : (x : A) β†’ P |x|
Ξ“ ⊒ p : (x y : A) β†’ f x β‰… f y
────────────────────────────── sq-elim
Ξ“ ⊒ unsq P p f : (x : β€–Aβ€–) β†’ P x

────────────────────── sq-comp
Ξ“ ⊒ unsq P f |a| ⊳ f a

In addition to the usual formation, introduction, elimination, and computation rules, we also have an axiom that states that any two squashed values of the squashed type are equal. Notice that this also breaks canonicity of propositional equality.

Because the function applied in the eliminator is dependent, the condition that it acts identically on all elements is a heterogeneous equality rather than a homogeneous one. However, because the return type of the function can only depend on the squashed value, and we know that the squashed values are all equal by sqax, we can alternatively replace f x β‰… f y by subst P (sqax x y) (f x) ≑ f y. On the other hand, since substitution does not reduce on sqax, if P is nondependent, the condition does not become f x ≑ f y as we would intuitively expect, not unless we have the extra computation rule for congruence.

Quotient Types

This section adapts Martin Hofmann’s presentation in A simple model for quotient types.

Instead of treating all terms of a type as equal, perhaps we would like to treat only some of them as equal. Quotient types allow us to do so with a quotient relation ~: two quotiented terms are equal if they are related. This is analogous to quotient sets, where an equivalence relation divides up the members of a set into equivalence classes. Like with squash types, the eliminator allows β€œlifting” a function f on A to a function on the quotient space Aβ§Έ~.

Ξ“ ⊒ A : Type
Ξ“ ⊒ ~ : A β†’ A β†’ Type
──────────────────── Q-form
Ξ“ ⊒ Aβ§Έ~ : Type

Ξ“ ⊒ a : A
Ξ“ ⊒ ~ : A β†’ A β†’ Type
──────────────────── Q-intro
Ξ“ ⊒ [a]Λ· : Aβ§Έ~

Ξ“ ⊒ a : A
Ξ“ ⊒ b : A
Ξ“ ⊒ ~ : A β†’ A β†’ Type
────────────────────────────────── Q-ax
Ξ“ ⊒ QaxΛ· a b : a ~ b β†’ [a]Λ· ≑ [b]Λ·

Ξ“ ⊒ P : Aβ§Έ~ β†’ Type
Ξ“ ⊒ ~ : A β†’ A β†’ Type
Ξ“ ⊒ f : (x : A) β†’ P [x]Λ·
Ξ“ ⊒ p : (x y : A) β†’ (r : x ~ y) β†’ f x β‰… f y
─────────────────────────────────────────── Q-elim
Ξ“ ⊒ QelimΛ· P p f : (x : Aβ§Έ~) β†’ P x

─────────────────────────── Q-comp
Ξ“ ⊒ QelimΛ· P p f [a]Λ· ⊳ f a

Also like with squash types, Qax can yield a noncanonical closed proof of equality. We can also replace f x β‰… f y by subst P (QaxΛ· x y r) (f x) ≑ f y in the condition of the eliminator just as was done for squash types, with the same problem of substitution not reducing on Qax unless we have the extra computation rule for congruence.

Effectiveness

The follow proof is from Nuo Li’s Bachelor’s thesis, Quotient Types in Type Theory.

An important property that quotient types can have is effectiveness: the only elements belonging to an equivalence class of a quotiented element with respect to propositional equality are the ones related by the quotient relation. For a quotient to be effective, the relation must be an equivalence relation; that is, it must be reflexive, symmetric, and transitive. It also has to satisfy a weak form of propositional extensionality: if x ~ z ↔ y ~ z, then x ~ z ≑ y ~ z. This can be derived from full propositional extensionality, which equates any two bi-implicated relations. We stick to only the weak extensionality, which is all we need, and collect all these facts in a record type.

record PropEquiv (A : Type) (~ : A β†’ A β†’ Type) : Type where
  ~refl : (x : A) β†’ x ~ x
  ~sym : (x y : A) β†’ x ~ y β†’ y ~ x
  ~trans : (x y z : A) β†’ x ~ y β†’ y ~ z β†’ x ~ z
  ~ext : (x y z : A) β†’ (y ~ z β†’ x ~ z) β†’ (x ~ z β†’ y ~ z) β†’ x ~ z ≑ y ~ z

With these, we can prove a lemma we will need later: if x ~ y, then for any z, x ~ z ≑ y ~ z.

A : Type
~ : A β†’ A β†’ Type
pe : PropEquiv A ~
z x y : A
r : x ~ y
────────────────────────────────────────────────────── lemma₁
yzxz : y ~ z β†’ x ~ z ≔ pe.~trans x y z r
xzyz : x ~ z β†’ y ~ z ≔ pe.~trans y x z (pe.~sym x y r)
------------------------------------------------------
pe.~ext x y z yzxz xzyz : x ~ z ≑ y ~ z

Let a be some particular A we can quotient by ~, and let P : A β†’ Type be a function defined by Ξ» x β‡’ x ~ a. Then we can β€œlift” P to a function PΜ‚ : Aβ§Έ~ β†’ Type using QelimΛ·, since lemma₁ gives us the required condition that if x ~ y then P x ≑ P y when instantiated with a.

Now we are ready to tackle effectiveness. Suppose we have p : [a]Λ· ≑ [b]Λ·, where ~ is a propositional equivalence relation. We wish to show that a ~ b. By congruence on p, using our lifted function, we have that PΜ‚ [a]Λ· ≑ PΜ‚ [b]Λ·, which computes to a ~ a ≑ b ~ a. Finally, by reflexivity of ~, coercion along the equality, and symmetry of ~, we obtain a ~ b. The full proof is outlined below.

A : Type
~ : A β†’ A β†’ Type
pe : PropEquiv A ~
a b : A
p : [a]Λ· ≑ [b]Λ·
────────────────────────────────────────────────── eff
P (x : A) : Type ≔ x ~ a
Q (_ : Aβ§Έ~) : Type ≔ Type
PΜ‚ (x : Aβ§Έ~): Type ≔ QelimΛ· Q (lemma₁ A ~ pe a) P x
lemmaβ‚‚ : a ~ a ≑ b ~ a ≔ cong PΜ‚ p
--------------------------------------------------
pe.~sym (coe lemmaβ‚‚ (pe.~refl a)) : a ~ b

Squashes from Quotients

Squashes can be seen as a special case of quotients where the quotient relation is trivially true.

a ~ b ≔ Unit
βˆ₯Aβˆ₯ ≔ A/~
|a| ≔ [a]Λ·
sqax a b ≔ QaxΛ· a b unit
unsq P p f ≔ QelimΛ· P (Ξ» x y _ β‡’ p x y) f

Higher Inductive Types

Higher inductive types are inductive types with quotient-like behaviour: with equality constructors, you can specify new equalities between your elements. One popular HIT is the interval, which consists of two endpoints and a path between them

data 𝕀 : Type where
  𝟎 : 𝕀
  𝟏 : 𝕀
  seg : 𝟎 ≑ 𝟏

The eliminator for the interval requires the same kind of condition as quotient types: when eliminating an element of the interval with some function on an endpoint, the eliminator must treat both endpoints equally. On top of that, applying the eliminator to both sides of the segment should yield exactly the same proof that both endpoints are treated equally.

Ξ“ ⊒ P : 𝕀 β†’ Type
Ξ“ ⊒ bβ‚€ : P 𝟎
Ξ“ ⊒ b₁ : P 𝟏
Ξ“ ⊒ s : bβ‚€ β‰… b₁
───────────────────────────────────── 𝕀-elim
Ξ“ ⊒ 𝕀-elim P bβ‚€ b₁ s : (i : 𝕀) β†’ P i

─────────────────────────── 𝕀-compβ‚€
Ξ“ ⊒ 𝕀-elim P bβ‚€ b₁ s 𝟎 ⊳ bβ‚€

─────────────────────────── 𝕀-comp₁
Ξ“ ⊒ 𝕀-elim P bβ‚€ b₁ s 𝟏 ⊳ b₁

─────────────────────────────────── 𝕀-comp-seg
Ξ“ ⊒ apd P (𝕀-elim P bβ‚€ b₁ s) seg ⊳ s

Again, use of heterogeneous equality can be replaced by a homogeneous one if we do the appropriate substitution; s would then have type subst P seg bβ‚€ ≑ b₁.

Functions on higher inductive types can also be defined by pattern matching on all constructors, including on the equality constructors. Just as a function f defined by pattern matching on the data constructors describes how f acts on each of them, pattern matching on the equality constructors describes how applying f on both sides of the equality yields an equality. For instance, defining the interval eliminator with pattern matching below, the type of s must be 𝕀-elim' 𝟎 β‰… 𝕀-elim' 𝟏, or bβ‚€ β‰… b₁ (or the homogeneous alternative if desired). The application 𝕀-elim' seg should be thought of as a shorthand for apd P 𝕀-elim' seg.

𝕀-elim' : (i : 𝕀) β†’ P i
𝕀-elim' 𝟎 ≔ bβ‚€
𝕀-elim' 𝟏 ≔ b₁
𝕀-elim' seg ≔ s

The Interval and Function Extensionality

Curiously, just by defining the interval type, we are able to prove function extensionality.

A : Type
B : A β†’ Type
f : (x : A) β†’ B x
g : (x : A) β†’ B x
h : (x : A) β†’ f x ≑ g x
──────────────────────────────────────────────────────────────── funext
k (i : 𝕀) (x : A) : B x ≔ 𝕀-elim (Ξ» _ β‡’ B x) (f x) (g x) (h x) i
----------------------------------------------------------------
cong k seg : f ≑ g

The resulting type is Ξ» (x : A) β‡’ f x ≑ Ξ» (x : A) β‡’ g x by reduction of the interval eliminator, but the uniqueness rule for functions will get us the final desired type.

Quotients as a HIT

Quotient types can be implemented as a higher inductive type where the equality induced by the quotient relation is an equality constructor.

data _β§Έ_ (A : Type) (~ : A β†’ A β†’ Type) : Type where
  [_]˷ : (a : A) → A⧸~
  QaxΛ· : (a b : A) β†’ a ~ b β†’ [a]Λ· ≑ [b]Λ·

The eliminator for quotients also requires that the function being defined behaves identically on all equalities constructed by Qax, with the additional information that equal elements are related. We define by pattern matching the eliminator that corresponds to QelimΛ· P p f [a]Λ·.

Q-elim' : βˆ€ {A ~} β†’ (a : Aβ§Έ~) β†’ P a
Q-elim' [a]Λ· ≔ f a
Q-elim' (QaxΛ· a b r) ≔ p a b r

Cubical Type Theory

Most of this material is adapted from NaΓ―ve Cubical Type Theory and Cubical Methods in HoTT and UF. Please note that this section is still under construction.

In cubical type theories, the interval is taken as a primitive pretype. The notion of propositional equality is encoded as a path from an interval element into some type, and two inhabitants of the type are equal if there is such a path between them. Note that we allow the type of the endpoints of paths to vary along the path; in other words, we have a dependent path corresponding to a heterogeneous equality. Note also that the introduction form for paths, the interval abstraction, resemble functions, but are distinct from them: (Ξ›i. a) is a path from a[i ↦ 𝟎] to a[i ↦ 𝟏], whereas (Ξ»i β‡’ a) is a function. We use typed conversion and reduction so that paths applied to the interval endpoints can reduce to the path endpoints despite not being in the canonical interval abstraction form.

(i : 𝕀) ∊ Ξ“
─────────── 𝕀-var
Ξ“ ⊒ i : 𝕀

───────── 𝕀-𝟎
Ξ“ ⊒ 𝟎 : 𝕀

───────── 𝕀-𝟏
Ξ“ ⊒ 𝟏 : 𝕀

Ξ“ ⊒ A : 𝕀 β†’ Type
Ξ“ ⊒ a : A 𝟎
Ξ“ ⊒ b : A 𝟏
────────────────────── path-form
Ξ“ ⊒ pathd A a b : Type

Ξ“ (i : 𝕀) ⊒ a : A
────────────────────────────────────────────── path-intro
Ξ“ ⊒ (Ξ›i. a) : pathd (Ξ»i β‡’ A) a[i ↦ 𝟎] a[i ↦ 𝟏]

Ξ“ ⊒ r : 𝕀
Ξ“ ⊒ p : pathd A a b
─────────────────── path-elim
Ξ“ ⊒ p r : A r

Ξ“ (i : 𝕀) ⊒ a : A
──────────────────────────────────── path-endβ‚€
Ξ“ ⊒ (Ξ›i. a) 𝟎 ⊳ a[i ↦ 𝟎] : A[i ↦ 𝟎]

Ξ“ (i : 𝕀) ⊒ a : A
─────────────────────────────────── path-end₁
Ξ“ ⊒ (Ξ›i. a) 𝟏 ⊳ a[i ↦ 𝟏] : A[i ↦ 𝟏]

Ξ“ ⊒ p : pathd A a b
─────────────────── path-uniqβ‚€
Ξ“ ⊒ p 𝟎 ⊳ a : A 𝟎

Ξ“ ⊒ p : pathd A a b
─────────────────── path-uniq₁
Ξ“ ⊒ p 𝟏 ⊳ b : A 𝟏

Ξ“ (i : 𝕀) ⊒ e₁ β‰ˆ eβ‚‚ i : A i
─────────────────────────────── path-uniq
Ξ“ ⊒ (Ξ›i. e₁) β‰ˆ eβ‚‚ : pathd A a b

With these rules alone, we are already able to prove a few properties of equality we would expect to hold: reflexivity and (dependent, heterogeneous) congruence. Just as with the interval HIT, we can also prove function extensionality.

A : Type
a : A
──────────────────────────── refl*
(Ξ›_. a) : pathd (Ξ»_ β‡’ A) a a

A : 𝕀 β†’ Type
a : A 𝟎
b : A 𝟏
P : (i : 𝕀) β†’ A i β†’ Type
f : (i : 𝕀) β†’ (x : A i) β†’ P i x
p : pathd A a b
──────────────────────────────────────────────────── apd*
(Ξ›i. f i (p i)) : pathd (Ξ»i β‡’ P i (p i)) (f a) (f b)

A : Type
B : A β†’ Type
f : (x : A) β†’ B x
g : (x : A) β†’ B x
h : (x : A) β†’ pathd (Ξ»_ β‡’ B x) (f x) (g x)
────────────────────────────────────────────── funext'
(Ξ›i. (h x) i) : pathd (Ξ»_ β‡’ (x : A) β†’ B x) f g

Coercion

However, this is not enough: we cannot prove coercion or substitution. Since substitution can be proven from coercion and congruence, we take coercion as an additional primitive form. It takes an element of some type at some interval element and gives an element of that type at a different interval element, and reduces when the interval elements are the same. Additionally, it reduces if the type does not change between the two interval elements, similar to the regularity rule for coercions.

Ξ“ ⊒ i : 𝕀
Ξ“ ⊒ j : 𝕀
Ξ“ ⊒ A : 𝕀 β†’ Type
───────────────────────────── coe
Ξ“ ⊒ coe [i ⇝ j] A : A i β†’ A j

─────────────────────── coe-comp
Ξ“ ⊒ coe [i ⇝ i] A a ⊳ a

Ξ“ ⊒ A i β‰ˆ A j
─────────────────────── coe-reg
Ξ“ ⊒ coe [i ⇝ j] A a ⊳ a

Now we are able to prove some more properties: heterogeneous substitution, heterogeneous symmetry, and homogeneous transitivity.

A : 𝕀 β†’ Type
a : A 𝟎
b : A 𝟏
P : (i : 𝕀) β†’ A i β†’ Type
p : pathd A a b
──────────────────────────────────────────── subst*
coe [𝟎 ⇝ 𝟏] (Ξ›i. P i (p i)) : P 𝟎 a β†’ P 𝟏 b

A : 𝕀 β†’ Type
a : A 𝟎
b : A 𝟏
p : pathd A a b
──────────────────────────────────────────────── sym*
Q (i : 𝕀) : Type ≔ pathd (Ξ»_ β‡’ Type) (A i) (A 𝟎)
A' (i : 𝕀) : Q i ≔ coe [𝟎 ⇝ i] Q (Ξ›_. A 𝟎)
P (i : 𝕀) : Type ≔ pathd (A' i) (p i) a
------------------------------------------------
coe [𝟎 ⇝ 𝟏] P (Ξ›_. a) : pathd (A' 𝟏) b a

A : Type
a b c : A
p : pathd (Ξ»_ β‡’ A) a b
q : pathd (Ξ»_ β‡’ A) b c
───────────────────────────────────────────────── trans'
P (y : A) : Type ≔ pathd (Ξ»_ β‡’ A) a y
-------------------------------------------------
coe [𝟎 ⇝ 𝟏] (Ξ›i. P (q i)) p : pathd (Ξ»_ β‡’ A) a c

De Morgan Operators

Recall that to recover the J eliminator, we need both substitution and contractibility of singletons. We can attempt to prove the contractibility, but we run into a missing piece.

A : 𝕀 β†’ Type
a : A 𝟎
b : A 𝟏
p : pathd A a b
────────────────────────────────────────────────────────────────────────────────────── cos*
Q (i : 𝕀) : Type ≔ pathd (Ξ»_ β‡’ Type) (A 𝟎) (A i)
A' (i : 𝕀) : Q i ≔ coe [𝟎 ⇝ i] Q (Ξ›_. A 𝟎)
--------------------------------------------------------------------------------------
Ξ›i. ⟨p i, Ξ›j. p (i ∧ j)⟩ : pathd (Ξ»i β‡’ (x : A i) Γ— pathd (A' i) a x) ⟨a, Ξ›_. a⟩ ⟨b, p⟩

It appears that we need some sort of operator between interval elements, denoted ∧ above, that gives 𝟏 when i = 𝟏 = j, and 𝟎 otherwise. We can add it as a primitive operator for interval elements, called the meet, as well as a similar operator ∨, the join, and the unary operator ¬, the involution. Then the interval forms a De Morgan algebra, and this is known as De Morgan cubical type theory.

Ξ“ ⊒ i : 𝕀
Ξ“ ⊒ j : 𝕀
───────────── 𝕀-meet
Ξ“ ⊒ i ∧ j : 𝕀

Ξ“ ⊒ i : 𝕀
Ξ“ ⊒ j : 𝕀
───────────── 𝕀-join
Ξ“ ⊒ i ∨ j : 𝕀

Ξ“ ⊒ i : 𝕀
────────── 𝕀-inv
Ξ“ ⊒ Β¬i : 𝕀

────────────── 𝕀-meet-compβ‚€     ────────────── 𝕀-join-comp₁
Ξ“ ⊒ 𝟎 ∧ j ⊳ 𝟎                  Ξ“ ⊒ i ∨ 𝟏 ⊳ 𝟏

────────────── 𝕀-meet-comp₁     ────────────── 𝕀-join-compβ‚€
Ξ“ ⊒ 𝟏 ∧ j ⊳ j                  Ξ“ ⊒ i ∨ 𝟎 ⊳ i

─────────── 𝕀-invβ‚€              ─────────── 𝕀-inv₁
Ξ“ ⊒ ¬𝟎 ⊳ 𝟏                     Ξ“ ⊒ ¬𝟏 ⊳ 𝟎

──────────────────────         ──────────────────────
Ξ“ ⊒ Β¬(i ∧ j) β‰ˆ Β¬i ∨ Β¬j         Ξ“ ⊒ Β¬(i ∨ j) β‰ˆ Β¬i ∨ Β¬j

With substitution and contractibility of singletons, we are now able to derive the (heterogeneous) J eliminator.

A : 𝕀 β†’ Type
a : A 𝟎
b : A 𝟏
P : (i : 𝕀) β†’ (y : A i) β†’ pathd A a y β†’ Type
d : P 𝟎 a (Ξ›_. a)
p : pathd A a b
───────────────────────────────────────────────────────────────────────── J*'
Q (i : 𝕀) (y : A i) : Type ≔ (p : pathd (Ξ»j β‡’ A (i ∧ j)) a y) β†’ P i y p
R (_ : 𝕀) (y : A 𝟎) Γ— (p : pathd (Ξ»_ β‡’ A 𝟎) a y) : Type ≔ P 𝟎 y p
e (p : path (Ξ»_ β‡’ A 𝟎) a a) : P 𝟎 a p ≔ subst R (cos* (Ξ»_ β‡’ A 𝟎) a a p) d
--------------------------------------------------------------------------
subst A a b Q p e p : P 𝟏 b p

The presence of this additional structure also provides a simpler proof of symmetry.

A : 𝕀 β†’ Type
a : A 𝟎
b : A 𝟏
p : pathd A a b
───────────────────────────────────────────────── sym*
P (i : 𝕀) : Type ≔ pathd (Ξ»j β‡’ A (i ∧ Β¬j)) (p i) a
-------------------------------------------------
coe [𝟎 ⇝ 𝟏] P (Ξ›_. a) : pathd (Ξ»j β‡’ A Β¬j) b a

Composition

We can also attempt to prove a heterogeneous version of transitivity. We are given two paths, p and q, whose endpoints types are A and B, coinciding at A 𝟏 β‰ˆ B 𝟎. However, we run into a similar but distinct problem as before.

A B : 𝕀 β†’ Type
a : A 𝟎
b : A 𝟏 β‰ˆ B 𝟎
c : B 𝟏
p : pathd A a b
q : pathd B b c
───────────────────────────────────────────────── trans*
P (i : 𝕀) : Type ≔ pathd (Ξ»j β‡’ ? A B i j) a (q i)
-------------------------------------------------
coe [𝟎 ⇝ 𝟏] P p : pathd (Ξ»j β‡’ ? A B 𝟏 j) a c

The missing path, ? p q i j, should behave as follows:

  • If i = 𝟎, then return A 𝟎.
  • If i = 𝟏, j = 𝟎, then return A 𝟏, i.e. B 𝟎.
  • If i = 𝟏 = j, then return B 𝟏.

This time, it is not the interval elements that we need to somehow combine, but rather A and B. To do this, we need Kan composition, which intuitively β€œcloses” an open n-cube of paths. This is beyond the scope of this post and will not be discussed.

Variants of Cubical Type Theory

So far, a De Morgan cubical type theory has been presented. An alternate presentation derives the interval operators from either heterogeneous composition alone or homogeneous composition with coercion, usually referred to as Cartesian cubical type theory. See Unifying Cubical Models of Univalent Type Theory for further details on the different kinds of cubical type theories and their connections.

Appendix A: Other Relevant Typing Rules

Below are the typing rules for dependent functions and pairs, and a typing rule that uses convertibility to coerce a term to a another type. We omit the type annotation on the pair introductory form when clear from context. We assume that Type is well-behaved and causes no problems with consistency.

Ξ“ ⊒ a : A
Ξ“ ⊒ B : Type
Ξ“ ⊒ A β‰ˆ B
──────────── conv
Ξ“ ⊒ a : B

Ξ“ ⊒ A : Type
Ξ“ (x : A) ⊒ B : Type
────────────────────── β†’-form
Ξ“ ⊒ (x : A) β†’ B : Type

Ξ“ ⊒ A : Type
Ξ“ (x : A) ⊒ e : B
─────────────────────────────── β†’-intro
Ξ“ ⊒ Ξ» (x : A) β‡’ e : (x : A) β†’ B

Ξ“ ⊒ e₁ : (x : A) β†’ B
Ξ“ ⊒ eβ‚‚ : A
───────────────────── β†’-elim
Ξ“ ⊒ e₁ eβ‚‚ : B[x ↦ eβ‚‚]

──────────────────────────────────── β†’-comp
Ξ“ ⊒ (Ξ» (x : A) β‡’ e₁) eβ‚‚ ⊳ e₁[x ↦ eβ‚‚]

Ξ“ (x : A) ⊒ e₁ β‰ˆ eβ‚‚ x 
─────────────────────── β†’-uniq
Ξ“ ⊒ Ξ» (x : A) β‡’ e₁ β‰ˆ eβ‚‚

Ξ“ ⊒ A : Type
Ξ“ (x : A) ⊒ B : Type
────────────────────── Γ—-form
Ξ“ ⊒ (x : A) Γ— B : Type

Ξ“ ⊒ (x : A) Γ— B : Type
Ξ“ ⊒ a : A
Ξ“ ⊒ b : B[x ↦ a]
─────────────────────────────────────── Γ—-intro
Ξ“ ⊒ ⟨a, b⟩ as (x : A) Γ— B : (x : A) Γ— B

Ξ“ ⊒ p : (x : A) Γ— B
─────────────────── Γ—-elim₁
Ξ“ ⊒ fst p : A

Ξ“ ⊒ p : (x : A) Γ— B
──────────────────────── Γ—-elimβ‚‚
Ξ“ ⊒ snd p : B[x ↦ fst p]

────────────────── Γ—-comp₁
Ξ“ ⊒ fst ⟨a, b⟩ ⊳ a

────────────────── Γ—-compβ‚‚
Ξ“ ⊒ snd ⟨a, b⟩ ⊳ b

────────────────────── Γ—-uniq
Ξ“ ⊒ ⟨fst p, snd p⟩ β‰ˆ p

Convertibility (β‰ˆ) is defined to be the reflexive, symmetric, compatible closure of multi-step reduction (⊳) and whatever other uniqueness rules that are defined throughout. Convertibility is generally untyped and does not rely on typing judgements and is untyped. When convertibility is typed, the type is an input, whereas when reduction is typed, it is an output. Then in the general convertibility rule, we check convertibility of the types as well.

Ξ“ ⊒ e₁ ⊳* e : A₁
Ξ“ ⊒ eβ‚‚ ⊳* e : Aβ‚‚
Ξ“ ⊒ A : Type
Ξ“ ⊒ A β‰ˆ A₁ : Type
Ξ“ ⊒ A β‰ˆ Aβ‚‚ : Type
───────────────── β‰ˆ-⊳*
Ξ“ ⊒ e₁ β‰ˆ eβ‚‚ : A

Appendix B: Level-Heterogeneous Equality

This is a generalization of heterogeneous equality to be heterogeneous in the universe level as well.

Ξ“ ⊒ ℓ₁ : Level
Ξ“ ⊒ β„“β‚‚ : Level
Ξ“ ⊒ A : Set ℓ₁
Ξ“ ⊒ B : Set β„“β‚‚
Ξ“ ⊒ a : A
Ξ“ ⊒ b : B
───────────────────────── β‰Š-form
Ξ“ ⊒ a β‰Š b : Set (ℓ₁ βŠ” β„“β‚‚)

Ξ“ ⊒ a : A
Ξ“ ⊒ A : Set β„“
Ξ“ ⊒ β„“ : Level
────────────────── β‰Š-intro
Ξ“ ⊒ refl a : a β‰Š a

Ξ“ ⊒ p : a β‰Š b
Ξ“ ⊒ a : A
Ξ“ ⊒ b : B
Ξ“ ⊒ A : Set ℓ₁
Ξ“ ⊒ B : Set β„“β‚‚
Ξ“ ⊒ P : (β„“ : Level) β†’ (Y : Set β„“) β†’ (y : Y) β†’ a β‰Š y β†’ Type
Ξ“ ⊒ d : P ℓ₁ A a (refl a)
────────────────────────────────────────────────────────── H-elim
Ξ“ ⊒ H P d p : P β„“β‚‚ B b p

Ξ“ ⊒ p : a β‰Š b
Ξ“ ⊒ a : A
Ξ“ ⊒ b : B
Ξ“ ⊒ A B : Set β„“
Ξ“ ⊒ P : (Y : Set β„“) β†’ (y : Y) β†’ a β‰Š y β†’ Type
Ξ“ ⊒ d : P A a (refl a)
──────────────────────────────────────────── I-elim
Ξ“ ⊒ I P d p : P B b p

Ξ“ ⊒ p : a β‰Š b
Ξ“ ⊒ a b : A
Ξ“ ⊒ P : (y : A) β†’ a β‰Š y β†’ Type
Ξ“ ⊒ d : P a (refl a)
────────────────────────────── J-elim
Ξ“ ⊒ J P d p : P b p

Ξ“ ⊒ p : a β‰Š a
Ξ“ ⊒ P : a β‰Š a β†’ Type
Ξ“ ⊒ d : P (refl a)
──────────────────── K-elim
Ξ“ ⊒ K P d p : P p
 equality  type theory