{-# OPTIONS --safe #-}

module Multiset.Bij.Path where

open import Multiset.Prelude
open import Multiset.Bij.Base as Bij

open import Multiset.Util.Square
  using
    ( ΣSquareP
    ; ΣSquarePProp
    )

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Path using (PathP≡doubleCompPathʳ ; fromPathP⁻)
open import Cubical.Foundations.Transport using (transport⁻)
open import Cubical.Foundations.Univalence
  using
    ( ua
    ; uaIdEquiv
    ; uaCompEquiv
    ; ua→
    ; ua→⁻
    )
open import Cubical.Foundations.Isomorphism using (Iso ; isoToEquiv)
open import Cubical.Foundations.GroupoidLaws using (cong-∙)
open import Cubical.Foundations.Function using (_∘_ ; flip ; idfun)

open import Cubical.Foundations.Structure

open import Cubical.Functions.FunExtEquiv
  using (funExtDep)

open import Cubical.Data.Sigma as Sigma
  using (Σ≡Prop ; ΣPathP ; ΣPathPProp)
open import Cubical.Data.Nat as 
  using ()
open import Cubical.Data.SumFin as Fin
  using (Fin)

hSet₀ : Type₁
hSet₀ = hSet ℓ-zero

module _ (s t : ) where
  isSetFin≃ : isSet (Fin s  Fin t)
  isSetFin≃ = isOfHLevel≃ 2 (Fin.isSetFin) (Fin.isSetFin)

  Fin≃ : hSet₀
  Fin≃ = (Fin s  Fin t) , isSetFin≃

Fin≃Path :  {s t : } (m : )  Fin s  Fin t  Fin≃ s m  Fin≃ t m
Fin≃Path {s} {t} m α = TypeOfHLevel≡ 2 path where
  path : (Fin s  Fin m)  (Fin t  Fin m)
  path = cong (_≃ Fin m) (ua α)

Fin≃PathId : (m n : )  Fin≃Path m (idEquiv (Fin n))  refl {x = Fin≃ n m}
Fin≃PathId m n = ΣSquarePProp  _  isPropΠ2  _ _  isPropIsProp)) (cong (cong (_≃ Fin m)) uaIdEquiv)

Fin≃PathComp :  {m n o : } (k : )
   (α : Fin m  Fin n)
   (β : Fin n  Fin o) 
      Fin≃Path k (α ∙ₑ β)  Fin≃Path k α  Fin≃Path k β
Fin≃PathComp k α β = ΣSquarePProp ((λ _  isPropΠ2  _ _  isPropIsProp)))
  ( cong (_≃ Fin k) (ua (α ∙ₑ β)) ≡⟨ cong (cong (_≃ Fin k)) (uaCompEquiv α β) 
    cong (_≃ Fin k) (ua α  ua β) ≡⟨ cong-∙ (_≃ Fin k) (ua α) (ua β) ⟩∎
    cong (_≃ Fin k) (ua α)  cong (_≃ Fin k) (ua β) 
  )

Code :   Bij  hSet₀
Code m = rec (isOfHLevelTypeOfHLevel 2)
  (flip Fin≃ m)
  (Fin≃Path m)
  (Fin≃PathId m)
  (Fin≃PathComp m)

isSetCode :  {m} {x}  isSet  Code m x 
isSetCode {m = m} {x} = str (Code m x)

encode : {n : }  {x : Bij}  obj n  x   Code n x 
encode {n = n} p = subst  x   Code n x ) p (idEquiv (Fin n))

encodeRefl :  {n}  encode {x = obj n} refl  idEquiv (Fin n)
encodeRefl {n = n} = substRefl {B = λ x   Code n x } {x = obj n} (idEquiv (Fin n))

decode : {m : }  (x : Bij)   Code m x   obj m  x
decode {m = m} = elimSet  _  isOfHLevelΠ 2 λ _  isSetBijPath) (obj* m) (hom* m) where
  -- NOTE: This is contravariant so that
  --    PathP (λ i → ⟨ Code m (hom α i) ⟩) β₀ β₁
  -- reduces to a path of equivalences with ua in their domain.
  -- This way, we can use `ua→` to extract a commutative
  -- triangle of equivalences (see `commutesPointwise`).
  obj* : (m n : )  Fin n  Fin m  obj m  obj n
  obj* m n α = sym (hom α)

  hom* :  {n₀ n₁ : } (m : )
     (α : Fin n₀  Fin n₁)
     PathP  j   Code m (hom α j)   obj m  hom α j) (obj* m n₀) (obj* m n₁)
  hom* {n₀ = n₀} {n₁ = n₁} m α = funExtDep goal where
    module _ {β₀ : Fin n₀  Fin m} {β₁ : Fin n₁  Fin m} (p : PathP  i   Code m (hom α i) ) β₀ β₁) where abstract

      -- From `p`, we can deduce that there is a commutative triangle of equivalences:
      --
      --            α
      --  Fin n₀ -------> Fin n₁
      --    |               |
      -- β₀ |               | β₁
      --    |               |
      --    '---> Fin m <---'
      commutesPointwise :  (k : Fin n₀)  equivFun β₀ k  equivFun β₁ (equivFun α k)
      commutesPointwise = ua→⁻ (congP  _  equivFun) p)

      commutes : β₀  α ∙ₑ β₁
      commutes = equivEq (funExt commutesPointwise)

      -- Using `comp-coh`, this lifts to `hom`s in `Bij`.
      -- NOTE: We use (_∙'_) here so that the following
      -- steps become easier.
      coh-commutes : hom β₀  hom α ∙' hom β₁
      coh-commutes =
        hom β₀                  ≡⟨ cong hom commutes 
        hom (α ∙ₑ β₁)           ≡⟨ comp-coh α β₁ 
        hom α  hom β₁          ≡⟨ compPath≡compPath' _ _ 
        hom α ∙' hom β₁         ≡⟨⟩
        hom α ∙∙ hom β₁ ∙∙ refl 

      -- The above coherence law can be translated back into
      -- a Square, as required by the goal.
      coh-sq : Square (hom β₀) (hom β₁) (hom α) (refl {x = obj m})
      coh-sq = transport (sym (PathP≡doubleCompPathʳ (hom α) (hom β₀) (hom β₁) refl)) coh-commutes

      -- Since `obj*` is defined contravariantly, the goal is
      -- `coh-sq`, but mirrored horizontally.  This way, the
      -- top and bottom of the square become
      --   (obj* _ _ βₓ) ≡ sym (hom βₓ)
      -- for βₓ ∈ { β₀, β₁ }.
      goal : Square (obj* _ _ β₀) (obj* _ _ β₁) (refl {x = obj m}) (hom α)
      goal = λ i j  coh-sq i (~ j)

decodeIdEquiv :  {n}  decode (obj n) (idEquiv (Fin n))  refl
decodeIdEquiv {n = n} =
  decode (obj n) (idEquiv (Fin n)) ≡⟨⟩
  sym (hom (idEquiv (Fin n)))      ≡⟨ cong sym (id-coh n) 
  sym refl                         ≡⟨⟩
  refl 

decode∘encodeRefl :  {n}  decode (obj n) (encode refl)  refl
decode∘encodeRefl {n = n} =
  decode (obj n) (encode refl) ≡⟨ cong (decode (obj n)) encodeRefl 
  decode (obj n) (idEquiv _)   ≡⟨ decodeIdEquiv ⟩∎
  refl 

decode∘encode :  {n} {x : Bij} (p : obj n  x)  decode x (encode p)  p
decode∘encode {n} {x = x} = elimProp {P = λ x  (p : obj n  x)  decode x (encode p)  p} propP obj* x where
  propP :  x  isProp ((p : obj n  x)  decode x (encode p)  p)
  propP x = isPropΠ  p  isGroupoidBij _ _ (decode x (encode p)) p)

  obj* :  m (p : obj n  obj m)  decode (obj m) (encode p)  p
  obj* m = J  x (p : obj n  x)  decode x (encode p)  p) decode∘encodeRefl

encode∘decodeIdEquiv :  {m}  encode (decode (obj m) (idEquiv (Fin m)))  idEquiv (Fin m)
encode∘decodeIdEquiv {m = m} =
  encode (decode (obj m) (idEquiv (Fin m))) ≡⟨ cong encode decodeIdEquiv 
  encode refl                               ≡⟨ encodeRefl ⟩∎
  idEquiv (Fin m)                           

encode∘decode :  {m} {x}
   (α :  Code m x )
   encode (decode x α)  α
encode∘decode {m = m} {x = x} = elimProp {P = λ x  (α :  Code m x )  encode (decode x α)  α} propP obj* x where
  propP :  x  isProp ((α :  Code m x )  encode (decode x α)  α)
  propP x = isPropΠ λ α  isSetCode {m = m} {x = x} (encode (decode x α)) α

  module _ (n : ) (α : Fin n  Fin m) where
    equivFunPath : PathP  j  ua α j  Fin m) (equivFun α) (idfun _)
    equivFunPath = ua→  k  refl)

    equivPath : PathP  j  ua α j  Fin m) α (idEquiv (Fin m))
    equivPath = ΣPathPProp  _  isPropIsEquiv _) equivFunPath

    transportPath : α  transport⁻  j  ua α j  Fin m) (idEquiv (Fin m))
    transportPath = fromPathP⁻ equivPath

    obj* : encode (decode (obj n) α)  α
    obj* =
      encode (decode (obj n) α)                           ≡⟨⟩
      transport⁻  j  ua α j  Fin m) (idEquiv (Fin m)) ≡⟨ sym transportPath 
      α 

BijPathFin≃Iso :  {m n}  Iso (obj m  obj n) (Fin n  Fin m)
BijPathFin≃Iso {m = m} {n = n} = iso′ where
  open Iso

  iso′ : Iso _ _
  iso′ .fun = encode
  iso′ .inv = decode {m = m} (obj n)
  iso′ .rightInv = encode∘decode {m = m} {x = obj n}
  iso′ .leftInv = decode∘encode

BijPath≃Fin≃ :  {m n}  (obj m  obj n)  (Fin n  Fin m)
BijPath≃Fin≃ = isoToEquiv BijPathFin≃Iso