module Id.Groupoid where

open import Agda.Primitive
open import Lib
open import Fam as _

open import Id.Intro
open import Id.Elim

module Id-Groupoid (C : Fam) ⦃ CId : Id-Intro C ⦄ ⦃ CId-Elim-C : Id-Elim C C ⦄
                   (_ : ⊤) where -- (_ : ⊤) forces the resolution of instance arguments
  open Id-Intro CId
  open Id-Elim CId-Elim-C

  abstract
    trans : ∀ {A} {x y z : C .Tm A} → C .Tm (Id x y) → C .Tm (Id y z) → C .Tm (Id x z)
    trans {x = x} p q = transp (λ w → Id x w) p q

    trans-β-l : ∀ {A} {y z : C .Tm A} {q : C .Tm (Id y z)} → C .Tm (Id (trans idp q) q)
    trans-β-l {q = q} = J (λ (z , q) → Id (trans idp q) q) transp-β (_ , q)

    trans-β-r : ∀ {A} {x y : C .Tm A} {p : C .Tm (Id x y)} → C .Tm (Id (trans p idp) p)
    trans-β-r = transp-β

    trans-β-triangle : ∀ {A} {x : C .Tm A} → C .Tm (Id (trans-β-l {q = idp {x = x}}) (trans-β-r))
    trans-β-triangle = J-β

  abstract
    sym : ∀ {A} {x y : C .Tm A} → C .Tm (Id x y) → C .Tm (Id y x)
    sym {x = x} {y = y} p = transp (λ z → Id z x) idp p

    sym-β : ∀ {A} {x : C .Tm A} → C .Tm (Id (sym (idp {x = x})) idp)
    sym-β = transp-β

  abstract
    sym-sym : ∀ {A} {x y : C .Tm A} (p : C .Tm (Id x y)) → C .Tm (Id (sym (sym p)) p)
    sym-sym p = J (λ (z , q) → Id (sym (sym q)) q) (trans (ap sym sym-β) sym-β) (_ , p)

  abstract
    trans-assoc : ∀ {A} {x y z w : C .Tm A} {p : C .Tm (Id x y)} {q : C .Tm (Id y z)} {r : C .Tm (Id z w)}
                → C .Tm (Id (trans p (trans q r)) (trans (trans p q) r))
    trans-assoc {A} {x} {y} {z} {w} {p} {q} {r}
      = J (λ (w , r) → Id (trans p (trans q r)) (trans (trans p q) r))
          (trans (ap (trans p) trans-β-r) (sym trans-β-r)) (_ , r)

  abstract
    trans-sym-r : ∀ {A} {x y : C .Tm A} {p : C .Tm (Id x y)} → C .Tm (Id (trans p (sym p)) idp)
    trans-sym-r {p = p} = J (λ (_ , q) → Id (trans q (sym q)) idp)
                      (trans (ap (trans _) sym-β) trans-β-r)
                             (_ , p)

    trans-sym-r-β : ∀ {A} {x : C .Tm A} → C .Tm (Id (trans-sym-r {x = x}) (trans (ap (trans _) sym-β) trans-β-r))
    trans-sym-r-β = J-β

  abstract
    trans-sym-l : ∀ {A} {x y : C .Tm A} {p : C .Tm (Id x y)} → C .Tm (Id (trans (sym p) p) idp)
    trans-sym-l {p = p} = J (λ (_ , p) → Id (trans (sym p) p) idp) (trans (ap (λ q → trans q _) sym-β) trans-β-r) (_ , p)

  abstract
    sym-trans : ∀ {A} {x y z : C .Tm A} {p : C .Tm (Id x y)} {q : C .Tm (Id y z)}
                → C .Tm (Id (sym (trans p q)) (trans (sym q) (sym p)))
    sym-trans {A} {x} {y} {z} {p} {q} =
      J (λ (_ , q) → Id (sym (trans p q)) (trans (sym q) (sym p)))
        (trans (ap sym trans-β-r) (sym (trans (ap (λ q → trans q (sym p)) sym-β) trans-β-l) )) (_ , q)

  abstract
    cong-trans : ∀ {A} {x y z : C .Tm A} {p₁ p₂ : C .Tm (Id x y)} {q₁ q₂ : C .Tm (Id y z)}
               → C .Tm (Id p₁ p₂) → C .Tm (Id q₁ q₂)
               → C .Tm (Id (trans p₁ q₁) (trans p₂ q₂))
    cong-trans {p₁ = p₁} {q₂ = q₂} α β = trans (ap (trans p₁) β) (ap (λ p → trans p q₂) α)

  abstract
    ap-id : ∀ {A} {x y : C .Tm A} {p : C .Tm (Id x y)}
          → C .Tm (Id (ap (λ x → x) p) p)
    ap-id {x = x} = J (λ (y , p) → Id (ap (λ x → x) p) p)
                    ap-β _

  abstract
    ap-id' : ∀ {A} (f : C .Tm A → C .Tm A) (h : ∀ a → C .Tm (Id (f a) a)) {x y : C .Tm A} {p : C .Tm (Id x y)}
          → C .Tm (Id (ap f p) (trans (h x) (trans p (sym (h y)))))
    ap-id' f h {x = x} = J (λ (y , p) → Id (ap f p) (trans (h x) (trans p (sym (h y)))))
                          (trans ap-β (sym (trans (ap (trans _) trans-β-l) trans-sym-r))) _

  abstract
    ap-∘ : ∀ {A B Z} (f : C .Tm A → C .Tm B) (g : C .Tm B → C .Tm Z) {x y} {p : C .Tm (Id x y)}
         → C .Tm (Id (ap (g ∘ f) p) (ap g (ap f p)))
    ap-∘ {A} {B} {Z} f g {x} {y} {p} = J (λ (y , p) → Id (ap (g ∘ f) p) (ap g (ap f p)))
                                         (trans ap-β (sym (trans (ap (ap g) ap-β) ap-β))) _

  abstract
    trans-ap : ∀ {A B} {f : C .Tm A → C .Tm B} {x y z : C .Tm A} {p : C .Tm (Id x y)} {q : C .Tm (Id y z)}
             → C .Tm (Id (trans (ap f p) (ap f q)) (ap f (trans p q)))
    trans-ap {A} {B} {f} {x} {y} {z} {p} {q} =
      J (λ (z , q) → Id (trans (ap f p) (ap f q)) (ap f (trans p q)))
        (trans (ap (trans (ap f p)) ap-β) (trans trans-β-r (sym (trans (ap (ap f) trans-β-r) idp)))) (_ , q)

  abstract
    transp-trans : ∀ {A : C .Ty} {x : C .Tm A} {P : C .Tm A → C .Ty}
                     {d : C .Tm (P x)} {y z} {p : C .Tm (Id x y)} {q : C .Tm (Id y z)}
                   → C .Tm (Id (transp P (transp P d p) q) (transp P d (trans p q)))
    transp-trans {A} {x} {P} {d} {y} {z} {p} {q} =
      J (λ (_ , q) → Id (transp P (transp P d p) q) (transp P d (trans p q)))
        (trans transp-β (sym (ap (transp P d) trans-β-r)))
        (_ , q)

  abstract
    trans-pentagon : ∀ {A} {x y : C .Tm A} (p : C .Tm (Id x y)) →
                     C .Tm (Id (trans (sym (trans-β-r)) (ap (trans p) (sym trans-sym-l)))
                            (sym (trans trans-assoc (trans (ap (λ q → trans q p) trans-sym-r) trans-β-l))))
    trans-pentagon {x = x} p = J (λ (y , p) → Id (trans (sym (trans-β-r)) (ap (trans p) (sym trans-sym-l)))
                                                 (sym (trans trans-assoc (trans (ap (λ q → trans q p) trans-sym-r) trans-β-l))))
                                 p₀ (_ , p) where
      abstract
        p₀ : C .Tm (Id (trans (sym (trans-β-r {x = x} {p = idp})) (ap (trans idp) (sym trans-sym-l)))
                    (sym (trans trans-assoc (trans (ap (λ q → trans q idp) trans-sym-r) trans-β-l))))
        p₀ = trans (ap (trans _) (trans (ap-id' _ (λ a → trans-β-l))
                  (trans (ap (λ q → trans trans-β-l (trans (sym q) (sym trans-β-l))) (trans J-β (ap (λ q → trans q trans-β-r) (ap-id' _ (λ _ → trans-β-r)))))
                  idp)))
            (sym (trans (trans sym-trans (trans (ap (trans _) (ap sym (trans J-β (ap (λ q → trans q (sym trans-β-r)) (ap-id' _ (λ _ → trans-β-l))))))
            (ap (λ q → trans (sym q) (sym (trans (trans trans-β-l (trans trans-β-r (sym trans-β-l))) (sym trans-β-r)))) (ap (λ q → trans q trans-β-l) (ap-id' _ (λ _ → trans-β-r))))))
            (trans (cong-trans (trans sym-trans (cong-trans idp (trans sym-trans (cong-trans (trans sym-trans (cong-trans (sym-sym _) (trans (ap sym trans-sym-r-β) (trans sym-trans (cong-trans idp (trans (ap sym (ap-id' _ (λ a → trans-β-l))) (trans sym-trans (cong-trans (trans sym-trans (cong-trans (sym-sym _) idp)) idp)))))))) idp)))) (trans sym-trans (cong-trans (sym-sym _) (trans sym-trans (cong-trans (trans sym-trans (cong-trans (sym-sym _) idp)) idp)))))
            (trans (trans (sym trans-assoc) (cong-trans idp (trans (sym trans-assoc) idp)))
            (trans (cong-trans (ap sym trans-β-triangle) idp)
            (ap (trans _)
            (trans (sym trans-assoc)
            (trans (cong-trans (sym trans-β-triangle) idp)
            (ap (trans _)
            (sym
            (trans (cong-trans (trans sym-trans (cong-trans idp (trans sym-trans (cong-trans (trans sym-trans (cong-trans (sym-sym _) idp)) idp)))) idp)
            (trans (sym trans-assoc)
            (sym
            (trans (sym trans-assoc)
            (ap (trans _)
            (trans (sym trans-assoc)
            (trans (sym trans-assoc)
            (sym
            (trans (sym trans-assoc)
            (trans (sym trans-assoc)
            (trans (cong-trans (sym trans-β-triangle) idp)
            (ap (trans _)
            (ap (trans _)
            (sym (trans (cong-trans idp (trans trans-assoc (trans (cong-trans trans-sym-l idp) trans-β-l)))
            (trans (trans trans-assoc (cong-trans (trans trans-assoc (trans (cong-trans trans-sym-l idp) trans-β-l)) idp))
            idp))))))))))))))))))))))))))