module Abelian where -- identity types that never use K -- homotopically, Id M N is thought of as a path from M to N -- we also use M ≃ N and Paths M N as notation for Id M N module Paths where data Id {A : Set} : A -> A -> Set where Refl : {a : A} -> Id a a _≃_ : {A : Set} -> A -> A -> Set _≃_ = Id Paths : {A : Set} -> A -> A -> Set Paths = Id jay : {A : Set} (C : (x y : A) -> Id x y -> Set) -> {M N : A} -> (P : Id M N) -> ((x : A) -> C x x Refl) -> C M N P jay _ Refl b = b _ subst : {A : Set} (p : A -> Set) {x y : A} -> Id x y -> p x -> p y subst C p = jay (λ x y _ → C x → C y) p (λ x → λ x' → x') resp : {A C : Set} {M N : A} (f : A -> C) -> Id M N -> Id (f M) (f N) resp {A}{C}{M}{N} f a = subst (\ x -> Id (f M) (f x)) a Refl resp2 : ∀ {A B C} {M N : A} {M' N' : B} (f : A -> B -> C) -> Id M N -> Id M' N' -> Id (f M M') (f N N') resp2 {A}{B}{C}{M}{N}{M'}{N'} f a b = subst (\ x -> Id (f M M') (f x N')) a (subst (λ x → Id (f M M') (f M x)) b Refl) trans : {A : Set} {M N P : A} -> Id M N -> Id N P -> Id M P trans {A}{M}{N}{P} a b = subst (\ x -> Id M x) b a sym : {a : Set} {x y : a} -> Id x y -> Id y x sym p = jay (λ x y _ → Id y x) p (λ _ → Refl) trans-unit-l : {A : Set} {M N : A} -> (p : Id M N) -> Id (trans Refl p) p trans-unit-l p = jay (λ _ _ p' → Id (trans Refl p') p') p (λ _ → Refl) trans-unit-r : {A : Set} {M N : A} -> (p : Id M N) -> Id (trans p Refl) p trans-unit-r p = Refl resptrans : {A : Set} {x y z : A} {p q : Id x y} {p' q' : Id y z} -> Id p q -> Id p' q' -> Id (trans p p') (trans q q') resptrans a b = resp2 trans a b resptrans-unit-r : {A : Set} {x y : A} {p q : Id x y} -> (a : Id p q) -> Id (resptrans a (Refl{_}{Refl})) a -- definitional equalities work out such that this works unadjusted resptrans-unit-r a = jay (λ _ _ p → Id (resptrans p (Refl {_} {Refl})) p) a (λ _ → Refl) resptrans-unit-l : {A : Set} {x y : A} {p q : Id x y} -> (a : Id p q) -> Id (resptrans (Refl{_}{Refl}) a) ( (trans (trans-unit-l p) (trans a (sym (trans-unit-l q)))) ) -- definitional equalities work out such that you need an adjustment on the right resptrans-unit-l a = jay {_} (λ p' q' a' → Id (resp (trans Refl) a') (trans (trans-unit-l p') (trans a' (sym (trans-unit-l q'))))) {_} {_} a (λ x → jay (λ xend _ x' → Id Refl (subst (Id (subst (Id xend) x' Refl)) (subst (Id x') (jay (λ x0 y _ → Id y x0) (jay (λ _ _ p' → Id (subst (Id _) p' Refl) p') x' (λ _ → Refl)) (λ _ → Refl)) Refl) (jay (λ _ _ p' → Id (subst (Id _) p' Refl) p') x' (λ _ → Refl)))) x (λ _ → Refl)) -- would be a one-liner using pattern matching -- nothing about the interchange law depends on talking about loops trans-resptrans-ichange : {A : Set} {x y z : A} (p q : Id x y) -> (a : Id p q) (r : Id x y) (b : Id q r) (p' q' : Id y z) (c : Id p' q') (r' : Id y z) (d : Id q' r') -> Id (resptrans (trans a b) (trans c d)) (trans (resptrans a c) (resptrans b d)) trans-resptrans-ichange {A}{x}{y}{z} p q a = jay (λ p' q' a' → (r : Id x y) (b : Id q' r) (p0 q0 : Id y z) (c : Id p0 q0) (r' : Id y z) (d : Id q0 r') → Id (resptrans (trans a' b) (trans c d)) (trans (resptrans a' c) (resptrans b d))) a (λ pq r b → jay (λ pq' r' b' → (p' q' : Id y z) (c : Id p' q') (r0 : Id y z) (d : Id q' r0) → Id (resptrans (trans Refl b') (trans c d)) (trans (resptrans Refl c) (resptrans b' d))) b (λ pqr p' q' c → jay (λ p0 q0 c' → (r' : Id y z) (d : Id q0 r') → Id (resptrans Refl (trans c' d)) (trans (resptrans Refl c') (resptrans Refl d))) c (λ p'q' r' d → jay (λ p'q0 r0 d' → Id (resptrans Refl (trans Refl d')) (trans Refl (resptrans Refl d'))) d (λ _ → Refl)))) {- more general interchange? hcomp : {Γ : Set} {Δ : Set} {θ1' θ2' : Γ -> Δ} {θ1 θ2 : Γ} -> (δ1 : Id θ1' θ2') -> (δ2 : Id θ1 θ2) -> Id (θ1' θ1) (θ2' θ2) hcomp δ1 δ2 = resp2 (λ x y → x y) δ1 δ2 ichange : {Γ : Set} {Δ : Set} {θ1' θ2' θ3' : Γ -> Δ} {θ1 θ2 θ3 : Γ} -> (δ1' : Id θ1' θ2') -> (δ1 : Id θ1 θ2) -> (δ2' : Id θ2' θ3') -> (δ2 : Id θ2 θ3) -> Id (hcomp (trans δ1' δ2') (trans δ1 δ2)) (trans (hcomp δ1' δ1) (hcomp δ2' δ2)) ichange δ1' δ1 δ2' δ2 = {!!} -} -- syntax for equality chain reasoning infix 2 _∎ infixr 2 _≃〈_〉_ _≃〈_〉_ : {A : Set} (x : A) {y z : A} → Id x y → Id y z → Id x z _ ≃〈 p1 〉 p2 = (trans p1 p2) _∎ : ∀ {A : Set} (x : A) → Id x x _∎ _ = Refl module FundamentalAbelian (A : Set) (base : A) where open Paths π1El : Set π1El = base ≃ base π2El : Set π2El = _≃_{π1El} Refl Refl _∘_ : π2El → π2El → π2El p ∘ q = trans q p _⊙_ : π2El → π2El → π2El a ⊙ b = resptrans b a ⊙-unit-l : (p : π2El) → (Refl ⊙ p) ≃ p ⊙-unit-l p = resptrans-unit-r p ⊙-unit-r : (a : π2El) → (a ⊙ Refl) ≃ a ⊙-unit-r a = trans (resptrans-unit-l a) (trans-unit-l a) -- because we know the base is Refl, the adjustment cancels interchange : (a b c d : _) → ((a ∘ b) ⊙ (c ∘ d)) ≃ ((a ⊙ c) ∘ (b ⊙ d)) interchange a b c d = trans-resptrans-ichange _ _ d _ c _ _ b _ a same : (a b : π2El) → (a ∘ b) ≃ (a ⊙ b) same a b = (( a ∘ b) ≃〈 resp (λ x → x ∘ b) (sym (⊙-unit-r a)) 〉 ((a ⊙ Refl) ∘ b) ≃〈 resp (λ x → (a ⊙ Refl) ∘ x) (sym (⊙-unit-l b)) 〉 ((a ⊙ Refl) ∘ (Refl ⊙ b)) ≃〈 sym (interchange a Refl Refl b) 〉 ((a ∘ Refl) ⊙ (Refl ∘ b)) ≃〈 resp (λ x → x ⊙ (Refl ∘ b)) (trans-unit-l a) 〉 (a ⊙ (Refl ∘ b)) ≃〈 resp (λ x → a ⊙ x) (trans-unit-r b) 〉 (a ⊙ b) ∎) abelian : (a b : π2El) → (a ∘ b) ≃ (b ∘ a) abelian a b = (a ∘ b) ≃〈 resp (λ x → x ∘ b) (sym (⊙-unit-l a)) 〉 ((Refl ⊙ a) ∘ b) ≃〈 resp (λ x → (Refl ⊙ a) ∘ x) (sym (⊙-unit-r b)) 〉 ((Refl ⊙ a) ∘ (b ⊙ Refl)) ≃〈 interchange Refl b a Refl 〉 ((Refl ∘ b) ⊙ (a ∘ Refl)) ≃〈 resp (λ x → x ⊙ (a ∘ Refl)) (trans-unit-r b) 〉 (b ⊙ (a ∘ Refl)) ≃〈 resp (λ x → b ⊙ x) (trans-unit-l a) 〉 (b ⊙ a) ≃〈 sym (same b a) 〉 (b ∘ a) ∎ {- -- for reference, this is the minimal generalization of the IH that goes through -- for proving the interchange law ichange : (p q : π1El) → (a : Id p q) (r : π1El) (b : Id q r) (p' q' : π1El) (c : Id p' q') (r' : π1El) (d : Id q' r') → Id (resptrans (trans a b) (trans c d)) (trans (resptrans a c) (resptrans b d)) ichange p q a = jay (λ p' q' a' → (r : π1El) (b : Id q' r) (p0 q0 : π1El) (c : Id p0 q0) (r' : π1El) (d : Id q0 r') → Id (resptrans (trans a' b) (trans c d)) (trans (resptrans a' c) (resptrans b d))) a (λ pq r b → jay (λ pq' r' b' → (p' q' : π1El) (c : Id p' q') (r0 : π1El) (d : Id q' r0) → Id (resptrans (trans Refl b') (trans c d)) (trans (resptrans Refl c) (resptrans b' d))) b (λ pqr p' q' c → jay (λ p0 q0 c' → (r' : π1El) (d : Id q0 r') → Id (resptrans Refl (trans c' d)) (trans (resptrans Refl c') (resptrans Refl d))) c (λ p'q' r' d → jay (λ p'q0 r0 d' → Id (resptrans Refl (trans Refl d')) (trans Refl (resptrans Refl d'))) d (λ _ → Refl)))) -} -- ENH: can you relax the restriction that the base point is identity? -- abelian' : {loop : Id base base} {a b : Id loop loop} → Id (trans a b) (trans b a)