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

-- 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}
  -- 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 : (transport C loop c-base) ≡ c-base)
    → (s : S¹) → C s

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

-- Integers
-- Not using the Agda type cus it uses with!!
data Z : Set where
  pos : ℕ → Z
  zero : Z
  neg : ℕ → Z

_+_ : 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

-_ : Z → Z
- pos x = neg x
- zero = zero
- neg x = pos x

_-_ : 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 ⟩
    suc (zero N+ suc a)
  ≡⟨ refl ⟩
    suc zero N+ suc a
  ≡⟨ +-comm 1 (suc a) ⟩
    suc a N+ suc zero
  ∎
lemma-1 (suc a) (suc b) = cong suc (lemma-1 a (suc b))

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 ⟩
--     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 ⟩
--     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)
--   ∎
-- 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) = {! !}

double-neg : (a : Z) → - (- a) ≡ a
double-neg (pos x) = refl
double-neg zero = refl
double-neg (neg x) = refl

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)

Z-inverse-r : (a : Z) → (- a) + a ≡ zero
Z-inverse-r a = trans (Z-comm (- a) a) (Z-inverse-l 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

_∙_ = trans

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