module Cubical.Categories.Isomorphism where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism using (isoFunInjective)
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Function
open import Cubical.Categories.Category
open import Cubical.Categories.Functor.Base

private
  variable
    ℓC ℓC' ℓD ℓD' : Level


module _ {C : Category ℓC ℓC'} where

  open Category C
  open isIso


  invIso : {x y : ob} → CatIso C x y → CatIso C y x
  invIso f .fst = f .snd .inv
  invIso f .snd .inv = f .fst
  invIso f .snd .sec = f .snd .ret
  invIso f .snd .ret = f .snd .sec

  invIsoIdem : {x y : ob} → (f : CatIso C x y) → invIso (invIso f) ≡ f
  invIsoIdem f = refl


  ⋆Iso : {x y z : ob} → (f : CatIso C x y)(g : CatIso C y z) → CatIso C x z
  ⋆Iso f g .fst = f .fst ⋆ g .fst
  ⋆Iso f g .snd .inv = g .snd .inv ⋆ f .snd .inv
  ⋆Iso f g .snd .sec = sym (⋆Assoc _ _ _)
    ∙ (λ i → ⋆Assoc (g .snd .inv) (f .snd .inv) (f .fst) i ⋆ g .fst)
    ∙ (λ i → (g .snd .inv ⋆ f .snd .sec i) ⋆ g .fst)
    ∙ (λ i → ⋆IdR (g .snd .inv) i ⋆ g .fst)
    ∙ g .snd .sec
  ⋆Iso f g .snd .ret = sym (⋆Assoc _ _ _)
    ∙ (λ i → ⋆Assoc (f .fst) (g .fst) (g .snd .inv) i ⋆ f .snd .inv)
    ∙ (λ i → (f .fst ⋆ g .snd .ret i) ⋆ f .snd .inv)
    ∙ (λ i → ⋆IdR (f .fst) i ⋆ f .snd .inv)
    ∙ f .snd .ret

  compIso : {x y z : ob} → (g : CatIso C y z)(f : CatIso C x y) → CatIso C x z
  compIso g f = ⋆Iso f g


  ⋆IsoIdL : {x y : ob} → (f : CatIso C x y) → ⋆Iso idCatIso f ≡ f
  ⋆IsoIdL _ = CatIso≡ _ _ (⋆IdL _)

  ⋆IsoIdR : {x y : ob} → (f : CatIso C x y) → ⋆Iso f idCatIso ≡ f
  ⋆IsoIdR _ = CatIso≡ _ _ (⋆IdR _)

  ⋆IsoInvRev : {x y z : ob} → (f : CatIso C x y)(g : CatIso C y z) → invIso (⋆Iso f g) ≡ ⋆Iso (invIso g) (invIso f)
  ⋆IsoInvRev _ _ = refl


  pathToIso-∙ : {x y z : ob}(p : x ≡ y)(q : y ≡ z) → pathToIso (p ∙ q) ≡ ⋆Iso (pathToIso p) (pathToIso q)
  pathToIso-∙ p q = J2 (λ y p z q → pathToIso (p ∙ q) ≡ ⋆Iso (pathToIso p) (pathToIso q)) pathToIso-∙-refl p q
    where
    pathToIso-∙-refl : {x : ob} → pathToIso {x = x} (refl ∙ refl) ≡ ⋆Iso (pathToIso refl) (pathToIso refl)
    pathToIso-∙-refl = cong pathToIso (sym compPathRefl)
      ∙ sym (⋆IsoIdL _)
      ∙ (λ i → ⋆Iso (pathToIso-refl (~ i)) (pathToIso refl))


  transportPathToIso : {x y z : ob}(f : C [ x , y ])(p : y ≡ z) → PathP (λ i → C [ x , p i ]) f (f ⋆ pathToIso {C = C} p .fst)
  transportPathToIso {x = x} f = J (λ _ p → PathP (λ i → C [ x , p i ]) f (f ⋆ pathToIso {C = C} p .fst))
    (sym (⋆IdR _) ∙ cong (λ x → f ⋆ x) (sym (cong fst (pathToIso-refl {C = C}))))


  pathToIso-Comm : {x y z w : ob}
    → (p : x ≡ y)(q : z ≡ w)
    → (f : Hom[ x , z ])(g : Hom[ y , w ])
    → PathP (λ i → Hom[ p i , q i ]) f g
    → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} p .fst ⋆ g
  pathToIso-Comm {x = x} {z = z} p q =
    J2 (λ y p w q →
        (f : Hom[ x , z ])(g : Hom[ y , w ])
      → PathP (λ i → Hom[ p i , q i ]) f g
      → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} p .fst ⋆ g)
    sqr-refl p q
    where
    sqr-refl : (f g : Hom[ x , z ]) → f ≡ g
      → f ⋆ pathToIso {C = C} refl .fst ≡ pathToIso {C = C} refl .fst ⋆ g
    sqr-refl f g p = (λ i → f ⋆ pathToIso-refl {C = C} i .fst)
      ∙ ⋆IdR _ ∙ p ∙ sym (⋆IdL _)
      ∙ (λ i → pathToIso-refl {C = C} (~ i) .fst ⋆ g)

  pathToIso-Square : {x y z w : ob}
    → (p : x ≡ y)(q : z ≡ w)
    → (f : Hom[ x , z ])(g : Hom[ y , w ])
    → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} p .fst ⋆ g
    → PathP (λ i → Hom[ p i , q i ]) f g
  pathToIso-Square {x = x} {z = z} p q =
    J2 (λ y p w q →
        (f : Hom[ x , z ])(g : Hom[ y , w ])
      → f ⋆ pathToIso {C = C} q .fst ≡ pathToIso {C = C} p .fst ⋆ g
      → PathP (λ i → Hom[ p i , q i ]) f g)
    sqr-refl p q
    where
    sqr-refl : (f g : Hom[ x , z ])
      → f ⋆ pathToIso {C = C} refl .fst ≡ pathToIso {C = C} refl .fst ⋆ g
      → f ≡ g
    sqr-refl f g p = sym (⋆IdR _)
      ∙ (λ i → f ⋆ pathToIso-refl {C = C} (~ i) .fst)
      ∙ p
      ∙ (λ i → pathToIso-refl {C = C} i .fst ⋆ g)
      ∙ ⋆IdL _

  module _ (isUnivC : isUnivalent C) where
    open isUnivalent isUnivC


    transportIsoToPath : {x y z : ob}(f : C [ x , y ])(p : CatIso C y z)
      → PathP (λ i → C [ x , CatIsoToPath p i ]) f (f ⋆ p .fst)
    transportIsoToPath f p i =
      hcomp (λ j → λ
        { (i = i0) → f
        ; (i = i1) → f ⋆ secEq (univEquiv _ _) p j .fst })
      (transportPathToIso f (CatIsoToPath p) i)

    transportIsoToPathIso : {x y z : ob}(f : CatIso C x y)(p : CatIso C y z)
      → PathP (λ i → CatIso C x (CatIsoToPath p i)) f (⋆Iso f p)
    transportIsoToPathIso f p i .fst = transportIsoToPath (f .fst) p i
    transportIsoToPathIso f p i .snd =
      isProp→PathP (λ i → isPropIsIso (transportIsoToPath (f .fst) p i)) (f .snd) (⋆Iso f p .snd) i


    isoToPath-Square : {x y z w : ob}
      → (p : CatIso C x y)(q : CatIso C z w)
      → (f : Hom[ x , z ])(g : Hom[ y , w ])
      → f ⋆ q .fst ≡ p .fst ⋆ g
      → PathP (λ i → Hom[ CatIsoToPath p i , CatIsoToPath q i ]) f g
    isoToPath-Square p q f g comm =
      pathToIso-Square (CatIsoToPath p) (CatIsoToPath q) _ _
        ((λ i → f ⋆ secEq (univEquiv _ _) q i .fst) ∙ comm ∙ (λ i → secEq (univEquiv _ _) p (~ i) .fst ⋆ g))


module _ {C : Category ℓC ℓC'} where

  open Category C
  open isIso

  ⋆InvLMove : {x y z : ob}
    (f : CatIso C x y)
    {g : Hom[ y , z ]}{h : Hom[ x , z ]}
    → f .fst ⋆ g ≡ h
    → g ≡ f .snd .inv ⋆ h
  ⋆InvLMove f {g = g} p =
      sym (⋆IdL _)
    ∙ (λ i → f .snd .sec (~ i) ⋆ g)
    ∙ ⋆Assoc _ _ _
    ∙ (λ i → f .snd .inv ⋆ p i)

  ⋆InvRMove : {x y z : ob}
    (f : CatIso C y z)
    {g : Hom[ x , y ]}{h : Hom[ x , z ]}
    → g ⋆ f .fst ≡ h
    → g ≡ h ⋆ f .snd .inv
  ⋆InvRMove f {g = g} p =
      sym (⋆IdR _)
    ∙ (λ i → g ⋆ f .snd .ret (~ i))
    ∙ sym (⋆Assoc _ _ _)
    ∙ (λ i → p i ⋆ f .snd .inv)

  ⋆CancelL : {x y z : ob}
    (f : CatIso C x y){g h : Hom[ y , z ]}
    → f .fst ⋆ g ≡ f .fst ⋆ h
    → g ≡ h
  ⋆CancelL f {g = g} {h = h} p =
      sym (⋆IdL _)
    ∙ (λ i → f .snd .sec (~ i) ⋆ g)
    ∙ ⋆Assoc _ _ _
    ∙ (λ i → f .snd .inv ⋆ p i)
    ∙ sym (⋆Assoc _ _ _)
    ∙ (λ i → f .snd .sec i ⋆ h)
    ∙ ⋆IdL _

  ⋆CancelR : {x y z : ob}
    (f : CatIso C y z){g h : Hom[ x , y ]}
    → g ⋆ f .fst ≡ h ⋆ f .fst
    → g ≡ h
  ⋆CancelR f {g = g} {h = h} p =
      sym (⋆IdR _)
    ∙ (λ i → g ⋆ f .snd .ret (~ i))
    ∙ sym (⋆Assoc _ _ _)
    ∙ (λ i → p i ⋆ f .snd .inv)
    ∙ ⋆Assoc _ _ _
    ∙ (λ i → h ⋆ f .snd .ret i)
    ∙ ⋆IdR _


module _ {C : Category ℓC ℓC'} where

  open Category
  open isIso

  op-Iso : {x y : C .ob} → CatIso C x y → CatIso (C ^op) x y
  op-Iso f .fst = f .snd .inv
  op-Iso f .snd .inv = f .fst
  op-Iso f .snd .sec = f .snd .sec
  op-Iso f .snd .ret = f .snd .ret

  op-Iso⁻ : {x y : C .ob} → CatIso (C ^op) x y → CatIso C x y
  op-Iso⁻ f .fst = f .snd .inv
  op-Iso⁻ f .snd .inv = f .fst
  op-Iso⁻ f .snd .sec = f .snd .sec
  op-Iso⁻ f .snd .ret = f .snd .ret

module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}{F : Functor C D} where

  open Category hiding (_∘_)
  open isIso
  open Functor


  F-PresIsIso : {x y : C .ob}{f : C [ x , y ]} → isIso C f → isIso D (F .F-hom f)
  F-PresIsIso f .inv = F . F-hom (f .inv)
  F-PresIsIso f .sec = sym (F .F-seq (f .inv) _) ∙ cong (F .F-hom) (f .sec) ∙ F .F-id
  F-PresIsIso f .ret = sym (F .F-seq _ (f .inv)) ∙ cong (F .F-hom) (f .ret) ∙ F .F-id


  F-Iso : {x y : C .ob} → CatIso C x y → CatIso D (F .F-ob x) (F .F-ob y)
  F-Iso f .fst = F . F-hom (f .fst)
  F-Iso f .snd = F-PresIsIso (f .snd)

  F-Iso-PresId : {x : C .ob} → F-Iso (idCatIso {x = x}) ≡ idCatIso
  F-Iso-PresId = CatIso≡ _ _ (F .F-id)

  F-Iso-Pres⋆ : {x y z : C .ob} → (f : CatIso C x y)(g : CatIso C y z) → F-Iso (⋆Iso f g) ≡ ⋆Iso (F-Iso f) (F-Iso g)
  F-Iso-Pres⋆ _ _ = CatIso≡ _ _ (F .F-seq _ _)


  F-pathToIso : {x y : C .ob} → (p : x ≡ y) → F-Iso (pathToIso p) ≡ pathToIso (cong (F .F-ob) p)
  F-pathToIso p = J (λ y p → F-Iso (pathToIso p) ≡ pathToIso (cong (F .F-ob) p)) F-pathToIso-refl p
    where
    F-pathToIso-refl : {x : C .ob} → F-Iso (pathToIso {x = x} refl) ≡ pathToIso (cong (F .F-ob) refl)
    F-pathToIso-refl = cong F-Iso pathToIso-refl
      ∙ F-Iso-PresId
      ∙ sym pathToIso-refl

  F-pathToIso-∘ : {x y : C .ob} → F-Iso ∘ pathToIso {x = x} {y = y} ≡ pathToIso ∘ cong (F .F-ob)
  F-pathToIso-∘ i p = F-pathToIso p i

module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}
  (isUnivC : isUnivalent C) (isUnivD : isUnivalent D)
  (F : Functor C D)
  where
    open isUnivalent
    open Category
    open Functor
    private
      isoToPathC = CatIsoToPath isUnivC
      isoToPathD = CatIsoToPath isUnivD

    F-isoToPath : {x y : C .ob} → (f : CatIso C x y) →
      isoToPathD (F-Iso {F = F} f) ≡ cong (F .F-ob) (isoToPathC f)
    F-isoToPath f = isoFunInjective (equivToIso (univEquiv isUnivD _ _)) _ _
      ( secEq (univEquiv isUnivD _ _) _
      ∙ sym (sym (F-pathToIso {F = F} (isoToPathC f))
      ∙ cong (F-Iso {F = F}) (secEq (univEquiv isUnivC _ _) f)))