Table of Contents
- Inductively-Defined Equality
- The J Eliminator
- The K Eliminator
- Heterogeneous Equality
- Substitution and Contractibility of Singletons
- Congruence and Coercion
- Mid-Summary
- Extensional Equality
- Function Extensionality
- Propositional Truncation/Squash Types
- Quotient Types
- Higher Inductive Types
- Cubical Type Theory
- Appendix A: Other Relevant Typing Rules
- Appendix B: Level-Heterogeneous Equality
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; note however that we may only eliminate equalities over terms whose types we already know are equal.
Ξ β’ a : A
Ξ β’ b : B
ββββββββββββββββ β
-form
Ξ β’ a β
b : Type
Ξ β’ a : A
βββββββββββββββββββ β
-intro
Ξ β’ refl* a : a β
a
Ξ β’ p : a β
b
Ξ β’ a : A
Ξ β’ b : A
Ξ β’ P : (c : A) β a β
c β Type
Ξ β’ d : P a (refl* a)
βββββββββββββββββββββββββββββββββββββββββββ J*-elim
Ξ β’ J* P d p : P b p
βββββββββββββββββββββββ J*-comp
Ξ β’ J* P d (refl a) β³ d
UIP* and K* 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. We can then prove K by substituting its motive over RIP*.
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
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 B a b) p q : p β
q
A : Type
a b : A
p : a β
b
P : A β Type
βββββββββββββββββββββββββββββββββββββββββββββββββββββββ subst*
Q (b : A) (_ : a β
b) : Type β P a β P b
id (pa : P A a) : P A a β pa
-------------------------------------------------------
J* Q id p : P a β P 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) P d : P 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 returnA π. - If
i = π, j = π, then returnA π, i.e.B π. - If
i = π = j, then returnB π.
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