upd

src/CircleFundamentalGroup.agda

@@ -0,0 +1,74 @@
+{-# OPTIONS --without-K #-}
+
+module CircleFundamentalGroup where
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+  renaming (Set to Type) public
+open import Agda.Builtin.Int
+
+-- Path
+data _≡_ {l : Level} {A : Type l} : A → A → Type l where
+  refl : (x : A) → x ≡ x
+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
+
+-- Id
+id : {ℓ : Level} {A : Set ℓ} → A → A
+id x = x
+ 
+-- Transport
+transport : {X : Set} (P : X → Set) {x y : X}
+  → x ≡ y
+  → P x → P y
+transport P (refl x) = id
+
+-- 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)
+
+-- Circle (S¹)
+postulate
+  S¹ : Set
+  base : S¹
+  loop : base ≡ base
+  S¹-ind : (C : S¹ → Type)
+    → (c-base : C base)
+    → (c-loop : c-base ≡ c-base)
+    → (s : S¹) → C s
+
+-- Fundamental group of a circle
+
+loop-space : {A : Type} → (a : A) → Set
+loop-space a = a ≡ a
+
+π₁ : {A : Type} → (a : A) → Type
+π₁ a = ?
+
+π₁[S¹]≡ℤ : π₁ base ≡ Int
+π₁[S¹]≡ℤ = ?
+
+-- References:
+-- - https://homotopytypetheory.org/2011/04/29/a-formal-proof-that-pi1s1-is-z/
+-- - HoTT book ch. 6.11
+-- - https://en.wikipedia.org/wiki/Fundamental_group

src/Path2.lagda.md

@@ -100,15 +100,21 @@ 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₂ =
+  let asdf a = ap (λ b → (a , b)) p₂ in
+  let uiop = path-ind (λ x y p → (x , b₁) ≡ (y , b₂)) (λ x → asdf x) p₁ in
   ?
+
+  -- Use ap with both cases
+  -- path concatenation?
+
   where
-    D : (x y : A × B) → (p : x ≡ y) → Type
-    D x y p = ?
+    -- 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
+    -- d : (x : A × B) → D x x (refl x)
+    -- d x = refl x
 
-    asdf = path-ind D d p₁
+    -- asdf = path-ind D d p₁
 
     ap-f : {A B : Type} → A → (A → B) → B
     ap-f x f = f x
@@ -122,13 +128,19 @@ prod {A} {B} {a₁} {a₂} {b₁} {b₂} p₁ p₂ =
 
     -- (ap-f a₁) f₁ ≡ (ap-f a₁) f₂
 
+sym2 : {A : Type} {x y : A} → x ≡ y → y ≡ x
+sym2 {A} {x} {y} p = path-ind (λ x y p → y ≡ x) refl p
+
 -- 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 = ?
+lift {A} {x} {y} {P} u p =
+  -- let up = apd {B = P} (λ x → u) p in
+  --let a = prod p (sym2 up) in
+  ?
   where
     f : (a : A) → ?
 
@@ -138,19 +150,38 @@ lift-prop : {A : Type} {x y : A} {P : (x : A) → Type}
   → pr₁ (lift u p) ≡ p
 lift-prop u p = ?
 
+
+
+
+
+_≡′_ : {A : Type} {B : (x : A) → Type}
+  → {x y : A} → {p : x ≡ y}
+  → (bx : B x) → (by : B y)
+  → Type
+_≡′_ {A} {B} {x} {y} {p} bx by = (transport B p) bx ≡ by
+
+
+_≡₃_ : {A : Type} {B : (x : A) → Type}
+  → {x y : A} → {p : x ≡ y}
+  → (bx : B x) → (by : B y)
+  → Type
+_≡₃_ {A} {B} {x} {y} {p} bx by = ?
+-- path-ind (λ x y p → B y) ? ? ≡ by
+
+
+
+
+
+
+
 -- our new custom dependent Path type
 _≡₂_ : {A : Type} {B : (x : A) → Type}
+-- Should not use explicit x, y here while hiding p
   → (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)