type-theory/src/2022-10-03-notes.lagda.md

129 lines
1.5 KiB
Markdown
Raw Normal View History

2022-10-10 20:39:12 +00:00
```
2022-10-13 06:53:13 +00:00
{-# OPTIONS --cubical #-}
2022-10-10 20:39:12 +00:00
----------
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