{-

This file proves the higher groupoid structure of types
for homogeneous and heterogeneous paths

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.GroupoidLaws where

open import Cubical.Foundations.Prelude

private
  variable
    ℓ : Level
    A : Type ℓ
    x y z w v : A

_⁻¹ : (x ≡ y) → (y ≡ x)
x≡y ⁻¹ = sym x≡y

infix  _⁻¹

-- homogeneous groupoid laws

symInvo : (p : x ≡ y) → p ≡ p ⁻¹ ⁻¹
symInvo p = refl

rUnit : (p : x ≡ y) → p ≡ p ∙ refl
rUnit p j i = compPath-filler p refl j i

-- The filler of left unit: lUnit-filler p =
-- PathP (λ i → PathP (λ j → PathP (λ k → A) x (p (~ j ∨ i)))
-- (refl i) (λ j → compPath-filler refl p i j)) (λ k i → (p (~ k ∧ i ))) (lUnit p)

lUnit-filler : {x y : A} (p : x ≡ y) → I → I → I → A
lUnit-filler {x = x} p j k i =
  hfill (λ j → λ { (i = i0) → x
                  ; (i = i1) → p (~ k ∨ j )
                  ; (k = i0) → p i
               -- ; (k = i1) → compPath-filler refl p j i
                  }) (inS (p (~ k ∧ i ))) j

lUnit : (p : x ≡ y) → p ≡ refl ∙ p
lUnit p j i = lUnit-filler p i1 j i

symRefl : refl {x = x} ≡ refl ⁻¹
symRefl i = refl

compPathRefl : refl {x = x} ≡ refl ∙ refl
compPathRefl = rUnit refl

-- The filler of right cancellation: rCancel-filler p =
-- PathP (λ i → PathP (λ j → PathP (λ k → A) x (p (~ j ∧ ~ i)))
-- (λ j → compPath-filler p (p ⁻¹) i j) (refl i)) (λ j i → (p (i ∧ ~ j))) (rCancel p)

rCancel-filler : ∀ {x y : A} (p : x ≡ y) → (k j i : I) → A
rCancel-filler {x = x} p k j i =
  hfill (λ k → λ { (i = i0) → x
                  ; (i = i1) → p (~ k ∧ ~ j)
               -- ; (j = i0) → compPath-filler p (p ⁻¹) k i
                  ; (j = i1) → x
                  }) (inS (p (i ∧ ~ j))) k

rCancel : (p : x ≡ y) → p ∙ p ⁻¹ ≡ refl
rCancel {x = x} p j i = rCancel-filler p i1 j i

rCancel-filler' : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y) → (i j k : I) → A
rCancel-filler' {x = x} {y} p i j k =
  hfill
    (λ i → λ
      { (j = i1) → p (~ i ∧ k)
      ; (k = i0) → x
      ; (k = i1) → p (~ i)
      })
    (inS (p k))
    (~ i)

rCancel' : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y) → p ∙ p ⁻¹ ≡ refl
rCancel' p j k = rCancel-filler' p i0 j k

lCancel : (p : x ≡ y) → p ⁻¹ ∙ p ≡ refl
lCancel p = rCancel (p ⁻¹)

assoc : (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) →
  p ∙ q ∙ r ≡ (p ∙ q) ∙ r
assoc p q r k = (compPath-filler p q k) ∙ compPath-filler' q r (~ k)


-- heterogeneous groupoid laws

symInvoP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → (p : PathP A x y) →
     PathP (λ j → PathP (λ i → symInvo (λ i → A i) j i) x y) p (symP (symP p))
symInvoP p = refl

rUnitP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → (p : PathP A x y) →
  PathP (λ j → PathP (λ i → rUnit (λ i → A i) j i) x y) p (compPathP p refl)
rUnitP p j i = compPathP-filler p refl j i

lUnitP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → (p : PathP A x y) →
  PathP (λ j → PathP (λ i → lUnit (λ i → A i) j i) x y) p (compPathP refl p)
lUnitP {A = A} {x = x} p k i =
  comp (λ j → lUnit-filler (λ i → A i) j k i)
       (λ j → λ { (i = i0) → x
                ; (i = i1) → p (~ k ∨ j )
                ; (k = i0) → p i
                }) (p (~ k ∧ i ))

rCancelP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → (p : PathP A x y) →
   PathP (λ j → PathP (λ i → rCancel (λ i → A i) j i) x x) (compPathP p (symP p)) refl
rCancelP {A = A} {x = x} p j i =
  comp (λ k → rCancel-filler (λ i → A i) k j i)
       (λ k → λ { (i = i0) → x
                ; (i = i1) → p (~ k ∧ ~ j)
                ; (j = i1) → x
                }) (p (i ∧ ~ j))

lCancelP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → (p : PathP A x y) →
   PathP (λ j → PathP (λ i → lCancel (λ i → A i) j i) y y) (compPathP (symP p) p) refl
lCancelP p = rCancelP (symP p)



assocP : {A : I → Type ℓ} {x : A i0} {y : A i1} {B_i1 : Type ℓ} {B : (A i1) ≡ B_i1} {z : B i1}
  {C_i1 : Type ℓ} {C : (B i1) ≡ C_i1} {w : C i1} (p : PathP A x y) (q : PathP (λ i → B i) y z) (r : PathP (λ i → C i) z w) →
  PathP (λ j → PathP (λ i → assoc (λ i → A i) B C j i) x w) (compPathP p (compPathP q r)) (compPathP (compPathP p q) r)
assocP {A = A} {B = B} {C = C} p q r k i =
    comp (\ j' → hfill  (λ j → λ {
                     (i = i0) → A i0
                   ; (i = i1) → compPath-filler' (λ i₁ → B i₁) (λ i₁ → C i₁) (~ k) j })
                     (inS (compPath-filler (λ i₁ → A i₁) (λ i₁ → B i₁) k i)) j')
     (λ j → λ
      { (i = i0) → p i0
      ; (i = i1) →
        comp (\ j' → hfill ((λ l → λ
            { (j = i0) → B k
            ; (j = i1) → C l
            ; (k = i1) → C (j ∧ l)
            })) (inS (B ( j ∨ k)) ) j')
          (λ l → λ
            { (j = i0) → q k
            ; (j = i1) → r l
            ; (k = i1) → r (j ∧ l)
            })
          (q (j ∨ k))
      })
    (compPathP-filler p q k i)



-- Loic's code below

-- some exchange law for doubleCompPath and refl

invSides-filler : {x y z : A} (p : x ≡ y) (q : x ≡ z) → Square p (sym q) q (sym p)
invSides-filler {x = x} p q i j =
  hcomp (λ k → λ { (i = i0) → p (k ∧ j)
                 ; (i = i1) → q (~ j ∧ k)
                 ; (j = i0) → q (i ∧ k)
                 ; (j = i1) → p (~ i ∧ k)})
        x

leftright : {ℓ : Level} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z) →
            (refl ∙∙ p ∙∙ q) ≡ (p ∙∙ q ∙∙ refl)
leftright p q i j =
  hcomp (λ t → λ { (j = i0) → p (i ∧ (~ t))
                 ; (j = i1) → q (t ∨ i) })
        (invSides-filler q (sym p) (~ i) j)

-- equating doubleCompPath and a succession of two compPath

split-leftright : {ℓ : Level} {A : Type ℓ} {w x y z : A} (p : w ≡ x) (q : x ≡ y) (r : y ≡ z) →
                  (p ∙∙ q ∙∙ r) ≡ (refl ∙∙ (p ∙∙ q ∙∙ refl) ∙∙ r)
split-leftright p q r j i =
  hcomp (λ t → λ { (i = i0) → p (~ j ∧ ~ t)
                 ; (i = i1) → r t })
        (doubleCompPath-filler p q refl j i)

split-leftright' : {ℓ : Level} {A : Type ℓ} {w x y z : A} (p : w ≡ x) (q : x ≡ y) (r : y ≡ z) →
                  (p ∙∙ q ∙∙ r) ≡ (p ∙∙ (refl ∙∙ q ∙∙ r) ∙∙ refl)
split-leftright' p q r j i =
  hcomp (λ t → λ { (i = i0) → p (~ t)
                 ; (i = i1) → r (j ∨ t) })
        (doubleCompPath-filler refl q r j i)

doubleCompPath-elim : {ℓ : Level} {A : Type ℓ} {w x y z : A} (p : w ≡ x) (q : x ≡ y)
                      (r : y ≡ z) → (p ∙∙ q ∙∙ r) ≡ (p ∙ q) ∙ r
doubleCompPath-elim p q r = (split-leftright p q r) ∙ (λ i → (leftright p q (~ i)) ∙ r)

doubleCompPath-elim' : {ℓ : Level} {A : Type ℓ} {w x y z : A} (p : w ≡ x) (q : x ≡ y)
                       (r : y ≡ z) → (p ∙∙ q ∙∙ r) ≡ p ∙ (q ∙ r)
doubleCompPath-elim' p q r = (split-leftright' p q r) ∙ (sym (leftright p (q ∙ r)))

cong-∙∙ : ∀ {B : Type ℓ} (f : A → B) (p : w ≡ x) (q : x ≡ y) (r : y ≡ z)
          → cong f (p ∙∙ q ∙∙ r) ≡ (cong f p) ∙∙ (cong f q) ∙∙ (cong f r)
cong-∙∙ f p q r j i = hcomp (λ k → λ { (j = i0) → f (doubleCompPath-filler p q r k i)
                                     ; (i = i0) → f (p (~ k))
                                     ; (i = i1) → f (r k) })
                            (f (q i))

cong-∙ : ∀ {B : Type ℓ} (f : A → B) (p : x ≡ y) (q : y ≡ z)
         → cong f (p ∙ q) ≡ (cong f p) ∙ (cong f q)
cong-∙ f p q = cong-∙∙ f refl p q

hcomp-unique : ∀ {ℓ} {A : Type ℓ} {φ} → (u : I → Partial φ A) → (u0 : A [ φ ↦ u i0 ]) →
               (h2 : ∀ i → A [ (φ ∨ ~ i) ↦ (\ { (φ = i1) → u i 1=1; (i = i0) → outS u0}) ])
               → (hcomp u (outS u0) ≡ outS (h2 i1)) [ φ ↦ (\ { (φ = i1) → (\ i → u i1 1=1)}) ]
hcomp-unique {φ = φ} u u0 h2 = inS (\ i → hcomp (\ k → \ { (φ = i1) → u k 1=1
                                                            ; (i = i1) → outS (h2 k) })
                                                   (outS u0))


lid-unique : ∀ {ℓ} {A : Type ℓ} {φ} → (u : I → Partial φ A) → (u0 : A [ φ ↦ u i0 ]) →
               (h1 h2 : ∀ i → A [ (φ ∨ ~ i) ↦ (\ { (φ = i1) → u i 1=1; (i = i0) → outS u0}) ])
               → (outS (h1 i1) ≡ outS (h2 i1)) [ φ ↦ (\ { (φ = i1) → (\ i → u i1 1=1)}) ]
lid-unique {φ = φ} u u0 h1 h2 = inS (\ i → hcomp (\ k → \ { (φ = i1) → u k 1=1
                                                            ; (i = i0) → outS (h1 k)
                                                            ; (i = i1) → outS (h2 k) })
                                                   (outS u0))


transp-hcomp : ∀ {ℓ} (φ : I) {A' : Type ℓ}
                     (A : (i : I) → Type ℓ [ φ ↦ (λ _ → A') ]) (let B = \ (i : I) → outS (A i))
                 → ∀ {ψ} (u : I → Partial ψ (B i0)) → (u0 : B i0 [ ψ ↦ u i0 ]) →
                 (transp (\ i → B i) φ (hcomp u (outS u0)) ≡ hcomp (\ i o → transp (\ i → B i) φ (u i o)) (transp (\ i → B i) φ (outS u0)))
                   [ ψ ↦ (\ { (ψ = i1) → (\ i → transp (\ i → B i) φ (u i1 1=1))}) ]
transp-hcomp φ A u u0 = inS (sym (outS (hcomp-unique
               ((\ i o → transp (\ i → B i) φ (u i o))) (inS (transp (\ i → B i) φ (outS u0)))
                 \ i → inS (transp (\ i → B i) φ (hfill u u0 i)))))
  where
    B = \ (i : I) → outS (A i)


hcomp-cong : ∀ {ℓ} {A : Type ℓ} {φ} → (u : I → Partial φ A) → (u0 : A [ φ ↦ u i0 ]) →
                                     (u' : I → Partial φ A) → (u0' : A [ φ ↦ u' i0 ]) →
             (ueq : ∀ i → PartialP φ (\ o → u i o ≡ u' i o)) → (outS u0 ≡ outS u0') [ φ ↦ (\ { (φ = i1) → ueq i0 1=1}) ]
             → (hcomp u (outS u0) ≡ hcomp u' (outS u0')) [ φ ↦ (\ { (φ = i1) → ueq i1 1=1 }) ]
hcomp-cong u u0 u' u0' ueq 0eq = inS (\ j → hcomp (\ i o → ueq i o j) (outS 0eq j))

congFunct-filler : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {x y z : A} (f : A → B) (p : x ≡ y) (q : y ≡ z)
                → I → I → I → B
congFunct-filler {x = x} f p q i j z =
  hfill (λ k → λ { (i = i0) → f x
                 ; (i = i1) → f (q k)
                 ; (j = i0) → f (compPath-filler p q k i)})
       (inS (f (p i)))
       z

congFunct : ∀ {ℓ} {B : Type ℓ} (f : A → B) (p : x ≡ y) (q : y ≡ z) → cong f (p ∙ q) ≡ cong f p ∙ cong f q
congFunct f p q j i = congFunct-filler f p q i j i1


-- congFunct for dependent types
congFunct-dep : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {x y z : A} (f : (a : A) → B a) (p : x ≡ y) (q : y ≡ z)
         → PathP (λ i → PathP (λ j → B (compPath-filler p q i j)) (f x) (f (q i))) (cong f p) (cong f (p ∙ q))
congFunct-dep {B = B} {x = x} f p q i j = f (compPath-filler p q i j)

cong₂Funct : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} {B : Type ℓ'} (f : A → A → B) →
        (p : x ≡ y) →
        {u v : A} (q : u ≡ v) →
        cong₂ f p q ≡ cong (λ x → f x u) p ∙ cong (f y) q
cong₂Funct {x = x} {y = y} f p {u = u} {v = v} q j i =
  hcomp (λ k → λ { (i = i0) → f x u
                  ; (i = i1) → f y (q k)
                  ; (j = i0) → f (p i) (q (i ∧ k))})
       (f (p i) u)

symDistr-filler : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z) → I → I → I → A
symDistr-filler {A = A} {z = z} p q i j k =
  hfill (λ k → λ { (i = i0) → q (k ∨ j)
                 ; (i = i1) → p (~ k ∧ j) })
       (inS (invSides-filler q (sym p) i j))
       k

symDistr : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z) → sym (p ∙ q) ≡ sym q ∙ sym p
symDistr p q i j = symDistr-filler p q j i i1

-- we can not write hcomp-isEquiv : {ϕ : I} → (p : I → Partial ϕ A) → isEquiv (λ (a : A [ ϕ ↦ p i0 ]) → hcomp p a)
-- due to size issues. But what we can write (compare to hfill) is:
hcomp-equivFillerSub : {ϕ : I} → (p : I → Partial ϕ A) → (a : A [ ϕ ↦ p i0 ])
                     → (i : I)
                     → A [ ϕ ∨ i ∨ ~ i ↦ (λ { (i = i0) → outS a
                                            ; (i = i1) → hcomp (λ i → p (~ i)) (hcomp p (outS a))
                                            ; (ϕ = i1) → p i0 1=1 }) ]
hcomp-equivFillerSub {ϕ = ϕ} p a i =
  inS (hcomp (λ k → λ { (i = i1) → hfill (λ j → p (~ j)) (inS (hcomp p (outS a))) k
                      ; (i = i0) → outS a
                      ; (ϕ = i1) → p (~ k ∧ i) 1=1 })
             (hfill p a i))

hcomp-equivFiller : {ϕ : I} → (p : I → Partial ϕ A) → (a : A [ ϕ ↦ p i0 ])
                  → (i : I) → A
hcomp-equivFiller p a i = outS (hcomp-equivFillerSub p a i)


pentagonIdentity : (p : x ≡ y) → (q : y ≡ z) → (r : z ≡ w) → (s : w ≡ v)
                      →
            (assoc p q (r ∙ s) ∙ assoc (p ∙ q) r s)
                              ≡
   cong (p ∙_) (assoc q r s) ∙∙ assoc p (q ∙ r) s ∙∙ cong (_∙ s) (assoc p q r)

pentagonIdentity {x = x} {y} p q r s =
        (λ i →
              (λ j → cong (p ∙_) (assoc q r s) (i ∧ j))
           ∙∙ (λ j → lemma₀₀ i j ∙ lemma₀₁ i j)
           ∙∙ (λ j → lemma₁₀ i j ∙ lemma₁₁ i j)
        )
   where


    lemma₀₀ : ( i j : I) → _ ≡ _
    lemma₀₀ i j i₁ =
         hcomp
        (λ k → λ { (j = i0) → p i₁
                 ; (i₁ = i0) → x
                 ; (i₁ = i1) → hcomp
                                 (λ k₁ → λ { (i = i0) → (q (j ∧ k))
                                           ; (k = i0) → y
                                           ; (j = i0) → y
                                           ; (j = i1)(k = i1) → r (k₁ ∧ i)})
                                 (q (j ∧ k))
        }) (p i₁)

    lemma₀₁ : ( i j : I) → hcomp
                       (λ k → λ {(i = i0) → q j
                               ; (j = i0) → y
                               ; (j = i1) → r (k ∧ i)
                          })
                       (q j) ≡ _
    lemma₀₁ i j i₁ = (hcomp
                        (λ k → λ { (j = i1) → hcomp
                                                (λ k₁ → λ { (i₁ = i0) → r i
                                                          ; (k = i0) → r i
                                                          ; (i = i1) → s (k₁ ∧  k ∧  i₁)
                                                          ; (i₁ = i1)(k = i1) → s k₁ })
                                                (r ((i₁ ∧ k) ∨ i))
                                  ; (i₁ = i0) → compPath-filler q r i j
                                  ; (i₁ = i1) → hcomp
                                                  (λ k₁ → λ { (k = i0) → r i
                                                            ; (k = i1) → s k₁
                                                            ; (i = i1) → s (k ∧ k₁)})
                                                  (r (i ∨ k))})
                         (hfill
                             (λ k → λ { (j = i1) → r k
                                      ; (i₁ = i1) → r k
                                      ; (i₁ = i0)(j = i0) → y })
                             (inS (q (i₁ ∨ j))) i))

    lemma₁₁ : ( i j : I) → (r (i ∨ j)) ≡ _
    lemma₁₁ i j i₁ =
           hcomp
             (λ k → λ { (i = i1) → s (i₁ ∧ k)
                      ; (j = i1) → s (i₁ ∧ k)
                      ; (i₁ = i0) → r (i ∨ j)
                      ; (i₁ = i1) → s k
              }) (r (i ∨ j ∨ i₁))


    lemma₁₀-back :  I → I → I → _
    lemma₁₀-back i j i₁ =
        hcomp
         (λ k → λ {
           (i₁ = i0) → x
         ; (i₁ = i1) → hcomp
                         (λ k₁ → λ { (k = i0) → q (j ∨ ~ i)
                                   ; (k = i1) → r (k₁ ∧ j)
                                   ; (j = i0) → q (k ∨ ~ i)
                                   ; (j = i1) → r (k₁ ∧ k)
                                   ; (i = i0) → r (k ∧ j ∧ k₁)
                         })
                         (q (k ∨ j ∨ ~ i))
         ; (i = i0)(j = i0) → (p ∙ q) i₁
         })
        (hcomp
           (λ k → λ { (i₁ = i0) → x
                    ; (i₁ = i1) → q ((j ∨ ~ i ) ∧ k)
                    ; (j = i0)(i = i1) → p i₁
            })
            (p i₁))


    lemma₁₀-front : I → I → I → _
    lemma₁₀-front i j i₁ =
       (((λ _ → x) ∙∙ compPath-filler p q j ∙∙
         (λ i₁ →
             hcomp
                (λ k → λ { (i₁ = i0) → q j
                         ; (i₁ = i1) → r (k ∧ (j ∨ i))
                         ; (j = i0)(i = i0) → q i₁
                         ; (j = i1) → r (i₁ ∧ k)
               })
            (q (j ∨ i₁))
         )) i₁)

    compPath-filler-in-filler :
                (p : _ ≡ y) → (q : _ ≡ _ )
              → _≡_ {A = Square (p ∙ q) (p ∙ q) (λ _ → x) (λ _ → z)}
               (λ i j → hcomp
                          (λ i₂ →
                           λ { (j = i0) → x
                             ; (j = i1) → q (i₂ ∨ ~ i)
                             ; (i = i0) → (p ∙ q) j
                            })
                          (compPath-filler p q (~ i) j))
               (λ _ → p ∙ q)
    compPath-filler-in-filler p q z i j =
       hcomp
         (λ k → λ {
            (j = i0) → p i0
          ; (j = i1) → q (k ∨ ~ i ∧ ~ z)
          ; (i = i0) → hcomp
                       (λ i₂ → λ {
                         (j = i0) → p i0
                        ;(j = i1) → q ((k ∨  ~ z) ∧ i₂)
                        ;(z = i1) (k = i0) → p j
                       })
                      (p j)
          ; (i = i1) →  compPath-filler p (λ i₁ → q (k ∧ i₁)) k j
          ; (z = i0) → hfill
                         ((λ i₂ → λ { (j = i0) → p i0
                             ; (j = i1) → q (i₂ ∨ ~ i)
                             ; (i = i0) → (p ∙ q) j
                            }))
                         (inS ((compPath-filler p q (~ i) j))) k
          ; (z = i1) → compPath-filler p q k j
         })
         (compPath-filler p q (~ i ∧ ~ z) j)


    cube-comp₋₀₋ :
        (c : I → I → I → A)
      → {a' : Square _ _ _ _}
      → (λ i i₁ → c i i0 i₁) ≡ a'
      → (I → I → I → A)
    cube-comp₋₀₋ c p i j k =
       hcomp
         (λ l → λ {
            (i = i0) → c i0 j k
           ;(i = i1) → c i1 j k
           ;(j = i0) → p l i k
           ;(j = i1) → c i i1 k
           ;(k = i0) → c i j i0
           ;(k = i1) → c i j i1
          })
        (c i j k)

    cube-comp₀₋₋ :
        (c : I → I → I → A)
      → {a' : Square _ _ _ _}
      → (λ i i₁ → c i0 i i₁) ≡ a'
      → (I → I → I → A)
    cube-comp₀₋₋ c p i j k =
       hcomp
         (λ l → λ {
            (i = i0) → p l j k
           ;(i = i1) → c i1 j k
           ;(j = i0) → c i i0 k
           ;(j = i1) → c i i1 k
           ;(k = i0) → c i j i0
           ;(k = i1) → c i j i1
          })
        (c i j k)



    lemma₁₀-back' : _
    lemma₁₀-back' k j i₁ =
       (cube-comp₋₀₋ (lemma₁₀-back)
         (compPath-filler-in-filler p q)) k j i₁


    lemma₁₀ : ( i j : I) → _ ≡ _
    lemma₁₀ i j i₁ =
        (cube-comp₀₋₋ lemma₁₀-front (sym lemma₁₀-back')) i j i₁