path2

2023-03-22 00:31:28 -05:00 · 2023-03-22 00:31:28 -05:00 · d79909bfd6
commit d79909bfd6
parent 3e8ffa187b
1 changed files with 160 additions and 0 deletions
--- a/src/Path2.lagda.md
+++ b/src/Path2.lagda.md
@ -0,0 +1,160 @@
+Path2
+===
+
+```
+{-# OPTIONS --without-K --rewriting #-}
+
+module Path2 where
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) renaming (Set to Type) public
+open import Function.Equivalence hiding (id)
+open import Data.Product
+
+-- Path
+data _≡_ {ℓ : Level} {A : Type ℓ} : A → A → Type ℓ where
+  refl : (x : A) → x ≡ x
+
+-- Id
+id : {ℓ : Level} {A : Set ℓ} → A → A
+id x = x
+
+-- Path induction
+path-ind : ∀ {ℓ : Level} {A : Type}
+  -- Motive
+  → (C : (x y : A) → x ≡ y → Type ℓ)
+  -- What happens in the case of refl
+  → (c : (x : A) → C x x (refl x))
+  -- Actual path to eliminate
+  → {x y : A} → (p : x ≡ y)
+  -- Result
+  → C x y p
+path-ind C c {x} (refl x) = c x
+
+-- Transport
+transport : {X : Set} (P : X → Set) {x y : X}
+  → x ≡ y
+  → P x → P y
+transport P (refl x) = id
+
+-- ap
+-- Chapter 2.2 of HoTT book
+ap : {A B : Type}
+  -- The function that we want to apply
+  → (f : A → B)
+  -- The path to apply it over
+  → {x y : A} → x ≡ y
+  -- Result
+  → f x ≡ f y
+ap {A} f p = path-ind D d p
+  where
+    D : (x y : A) → (p : x ≡ y) → Type
+    D x y p = f x ≡ f y
+
+    d : (x : A) → D x x (refl x)
+    d x = refl (f x)
+
+-- apd
+-- Lemma 2.3.4 of HoTT book
+apd : {A : Type} {B : A → Type}
+  -- The function that we want to apply
+  → (f : (a : A) → B a)
+  -- The path to apply it over
+  → {x y : A} → (p : x ≡ y)
+  -- Result
+  → (transport B p) (f x) ≡ f y
+apd {A} {B} f p = path-ind D d p
+  where
+    D : (x y : A) → (p : x ≡ y) → Type
+    D x y p = (transport B p) (f x) ≡ f y
+
+    d : (x : A) → D x x (refl x)
+    d x = refl (f x)
+```
+
+```
+-- Path products
+pr₁ : {A B : Type} {a₁ a₂ : A} {b₁ b₂ : B}
+  → (p : (a₁ , b₁) ≡ (a₂ , b₂))
+  → a₁ ≡ a₂
+pr₁ {A} {B} p = ap proj₁ p
+
+pr₂ : {A B : Type} {a₁ a₂ : A} {b₁ b₂ : B}
+  → (p : (a₁ , b₁) ≡ (a₂ , b₂))
+  → b₁ ≡ b₂
+pr₂ {A} {B} p = ap proj₂ p
+
+uniq : {A B : Type}
+  → (x : A × B)
+  → (proj₁ x , proj₂ x) ≡ x
+uniq x = refl x
+
+prod : {A B : Type} {a₁ a₂ : A} {b₁ b₂ : B}
+  → (p₁ : a₁ ≡ a₂) → (p₂ : b₁ ≡ b₂)
+  → (a₁ , b₁) ≡ (a₂ , b₂)
+prod {A} {B} {a₁} {a₂} {b₁} {b₂} p₁ p₂ =
+  ?
+  where
+    D : (x y : A × B) → (p : x ≡ y) → Type
+    D x y p = ?
+
+    d : (x : A × B) → D x x (refl x)
+    d x = refl x
+
+    asdf = path-ind D d p₁
+
+    ap-f : {A B : Type} → A → (A → B) → B
+    ap-f x f = f x
+
+    f : A → B → A × B
+    f a b = (a , b)
+
+    -- f a : B → A × B
+    -- p₂ : b₁ ≡ b₂
+    -- ap (f a) p₂
+
+    -- (ap-f a₁) f₁ ≡ (ap-f a₁) f₂
+
+-- Path lifting
+-- Lemma 2.3.2 of HoTT book
+lift : {A : Type} {x y : A} {P : A → Type}
+  → (u : P x)
+  → (p : x ≡ y)
+  → (x , u) ≡ (y , (transport P p) u)
+lift {A} {x} {y} {P} u p = ?
+  where
+    f : (a : A) → ?
+
+lift-prop : {A : Type} {x y : A} {P : (x : A) → Type}
+  → (u : P x)
+  → (p : x ≡ y)
+  → pr₁ (lift u p) ≡ p
+lift-prop u p = ?
+
+-- our new custom dependent Path type
+_≡₂_ : {A : Type} {B : (x : A) → Type}
+  → (x y : A) → {p : x ≡ y}
+  → {f : (x : A) → B x}
+  → Type
+_≡₂_ {A} {B} x y {p} {f} = (transport B p) (f x) ≡ f y
+
+-- our new custom dependent Path type (without transport!)
+_≡₃_ : {A : Type} {B : (x : A) → Type}
+  → (x y : A) → {p : x ≡ y}
+  → {f : (x : A) → B x}
+  → Type
+
+apd₂ : {A : Type} {B : (x : A) → Type}
+  -- The function that we want to apply
+  → (f : (x : A) → B x)
+  -- The path to apply it over
+  → {x y : A} → (p : x ≡ y)
+  -- Result
+  → x ≡₂ y
+apd₂ {A} {B} f p = path-ind D d p
+  where
+    D : (x y : A) → (p : x ≡ y) → Type
+    D x y p = (transport B p) (f x) ≡ f y
+
+    d : (x : A) → D x x (refl x)
+    d x = refl (f x)
+```