129 lines
1.5 KiB
Markdown
129 lines
1.5 KiB
Markdown
|
```
|
|||
|
|
{#- OPTIONS --cubical -#}
|
|||
|
|
|
|||
|
|
----------
|
|||
|
|
|
|||
|
|
A = ℕ
|
|||
|
|
|
|||
|
|
P : A → Type
|
|||
|
|
P n = Vec n
|
|||
|
|
|
|||
|
|
_+_
|
|||
|
|
zero + y = y
|
|||
|
|
suc x + y = suc (x + y)
|
|||
|
|
|
|||
|
|
-- x and y are NOT definitionally equal
|
|||
|
|
x = 1 + 2
|
|||
|
|
y = 2 + 1
|
|||
|
|
|
|||
|
|
--
|
|||
|
|
p : x ≡ y
|
|||
|
|
p = +-comm 1 2
|
|||
|
|
|
|||
|
|
|
|||
|
|
Identity {A : Type} {x y : A}
|
|||
|
|
|
|||
|
|
elim-unit :
|
|||
|
|
(A : Type) →
|
|||
|
|
|
|||
|
|
-- unit case
|
|||
|
|
(a : Unit → A) →
|
|||
|
|
|
|||
|
|
Unit → A
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
elim-nat : (A : Type) → (z : A) → (s : A → A) → ℕ → A
|
|||
|
|
|
|||
|
|
|
|||
|
|
elim-nat A f g 5 = a5
|
|||
|
|
- a0 = f
|
|||
|
|
- a1 = g a0
|
|||
|
|
- a2 = g a1
|
|||
|
|
- a3 = g a2
|
|||
|
|
- a4 = g a3
|
|||
|
|
- a5 = g a4
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
elim-identity :
|
|||
|
|
-- type that the identity type is over
|
|||
|
|
(A : Type) →
|
|||
|
|
|
|||
|
|
-- output type
|
|||
|
|
(C : (x y : A) → (p : x ≡ y) → Type) →
|
|||
|
|
|
|||
|
|
-- refl case
|
|||
|
|
(c : (z : A) → C z z (refl z)) →
|
|||
|
|
|
|||
|
|
(a b : A) → (p′ : a ≡ b) →
|
|||
|
|
C a b p′
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
-- In the case of transports
|
|||
|
|
D is C in the eliminator
|
|||
|
|
|
|||
|
|
P : A → Type
|
|||
|
|
|
|||
|
|
D : (x y : A) → (p : x ≡ y) → Type
|
|||
|
|
D x y p = P x → P y
|
|||
|
|
|
|||
|
|
transport : (A : Type) → (P : A → Type) → (x y : A) → (p : x ≡ y) → P x → P y
|
|||
|
|
transport = elim-identity A (λ a b _ → (P a → P b)) (λ a → id) x y p
|
|||
|
|
|
|||
|
|
|
|||
|
|
elim-identity A D d (a a : A) (refl a) = d a
|
|||
|
|
|
|||
|
|
|
|||
|
|
transport A P x x (refl x)
|
|||
|
|
= elim-identity A (λ a b _ → (P a → P b)) (λ x → id) x x (refl x)
|
|||
|
|
= (λ x → id) x
|
|||
|
|
= id
|
|||
|
|
|
|||
|
|
---
|
|||
|
|
|
|||
|
|
|
|||
|
|
-- Goal:
|
|||
|
|
p* : P (1 + 2) ≡ P (2 + 1)
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
----------
|
|||
|
|
|
|||
|
|
loop ∙ loop ∙ loop : S¹
|
|||
|
|
3 : ℤ
|
|||
|
|
|
|||
|
|
p : {A : Type} {x y : A} → x ≡ y
|
|||
|
|
-- Path from P base = ℤ to P base
|
|||
|
|
|
|||
|
|
P : S¹ → Type
|
|||
|
|
P base = ℤ
|
|||
|
|
P loop = ?
|
|||
|
|
```
|
|||
|
|
|
|||
|
|
For this week:
|
|||
|
|
|
|||
|
|
- Try to understand Lemma 2.3.4 in HoTT book
|