type-theory/src/CircleFundamentalGroup.agda

{-# OPTIONS --without-K #-}

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

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} 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

-- 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
    d x = refl

-- 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

-- Groups
record Group {ℓ : Level} : Set (lsuc ℓ) where
  constructor group
  field
    set : Set ℓ
    op : 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
open Group

-- wtf
open import Data.Bool

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 ]

bruh : (a : ℤ) → a + 0ℤ ≡ a
bruh +0 = refl
bruh +[1+ n ] = refl
bruh -[1+ n ] = refl

+-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₁ ]
  ≡⟨ refl ⟩
    + n - (+ n₁)
  ≡⟨ refl ⟩
    + n + (- (+ n₁))
  ≡⟨ ? ⟩
    (+[1+ n ]) - (+[1+ n₁ ])
  ≡⟨ refl ⟩
    +[1+ n ] - +[1+ n₁ ]
  ≡⟨ refl ⟩
    -[1+ n₁ ] + +[1+ n ]
  ∎
+-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₁)

+-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 ]
--   ≡⟨ refl ⟩
--     + (ℕ.suc n) + -[1+ n ]
--   ≡⟨ refl ⟩
--     (ℕ.suc n) ⊖ (ℕ.suc n)
--   ≡⟨ ? ⟩
--     + (ℕ.suc n ℕ.∸ ℕ.suc n)
--   ≡⟨ ? ⟩
--     0ℤ
--   ∎
ℤ-identity -[1+ n ] =
    -[1+ n ] + (- -[1+ n ])
  ≡⟨ refl ⟩
    -[1+ n ] + +[1+ n ]
  ≡⟨ +-comm -[1+ n ] +[1+ n ] ⟩
    +[1+ n ] + -[1+ n ]
  ≡⟨ ? ⟩
    0ℤ
  ∎

ℤ-group : Group
ℤ-group .set = ℤ
ℤ-group .op = _+_
ℤ-group .ident = 0ℤ
ℤ-group .assoc-prop = +-assoc
ℤ-group .inverse z = - z
ℤ-group .inverse-prop-l = ℤ-identity

-- Fundamental group of a circle

loop-space : {A : Type} → (a : A) → Set
loop-space a = a ≡ a

π₁ : {A : Type} → (a : A) → Group
π₁ 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