open import Cubical.Foundations.Prelude hiding (Sub)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels

module TT.Groupoid.IsoSet (X : hSet ℓ-zero) (Y : X .fst → hSet ℓ-zero) where

import TT.Groupoid.Syntax X Y as G
module S where
  open import TT.Set.Syntax X Y public
  open import TT.Set.ConPath X Y public
import TT.Groupoid.ToSet X Y as GS
import TT.Set.ToGroupoid X Y as SG
import TT.Groupoid.ToFromSet X Y as GSG
import TT.Set.ToFromGroupoid X Y as SGS

private variable
  Γ Δ : G.Con
  A : G.Ty Γ

isoCon : Iso G.Con S.Con
isoCon .Iso.fun = GS.⟦_⟧
isoCon .Iso.inv = SG.⟦_⟧
isoCon .Iso.rightInv = SGS.⟦_⟧
isoCon .Iso.leftInv = GSG.⟦_⟧

GSGS-Con : (Γ : G.Con) → cong GS.⟦_⟧ GSG.⟦ Γ ⟧ ≡ SGS.⟦ GS.⟦ Γ ⟧ ⟧
GSGS-Con Γ = S.isSetCon _ _ _ _

isoSub : Iso (G.Sub Δ Γ) (S.Sub GS.⟦ Δ ⟧ GS.⟦ Γ ⟧)
isoSub .Iso.fun = GS.⟦_⟧
isoSub {Δ} {Γ} .Iso.inv γ =
  transport (λ i → G.Sub (GSG.⟦ Δ ⟧ i) (GSG.⟦ Γ ⟧ i)) SG.⟦ γ ⟧
isoSub {Δ} {Γ} .Iso.rightInv γ i =
  comp (λ j → S.Sub (GSGS-Con Δ i j) (GSGS-Con Γ i j))
    (λ where
      j (i = i0) →
        GS.⟦
          transport-filler
            (λ i → G.Sub (GSG.⟦ Δ ⟧ i) (GSG.⟦ Γ ⟧ i))
            SG.⟦ γ ⟧
            j ⟧
      j (i = i1) → SGS.⟦ γ ⟧ j)
    GS.⟦ SG.⟦ γ ⟧ ⟧
isoSub .Iso.leftInv γ = fromPathP GSG.⟦ γ ⟧

isoTy : Iso (G.Ty Γ) (S.Ty GS.⟦ Γ ⟧)
isoTy .Iso.fun = GS.⟦_⟧
isoTy {Γ} .Iso.inv A = transport (λ i → G.Ty (GSG.⟦ Γ ⟧ i)) SG.⟦ A ⟧
isoTy {Γ} .Iso.rightInv A i =
  comp (λ j → S.Ty (GSGS-Con Γ i j))
    (λ where
      j (i = i0) → GS.⟦ transport-filler (λ i → G.Ty (GSG.⟦ Γ ⟧ i)) SG.⟦ A ⟧ j ⟧
      j (i = i1) → SGS.⟦ A ⟧ j)
    GS.⟦ SG.⟦ A ⟧ ⟧
isoTy .Iso.leftInv A = fromPathP GSG.⟦ A ⟧

isoTm : Iso (G.Tm Γ A) (S.Tm GS.⟦ Γ ⟧ GS.⟦ A ⟧)
isoTm .Iso.fun = GS.⟦_⟧
isoTm {Γ} {A} .Iso.inv a =
  transport (λ i → G.Tm (GSG.⟦ Γ ⟧ i) (GSG.⟦ A ⟧ i)) SG.⟦ a ⟧
isoTm {Γ} {A} .Iso.rightInv a i =
  comp
    (λ j →
      S.Tm
        (GSGS-Con Γ i j)
        (isSet→SquareP (λ i j → S.isSetTy (GSGS-Con Γ i j))
          (λ j → GS.⟦ GSG.⟦ A ⟧ j ⟧)
          (λ j → SGS.⟦ GS.⟦ A ⟧ ⟧ j)
          (λ i → GS.⟦ SG.⟦ GS.⟦ A ⟧ ⟧ ⟧)
          (λ i → GS.⟦ A ⟧)
          i j))
    (λ where
      j (i = i0) →
        GS.⟦
          transport-filler
            (λ i → G.Tm (GSG.⟦ Γ ⟧ i) (GSG.⟦ A ⟧ i))
            SG.⟦ a ⟧
            j ⟧
      j (i = i1) → SGS.⟦ a ⟧ j)
    GS.⟦ SG.⟦ a ⟧ ⟧
isoTm .Iso.leftInv a = fromPathP GSG.⟦ a ⟧