commit

cubical-playground.agda-lib

@@ -1,2 +1,2 @@
 include: src
-depend: standard-library cubical
+depend: standard-library cubical agda-unimath

src/2023-04-03-more-ch2.agda

@@ -0,0 +1,159 @@
+-- {{{
+
+open import Agda.Builtin.Equality
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) renaming (Set to Type)
+open import Data.Nat
+
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
+open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
+
+-- 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)
+  -- Actual path to eliminate
+  → (x y : A) → (p : x ≡ y)
+  -- Result
+  → C x y p
+path-ind C c x x refl = 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 = id
+
+transportconst : {A : Type} {x y : A}
+  → (B : Set)
+  → (p : x ≡ y)
+  → (b : B)
+  → transport (λ _ → B) p b ≡ b
+transportconst {A} {x} {y} B p b =
+  let
+    P : (x : A) → Type
+    P = λ _ → B
+
+    D : (x y : A) → (p : x ≡ y) → Type
+    D x y p = transport P p b ≡ b
+
+    d : (x : A) → D x x refl
+    d x = refl
+  in path-ind D d x y p
+
+ap : {A B : Type} → (f : A → B) → {x y : A} → (p : x ≡ y) → f x ≡ f y
+ap f {x} {y} p = path-ind (λ a b a≡b → f a ≡ f b) (λ _ → refl) x y p
+
+-- 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 {x} {y} p = 
+  let
+    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
+    d x = refl
+  in
+  path-ind D d x y p
+
+-- }}}
+
+-------------------------------------------------------------------------------
+-- Exercises
+
+lemma-212 : {A : Type} → Type
+lemma-212 {A} = (x y z : A) → (x ≡ y) → (y ≡ z) → (x ≡ z)
+
+-- Exercise 2.1: Show that the obvious proofs of Lemma 2.1.2 are pairwise equal
+
+l212-obv-proof-1 : {A : Type} → lemma-212
+l212-obv-proof-1 {A} x y z p q =
+  let
+    f = path-ind
+      (λ a b a≡b → (z : A) → (r : b ≡ z) → a ≡ z)
+      (λ a → (λ x r → r))
+    r = f x y p
+  in
+  r z q
+
+l212-obv-proof-2 : {A : Type} → lemma-212
+l212-obv-proof-2 {A} x y z p q =
+  let
+    f = path-ind
+      (λ a b a≡b → (x : A) → (r : x ≡ a) → x ≡ b)
+      (λ a → (λ x r → r))
+    r = f y z q
+  in
+  r x p
+
+l212-obv-proof-3 : {A : Type} → lemma-212
+l212-obv-proof-3 {A} x y z p q =
+  let
+    f : (y z : A) → (q : y ≡ z) → (x : A) → x ≡ y → x ≡ z
+    f = ?
+    r = f y z q
+
+    g : (x y : A) → (p : x ≡ y) → (x ≡ z)
+    g = path-ind
+      (λ a b a≡b → a ≡ z)
+      (λ a → r a ?)
+    s = g x y p
+  in
+  ?
+
+-- Exercise 2.3: Give a fourth, different proof of Lemma 2.1.2, and prove it
+-- equal to the others
+
+l212-obv-proof-4 : {A : Type} → lemma-212
+l212-obv-proof-4 {A} x y z p q =
+  let
+    f = path-ind
+      (λ a b a≡b → (x : A) → (r : x ≡ a) → x ≡ b)
+      (λ a → (λ x r → r))
+    r = f y z q
+  in
+  r x p
+
+-- Exercise 2.4: Define, by induction on n, a general notion of n-dimensional
+-- path in a type A, simultaneously with the type of boundaries of such paths
+
+data nPath {A : Type} : ℕ → Type where
+  zeroPath : (x y : A) → (p : x ≡ y) → nPath zero
+  sucPath : {n : ℕ} → (nPath n)
+
+-- Exercise 2.5: Prove that the functions (2.3.6) and (2.3.7) are
+-- inverse-equivalences
+
+
+-- TODO: In this implementation, should r be used in constructing the response?
+-- it feels like i'm doing it wrong because r is not used
+f236 : {A B : Type} {x y : A} {p : x ≡ y} {f : A → B}
+  → (r : f x ≡ f y) → (transport (λ _ → B) p (f x)) ≡ f y
+f236 {p = p} {f = f} _ = apd f p
+
+f237 : {A B : Type} {x y : A} {p : x ≡ y} {f : A → B}
+  → (r : (transport (λ _ → B) p (f x)) ≡ f y) → (f x ≡ f y)
+f237 {p = p} {f = f} _ = ap f p
+
+-- Exercise 2.6: Prove that if p : x = y, then the function (p ∙ –) : (y = z) →
+-- (x = z) is an equivalence.
+
+e26 : {A : Type} {x y : A} → (p : x ≡ y) → ?
+
+-- Exercise 2.9. Prove that coproducts have the expected universal property,
+-- (A + B → X) ≃ (A → X) × (B → X).

src/CircleFundamentalGroup.agda

@@ -3,12 +3,11 @@
 module CircleFundamentalGroup where
 
 open import Agda.Builtin.Equality
-open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-  renaming (Set to Type) public
-open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
-open import Data.Nat.Properties renaming (+-comm to ℕ+-comm; +-assoc to ℕ+-assoc)
-open import Data.Integer hiding (_+_)
--- open import Data.Integer.Properties
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) renaming (Set to Type)
+open import Data.Nat renaming (_+_ to _N+_)
+open import Data.Nat.Properties
+import Data.Integer
+import Data.Integer.Properties
 
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
@@ -38,6 +37,9 @@ transport : {X : Set} (P : X → Set) {x y : X}
   → P x → P y
 transport P refl = id
 
+-- Univalence
+-- ua : {ℓ : Level} {A B : Set ℓ} → (equiv A B) → (A ≡ B)
+
 -- apd
 -- Lemma 2.3.4 of HoTT book
 apd : {A : Type} {B : A → Type}
@@ -62,7 +64,7 @@ postulate
   loop : base ≡ base
   S¹-ind : (C : S¹ → Type)
     → (c-base : C base)
-    → (c-loop : c-base ≡ c-base)
+    → (c-loop : (transport C loop c-base) ≡ c-base)
     → (s : S¹) → C s
 
 -- Groups
@@ -70,115 +72,152 @@ record Group {ℓ : Level} : Set (lsuc ℓ) where
   constructor group
   field
     set : Set ℓ
-    op : set → set → set
+    _∘_ : set → set → set
     ident : set
-    assoc-prop : (a b c : set) → op (op a b) c ≡ op a (op b c)
-    inverse : set → set
-    inverse-prop-l : (a : set) → op a (inverse a) ≡ ident
-    inverse-prop-r : (a : set) → op (inverse a) a ≡ ident
+    G-_ : set → set
+    assoc-prop : (a b c : set) → (a ∘ b) ∘ c ≡ a ∘ (b ∘ c)
+    inverse-prop-l : (a : set) → a ∘ (G- a) ≡ ident
+    inverse-prop-r : (a : set) → (G- a) ∘ a ≡ ident
 open Group
 
--- wtf
-open import Data.Bool
+-- Integers
+-- Not using the Agda type cus it uses with!!
+data Z : Set where
+  pos : ℕ → Z
+  zero : Z
+  neg : ℕ → Z
 
-infixl 6 _+_
-_+_ : ℤ → ℤ → ℤ
-+ 0 + b = b
-+[1+ n ] + +0 = +[1+ n ]
-+[1+ n ] + +[1+ n₁ ] = +[1+ n ℕ+ n₁ ℕ+ 1 ]
-+[1+ n ] + -[1+ n₁ ] = + n - (+ n₁)
--[1+ n ] + + n₁ = + n₁ - +[1+ n ]
--[1+ n ] + -[1+ n₁ ] = -[1+ n ℕ+ n₁ ℕ+ 1 ]
+_+_ : Z → Z → Z
+pos x + pos y = pos (suc (x N+ y))
+pos x + zero = pos x
+pos zero + neg zero = zero
+pos zero + neg (suc y) = neg y
+pos (suc x) + neg zero = pos x
+pos (suc x) + neg (suc y) = pos x + neg y
+zero + b = b
+neg x + zero = neg x
+neg x + neg y = neg (suc (x N+ y))
+neg zero + pos zero = zero
+neg zero + pos (suc y) = pos y
+neg (suc x) + pos zero = neg x
+neg (suc x) + pos (suc y) = neg x + pos y
 
-bruh : (a : ℤ) → a + 0ℤ ≡ a
-bruh +0 = refl
-bruh +[1+ n ] = refl
-bruh -[1+ n ] = refl
+-_ : Z → Z
+- pos x = neg x
+- zero = zero
+- neg x = pos x
 
-+-comm : (a b : ℤ) → a + b ≡ b + a
-+-comm a +0 = bruh a
-+-comm +[1+ n ] +[1+ n₁ ] = cong (λ n → +[1+ n ℕ+ 1 ]) (ℕ+-comm n n₁)
-+-comm +[1+ n ] -[1+ n₁ ] =
-    +[1+ n ] + -[1+ n₁ ]
+_-_ : Z → Z → Z
+a - b = a + (- b)
+
+Z-comm : (a b : Z) → a + b ≡ b + a
+Z-comm (pos a) (pos b) = cong (λ x → pos (suc x)) (+-comm a b)
+Z-comm (pos a) zero = refl
+Z-comm (pos zero) (neg zero) = refl
+Z-comm (pos zero) (neg (suc b)) = refl
+Z-comm (pos (suc a)) (neg zero) = refl
+Z-comm (pos (suc a)) (neg (suc b)) = Z-comm (pos a) (neg b)
+Z-comm zero (pos b) = refl
+Z-comm zero zero = refl
+Z-comm zero (neg b) = refl
+Z-comm (neg a) zero = refl
+Z-comm (neg a) (neg b) = cong (λ x → neg (suc x)) (+-comm a b)
+Z-comm (neg zero) (pos zero) = refl
+Z-comm (neg zero) (pos (suc b)) = refl
+Z-comm (neg (suc a)) (pos zero) = refl
+Z-comm (neg (suc a)) (pos (suc b)) = Z-comm (neg a) (pos b)
+
+-- _+_ : Nat → Nat → Nat
+-- zero  + m = m
+-- suc n + m = suc (n + m)
+lemma-1 : (a b : ℕ) → suc (a N+ b) ≡ a N+ suc b
+lemma-1 zero zero = refl
+lemma-1 zero (suc b) = refl
+lemma-1 (suc a) zero =
+    suc (suc a N+ zero)
+  ≡⟨ cong suc (+-comm (suc a) zero) ⟩
+    suc (suc a)
   ≡⟨ refl ⟩
-    + n - (+ n₁)
+    suc (zero N+ suc a)
   ≡⟨ refl ⟩
-    + n + (- (+ n₁))
-  ≡⟨ ? ⟩
-    (+[1+ n ]) - (+[1+ n₁ ])
-  ≡⟨ refl ⟩
-    +[1+ n ] - +[1+ n₁ ]
-  ≡⟨ refl ⟩
-    -[1+ n₁ ] + +[1+ n ]
+    suc zero N+ suc a
+  ≡⟨ +-comm 1 (suc a) ⟩
+    suc a N+ suc zero
   ∎
-+-comm +0 +[1+ n ] = refl
-+-comm +0 -[1+ n ] = refl
-+-comm -[1+ n ] +[1+ n₁ ] = {! !}
-+-comm -[1+ n ] -[1+ n₁ ] = cong (λ n → -[1+ n ℕ+ 1 ]) (ℕ+-comm n n₁)
+lemma-1 (suc a) (suc b) = cong suc (lemma-1 a (suc b))
 
-+-assoc : (a b c : ℤ) → (a + b) + c ≡ a + (b + c)
-
-helper : ℕ → ℕ → Bool → ℤ
-helper m n true  = - + (n ℕ.∸ m)
-helper m n false = + (m ℕ.∸ n)
-
-_⊖2_ : ℕ → ℕ → ℤ
-m ⊖2 n = helper m n (m ℕ.<ᵇ n)
-
-wtf : (n : ℕ) → n ⊖2 n ≡ 0ℤ
-wtf 0 = refl
-wtf (ℕ.suc n) =
-    (ℕ.suc n) ⊖2 (ℕ.suc n)
-  ≡⟨ cong (helper (ℕ.suc n) (ℕ.suc n)) ? ⟩
-    + (ℕ.suc n ℕ.∸ ℕ.suc n)
-  ≡⟨ ? ⟩
-    0ℤ
-  ∎
-
--- ℤ-Group
-ℤ-identity : (z : ℤ) → z + (- z) ≡ 0ℤ
--- ℤ-identity (+_ 0) = refl
--- ℤ-identity +[1+ n ] =
---     +[1+ n ] + -[1+ n ]
+postulate
+  Z-assoc : (a b c : Z) → (a + b) + c ≡ a + (b + c)
+-- TODO: Actually formalize this (it's definitely true tho)
+-- Z-assoc (pos zero) (pos zero) (pos c) = refl
+-- Z-assoc (pos zero) (pos (suc b)) (pos c) = refl
+-- Z-assoc (pos (suc a)) (pos zero) (pos c) =
+--     (pos (suc a) + pos zero) + pos c
 --   ≡⟨ refl ⟩
---     + (ℕ.suc n) + -[1+ n ]
+--     pos (suc (suc a N+ zero)) + pos c
+--   ≡⟨ cong (λ x → pos (suc (suc x)) + pos c) (+-comm a zero) ⟩
+--     pos (suc (zero N+ suc a)) + pos c
 --   ≡⟨ refl ⟩
---     (ℕ.suc n) ⊖ (ℕ.suc n)
---   ≡⟨ ? ⟩
---     + (ℕ.suc n ℕ.∸ ℕ.suc n)
---   ≡⟨ ? ⟩
---     0ℤ
+--     pos (suc (suc (zero N+ suc a)) N+ c)
+--   ≡⟨ cong (λ x → pos (suc (suc x))) (lemma-1 a c) ⟩
+--     pos (suc (suc a N+ suc c))
+--   ≡⟨ refl ⟩
+--     pos (suc a) + pos (suc c)
+--   ≡⟨ refl ⟩
+--     pos (suc a) + (pos (suc (zero N+ c)))
+--   ≡⟨ refl ⟩
+--     pos (suc a) + (pos zero + pos c)
 --   ∎
-ℤ-identity -[1+ n ] =
-    -[1+ n ] + (- -[1+ n ])
-  ≡⟨ refl ⟩
-    -[1+ n ] + +[1+ n ]
-  ≡⟨ +-comm -[1+ n ] +[1+ n ] ⟩
-    +[1+ n ] + -[1+ n ]
-  ≡⟨ ? ⟩
-    0ℤ
-  ∎
+-- Z-assoc (pos (suc a)) (pos (suc b)) (pos c) = ?
+-- Z-assoc (pos a) (pos b) zero = refl
+-- Z-assoc (pos a) (pos b) (neg c) = {! !}
+-- Z-assoc (pos a) zero c = refl
+-- Z-assoc (pos a) (neg b) (pos c) = {! !}
+-- Z-assoc (pos a) (neg b) zero = {! !}
+-- Z-assoc (pos a) (neg b) (neg c) = {! !}
+-- Z-assoc zero b c = refl
+-- Z-assoc (neg a) (pos b) (pos c) = {! !}
+-- Z-assoc (neg a) (pos b) zero = {! !}
+-- Z-assoc (neg a) (pos b) (neg c) = {! !}
+-- Z-assoc (neg a) zero c = refl
+-- Z-assoc (neg a) (neg b) (pos c) = {! !}
+-- Z-assoc (neg a) (neg b) zero = {! !}
+-- Z-assoc (neg a) (neg b) (neg c) = {! !}
 
-ℤ-group : Group
-ℤ-group .set = ℤ
-ℤ-group .op = _+_
-ℤ-group .ident = 0ℤ
-ℤ-group .assoc-prop = +-assoc
-ℤ-group .inverse z = - z
-ℤ-group .inverse-prop-l = ℤ-identity
+double-neg : (a : Z) → - (- a) ≡ a
+double-neg (pos x) = refl
+double-neg zero = refl
+double-neg (neg x) = refl
 
--- Fundamental group of a circle
+Z-inverse-l : (a : Z) → a + (- a) ≡ zero
+Z-inverse-l (pos zero) = refl
+Z-inverse-l (pos (suc a)) = Z-inverse-l (pos a)
+Z-inverse-l zero = refl
+Z-inverse-l (neg zero) = refl
+Z-inverse-l (neg (suc a)) = Z-inverse-l (neg a)
 
-loop-space : {A : Type} → (a : A) → Set
-loop-space a = a ≡ a
+Z-inverse-r : (a : Z) → (- a) + a ≡ zero
+Z-inverse-r a = trans (Z-comm (- a) a) (Z-inverse-l a)
 
-π₁ : {A : Type} → (a : A) → Group
-π₁ a = ?
+Z-group : Group
+Z-group .set = Z
+Z-group ._∘_ = _+_
+Z-group .ident = zero
+Z-group .G-_ = -_
+Z-group .assoc-prop = Z-assoc
+Z-group .inverse-prop-l = Z-inverse-l
+Z-group .inverse-prop-r = Z-inverse-r
 
--- π₁[S¹]≡ℤ : π₁ base ≡ Int
--- π₁[S¹]≡ℤ = ?
+_∙_ = trans
 
--- 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
+asdf : (z : Z) → base ≡ base
+asdf (pos zero) = loop
+asdf (pos (suc x)) = loop ∙ asdf (pos x)
+asdf zero = refl
+asdf (neg zero) = sym loop
+asdf (neg (suc x)) = (sym loop) ∙ asdf (neg x)
+
+uiop : base ≡ base → Z
+uiop = path-ind (λ x y p → Z) ?
+
+transported-function : base ≡ base

src/CircleThing2.agda

@@ -0,0 +1,34 @@
+{-# OPTIONS --without-K #-}
+
+module CircleThing2 where
+
+open import Agda.Primitive renaming (Set to Type)
+
+open import elementary-number-theory.integers
+open import elementary-number-theory.natural-numbers
+open import foundation-core.identity-types
+open import foundation.univalence
+open import synthetic-homotopy-theory.circle
+
+infix 10 _≡_
+_≡_ = _＝_
+
+loops-to-ℤ : base-𝕊¹ ≡ base-𝕊¹ → ℤ
+loops-to-ℤ p = ?
+
+ℤ-to-loops : ℤ → base-𝕊¹ ≡ base-𝕊¹
+ℤ-to-loops = ind-ℤ
+    (λ _ → base-𝕊¹ ≡ base-𝕊¹)
+    (inv loop-𝕊¹)
+    neg-ver
+    refl
+    (loop-𝕊¹)
+    pos-ver
+  where
+    pos-ver : ℕ → base-𝕊¹ ≡ base-𝕊¹ → base-𝕊¹ ≡ base-𝕊¹
+    pos-ver zero-ℕ p = refl
+    pos-ver (succ-ℕ n) p = loop-𝕊¹ ∙ pos-ver n p
+
+    neg-ver : ℕ → base-𝕊¹ ≡ base-𝕊¹ → base-𝕊¹ ≡ base-𝕊¹
+    neg-ver zero-ℕ p = refl
+    neg-ver (succ-ℕ n) p = (inv loop-𝕊¹) ∙ neg-ver n p