a type theory with equality based on setoids
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 

137 lines
3.6 KiB

-- 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