Kubus

basiclib/basic.ktt

Paths: reflexivity, symmetry, concatenation, transport, J, function extensionality.

22 declarations, all certified by the kernel · source

1-- Basic path algebra
2
3✓def id {A : U} (x : A) : A := x
4
5✓def refl {A : U} (a : A) : Path A a a := \i -> a
6
7✓def sym {A : U} {a b : A} (p : Path A a b) : Path A b a := \i -> p (~i)
8
9✓def cong {A B : U} (f : A -> B) {a b : A} (p : Path A a b) : Path B (f a) (f b) :=
10 \i -> f (p i)
12✓def funext {A B : U} {f g : A -> B} (h : (x : A) -> Path B (f x) (g x)) : Path (A -> B) f g :=
13 \i x -> h x i
15✓def trans {A : U} {a b c : A} (p : Path A a b) (q : Path A b c) : Path A a c :=
16 \i -> hcomp j A [i = 0 -> a, i = 1 -> q j] (p i)
18✓def transport {A B : U} (p : Path U A B) (a : A) : B := comp i (p i) [] a
20✓def symInv {A : U} {a b : A} (p : Path A a b) : Path (Path A a b) (sym (sym p)) p :=
21 \i -> p
23-- contractibility of singletons
24✓def singl {A : U} (a : A) : U := (x : A) × Path A a x
26✓def contrSingl {A : U} {a b : A} (p : Path A a b) : Path (singl a) (a, refl a) (b, p) :=
27 \i -> (p i, \j -> p (i /\ j))
29✓def J {A : U} {a : A} (C : (x : A) -> Path A a x -> U) (d : C a (refl a)) {x : A} (p : Path A a x) : C x p :=
30 transport (\i -> C (contrSingl p i).1 (contrSingl p i).2) d
33✓data Empty : U
35✓def absurd {A : U} : Empty -> A
37✓data Unit : U := tt
39-- transport along refl is the identity, up to a path
40✓def transportRefl {A : U} (x : A) : Path A (transport (\i -> A) x) x :=
41 \i -> comp j A [i = 1 -> x] x
43✓def JRefl {A : U} {a : A} (C : (x : A) -> Path A a x -> U) (d : C a (refl a))
44 : Path (C a (refl a)) (J C d (refl a)) d :=
47-- the right unit law for path composition
48✓def rUnit {A : U} {a b : A} (p : Path A a b) : Path (Path A a b) p (trans p (refl b)) :=
49 \j i -> hcomp k A [i = 0 -> a, i = 1 -> b, j = 0 -> p i] (p i)
51✓def lUnit {A : U} {a b : A} (p : Path A a b) : Path (Path A a b) p (trans (refl a) p) :=
52 \j i -> hcomp k A [i = 0 -> a, i = 1 -> p k, j = 0 -> p (i /\ k)] a
54✓def isProp (A : U) : U := (x y : A) -> Path A x y
55✓def isSet (A : U) : U := (x y : A) -> isProp (Path A x y)
57-- paths in Σ-types
58✓def sigmaPath {A : U} {B : A -> U} {u v : (x : A) × B x}
59 (p : Path A u.1 v.1) (q : PathP (\i -> B (p i)) u.2 v.2) : Path ((x : A) × B x) u v :=
60 \i -> (p i, q i)
62-- dependent function extensionality
63✓def funextDep {A : U} {B : A -> U} {f g : (x : A) -> B x} (h : (x : A) -> Path (B x) (f x) (g x))
64 : Path ((x : A) -> B x) f g :=
65 \i x -> h x i