-
Notifications
You must be signed in to change notification settings - Fork 1
/
primitives.txt
74 lines (59 loc) · 2.13 KB
/
primitives.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
_=_ : Π {α : U}, α → α → U
idp : Π {α : U} (a : α), a = a
_⁻¹ : Π {α : U} {a b : α}, a = b → b = a
_⬝_ : Π {α : U} {a b c : α}, a = b → b = c → a = c
(p ⬝ q) ⬝ r ~> p ⬝ (q ⬝ r)
(p ⬝ q)⁻¹ ~> q⁻¹ ⬝ p⁻¹
p ⬝ (p⁻¹ ⬝ q) ~> q
p⁻¹ ⬝ (p ⬝ q) ~> q
p ⬝ p⁻¹ ~> idp a
p⁻¹ ⬝ p ~> idp b
(p⁻¹)⁻¹ ~> p
(idp x)⁻¹ ~> idp x
p ⬝ idp b ~> p
idp a ⬝ p ~> p
coe : Π {A B : U} : A = B → A → B
apd : Π {A : U} {B : A → U} {a b : A} (f : Π (x : A), B x) (p : a = b), coe (apd B p) (f a) = f b
cong f p⁻¹ ~> (cong f p)⁻¹
cong f (p ⬝ q) ~> cong f p ⬝ cong f q
cong g (cong f p) ~> cong (g ∘ f) p
cong id p ~> p
cong (λ _, x) p ~> idp x
cong f (idp x) ~> idp (f x)
N : U
zero : N
succ : N → N
N-ind : Π (A : N → V), A zero → (Π n, A n → A (succ n)) → Π n, A n
N-ind A z s zero ~> z
N-ind A z s (succ n) ~> s n (N-ind A z s n)
Z : U
pos : N → Z
neg : N → Z
Z-ind : Π (A : Z → V), (Π n, A (pos n)) → (Π n, A (neg n)) → Π z, A z
Z-ind A p n (pos x) ~> p x
Z-ind A p n (neg x) ~> n x
Z-succ : Z → Z
Z-pred : Z → Z
Z-succ (neg (succ n)) ~> neg n
Z-succ (neg zero) ~> pos zero
Z-succ (pos n) ~> pos (succ n)
Z-pred (neg n) ~> neg (succ n)
Z-pred (pos zero) ~> neg zero
Z-pred (pos (succ n)) ~> pos n
Z-succ (Z-pred z) ~> z
Z-pred (Z-succ z) ~> z
S¹ : U
base : S¹
loop : Path S¹ base base
S¹-ind : Π (A : S¹ → U) (b : A base), Path (A base) (coe (cong A loop) b) b → Π (x : S¹), A x
S¹-ind A b ℓ base ~> b
???
cong (λ x, S¹-ind A b ℓ x) loop ~> ℓ[x/base] ⬝ cong (λ x′ H′, b[x/x′]) loop
R : U
elem : Z → R
glue : Π (z : Z), Path R (elem z) (elem (Z-succ z))
R-ind : Π (A : R → U) (cz : Π z, A (elem z)), (Π z, Path (A (elem (Z-succ z))) (coe (cong A (glue z)) (cz z)) (cz (Z-succ z))) → Π z, A z
R-inj : Π (x y : Z), Id R (elem x) (elem y) → Id Z x y
R-ind A cz sz (elem z) ~> cz z
cong (λ x H, R-ind A cz sz) (glue z) ~> sz z
R-inj x x (refl (elem x)) ~> refl x