|
-- Equality with an explicit domain
|
|
let
|
|
Eq : (A : Type) (x y : A) -> Type;
|
|
Eq A x y = x == y;
|
|
|
|
-- Identity function with an explicit domain
|
|
-- (works as a type annotation)
|
|
let
|
|
the : (A : Type) -> A -> A;
|
|
the A x = x;
|
|
|
|
-- Singleton types
|
|
-- The subtype of A generated by "being equal to x : A"
|
|
let
|
|
singl : (A : Type) (x : A) -> Type;
|
|
singl A x = (y : A) * x == y;
|
|
|
|
-- Singletons are contractible
|
|
let
|
|
singlC : {A : Type} {a b : A} (p : a == b) -> Eq (singl A a) (a, refl) (b, p);
|
|
singlC p = (p, ());
|
|
|
|
-- Substitution follows from transport + congruence
|
|
-- (just transport by the congruence under P)
|
|
let
|
|
subst : {A : Type} (P : A -> Type) {x y : A} (p : x == y) -> P x -> P y;
|
|
subst P path px = coe (cong P path) px;
|
|
|
|
let
|
|
coe2 : {A B : Type} (p : A == B) → A → B;
|
|
coe2 p = subst (λ x → x) p;
|
|
|
|
-- Based path induction follows from contractibility of singletons +
|
|
-- substitution
|
|
let
|
|
J : {A : Type} (a : A) (P : (b : A) -> a == b -> Type)
|
|
(d : P a refl) (b : A) (p : a == b) -> P b p;
|
|
J {A} a P d b p =
|
|
subst {singl A a} (λ y → P y.1 y.2) (singlC p) d;
|
|
|
|
let
|
|
JComp : {A : Type} (a : A) (P : (b : A) -> a == b -> Type)
|
|
(d : P a refl)
|
|
→ J {A} a P d a refl == d;
|
|
JComp {A} a P d = refl;
|
|
|
|
-- Symmetry follows from axiom J
|
|
let
|
|
symm : {A : Type} {x y : A} (p : x == y) -> y == x;
|
|
symm {A} {x} {y} p = J x (λ y p -> y == x) refl y p;
|
|
|
|
let
|
|
symIsRefl : {A : Type} {a : A} → symm (refl {A} {a}) == refl {A} {a};
|
|
symIsRefl = refl;
|
|
|
|
let
|
|
isContr : Type -> Type;
|
|
isContr A = (x : A) * (y : A) -> y == x;
|
|
|
|
let
|
|
comp : {A : Type} {a b c : A} → a == b → b == c → a == c;
|
|
comp {A} {a} p q = subst (λ x → a == x) q (subst (λ x → a == x) p (refl {A} {a}));
|
|
|
|
let
|
|
trans : {A : Type} {a b c : A} → b == c → a == b → a == c;
|
|
trans {A} {a} p q = comp q p;
|
|
|
|
let
|
|
transSym : {A : Type} {a : A} → (p : a == a) → comp p (symm p) == refl;
|
|
transSym p = refl;
|
|
|
|
let
|
|
existsOne : (A : Type) (B : A -> Type) -> ((x : A) × B x) -> isContr A -> (x : A) -> B x;
|
|
existsOne A B prf contr it =
|
|
subst B (comp (contr.2 prf.1) (sym (contr.2 it))) prf.2;
|
|
|
|
let
|
|
indOne : (P : ⊤ -> Type) -> P () -> (x : ⊤) -> P x;
|
|
indOne P p x = subst P () p;
|
|
|
|
let
|
|
false : Type;
|
|
false = (A : Type) → A;
|
|
|
|
let
|
|
exFalso : (P : Type) -> false -> P;
|
|
exFalso P f = f P;
|
|
|
|
let
|
|
funExt : {A : Type} {B : A -> Type} {f g : (x : A) -> B x}
|
|
-> ((x : A) -> f x == g x) -> f == g;
|
|
funExt p = p;
|
|
|
|
let
|
|
hfunext : {A : Type} {B : A -> Type} {f g : (x : A) -> B x}
|
|
-> ((x : A) -> f x == g x) == (f == g);
|
|
hfunext = refl;
|
|
|
|
let
|
|
allAbsurd : {A : Type} (f g : false -> A) -> f == g;
|
|
allAbsurd f g x = exFalso (f x == g x) x;
|
|
|
|
let
|
|
coerceR1 : {A : Type}
|
|
→ Eq (A == A → A → A)
|
|
(λ p x → coe {A} {A} p x)
|
|
(λ x y → y);
|
|
coerceR1 = refl;
|
|
|
|
let
|
|
K : {A : Type} {x : A} (P : x == x → Type)
|
|
→ P refl → (p : x == x) → P p;
|
|
K P p path = subst P (the (refl == path) ()) p;
|
|
|
|
let
|
|
foo : {A : Type} {B : A -> Type} {f : (x : A) -> B x}
|
|
-> Eq (f == f) refl (λ x → refl);
|
|
foo = K (λ e → (refl {_} {f}) == e) refl (λ x → refl);
|
|
|
|
let
|
|
coh : {A : Type} (p : A == A) (x : A) → coe p == (λ x → x);
|
|
coh path elem x = refl;
|
|
|
|
let
|
|
coh2 : {A : Type} (p : A == A) (x : A) → coe p x == x;
|
|
coh2 path elem = K (λ path → coe {A} {A} path elem == elem) refl path;
|
|
|
|
-- let
|
|
-- cohsAgree : {A : Type} (p : A == A) (x : A) → coh {A} p x == coh2 {A} p x;
|
|
-- cohsAgree path elem = refl;
|
|
|
|
let
|
|
congComp : {A B : Type} (f : A -> B) {x : A}
|
|
-> cong f (refl {A} {x}) == refl {B} {f x};
|
|
congComp f = refl;
|
|
|
|
coe
|