TT.Groupoid.CwF

module TT.Groupoid.CwF where

open import Cubical.Foundations.Prelude hiding (Sub)

record Sorts : Type₁ where
  no-eta-equality
  field
    Con : Type
    Sub : Con → Con → Type
    Ty : Con → Type
    Tm : (Γ : Con) → Ty Γ → Type

module _ (sorts : Sorts) where
  open Sorts sorts

  private variable
    Γ Δ Θ Ξ : Con
    A B : Ty Γ

  record Ops : Type where
    no-eta-equality

    infixl 9 _∘_ _[_]ᵀ _[_]ᵗ
    field
      isSetSub : (Δ Γ : Con) → isSet (Sub Δ Γ)
      _∘_ : Sub Δ Γ → Sub Θ Δ → Sub Θ Γ
      assoc :
        (γ : Sub Δ Γ) (δ : Sub Θ Δ) (θ : Sub Ξ Θ) → γ ∘ (δ ∘ θ) ≡ (γ ∘ δ) ∘ θ

      id : Sub Γ Γ
      idr : (γ : Sub Δ Γ) → γ ∘ id ≡ γ
      idl : (γ : Sub Δ Γ) → id ∘ γ ≡ γ

      isGroupoidTy : (Γ : Con) → isGroupoid (Ty Γ)
      _[_]ᵀ : Ty Γ → Sub Δ Γ → Ty Δ

      []ᵀ-∘ :
        (A : Ty Γ) (γ : Sub Δ Γ) (δ : Sub Θ Δ) → A [ γ ∘ δ ]ᵀ ≡ A [ γ ]ᵀ [ δ ]ᵀ
      []ᵀ-assoc :
        (A : Ty Γ) (γ : Sub Δ Γ) (δ : Sub Θ Δ) (θ : Sub Ξ Θ) →
        Square
          (cong (A [_]ᵀ) (assoc γ δ θ))
          ([]ᵀ-∘ (A [ γ ]ᵀ) δ θ)
          ([]ᵀ-∘ A γ (δ ∘ θ))
          ([]ᵀ-∘ A (γ ∘ δ) θ ∙ cong _[ θ ]ᵀ ([]ᵀ-∘ A γ δ))

      []ᵀ-id : (A : Ty Γ) → A [ id ]ᵀ ≡ A
      []ᵀ-idl :
        (A : Ty Γ) (γ : Sub Δ Γ) →
        Square
          (cong (A [_]ᵀ) (idl γ))
          (cong _[ γ ]ᵀ ([]ᵀ-id A))
          ([]ᵀ-∘ A id γ)
          refl

      isSetTm : (Γ : Con) (A : Ty Γ) → isSet (Tm Γ A)
      _[_]ᵗ : Tm Γ A → (γ : Sub Δ Γ) → Tm Δ (A [ γ ]ᵀ)

      []ᵗ-∘ :
        (a : Tm Γ A) (γ : Sub Δ Γ) (δ : Sub Θ Δ) →
        PathP (λ i → Tm Θ ([]ᵀ-∘ A γ δ i)) (a [ γ ∘ δ ]ᵗ) (a [ γ ]ᵗ [ δ ]ᵗ)
      []ᵗ-id : (a : Tm Γ A) → PathP (λ i → Tm Γ ([]ᵀ-id A i)) (a [ id ]ᵗ) a

    field
      ◇ : Con
      ε : Sub Γ ◇
      ε-∘ : (γ : Sub Δ Γ) → ε ∘ γ ≡ ε
      ◇-η : id ≡ ε

    infixl 2 _▹_
    infixl 10 _⁺
    field
      _▹_ : (Γ : Con) → Ty Γ → Con
      p : Sub (Γ ▹ A) Γ
      q : Tm (Γ ▹ A) (A [ p ]ᵀ)

      _⁺ : (γ : Sub Δ Γ) → Sub (Δ ▹ A [ γ ]ᵀ) (Γ ▹ A)
      ⟨_⟩ : (a : Tm Γ A) → Sub Γ (Γ ▹ A)
      ⟨⟩-∘ : (a : Tm Γ A) (γ : Sub Δ Γ) → ⟨ a ⟩ ∘ γ ≡ γ ⁺ ∘ ⟨ a [ γ ]ᵗ ⟩
      ▹-η : id {Γ ▹ A} ≡ p ⁺ ∘ ⟨ q ⟩

    field
      ⁺-∘ :
        (γ : Sub Δ Γ) (δ : Sub Θ Δ) →
        PathP (λ i → Sub (Θ ▹ []ᵀ-∘ A γ δ i) (Γ ▹ A)) ((γ ∘ δ) ⁺) (γ ⁺ ∘ δ ⁺)

    []ᵀ-⁺-∘ :
      (B : Ty (Γ ▹ A)) (γ : Sub Δ Γ) (δ : Sub Θ Δ) →
      PathP (λ i → Ty (Θ ▹ []ᵀ-∘ A γ δ i))
        (B [ (γ ∘ δ) ⁺ ]ᵀ)
        (B [ γ ⁺ ]ᵀ [ δ ⁺ ]ᵀ)
    []ᵀ-⁺-∘ B γ δ = (λ j → B [ ⁺-∘ γ δ j ]ᵀ) ▷ []ᵀ-∘ B (γ ⁺) (δ ⁺)

    field
      ⁺-id : PathP (λ i → Sub (Γ ▹ []ᵀ-id A i) (Γ ▹ A)) (id ⁺) id

    []ᵀ-⁺-id :
      (B : Ty (Γ ▹ A)) → PathP (λ i → Ty (Γ ▹ []ᵀ-id A i)) (B [ id ⁺ ]ᵀ) B
    []ᵀ-⁺-id B = (λ j → B [ ⁺-id j ]ᵀ) ▷ []ᵀ-id B

    field
      p-⁺ : (γ : Sub Δ Γ) → p {A = A} ∘ γ ⁺ ≡ γ ∘ p

    []ᵀ-p-⁺ :
      (B : Ty Γ) (γ : Sub Δ Γ) → B [ p {A = A} ]ᵀ [ γ ⁺ ]ᵀ ≡ B [ γ ]ᵀ [ p ]ᵀ
    []ᵀ-p-⁺ B γ = sym ([]ᵀ-∘ B p (γ ⁺)) ∙∙ cong (B [_]ᵀ) (p-⁺ γ) ∙∙ []ᵀ-∘ B γ p

    field
      q-⁺ :
        (γ : Sub Δ Γ) →
        PathP (λ i → Tm (Δ ▹ A [ γ ]ᵀ) ([]ᵀ-p-⁺ A γ i)) (q [ γ ⁺ ]ᵗ) q

    field
      p-⟨⟩ : (a : Tm Γ A) → p ∘ ⟨ a ⟩ ≡ id

    []ᵀ-p-⟨⟩ : (B : Ty Γ) (a : Tm Γ A) → B [ p ]ᵀ [ ⟨ a ⟩ ]ᵀ ≡ B
    []ᵀ-p-⟨⟩ B a = sym ([]ᵀ-∘ B p ⟨ a ⟩) ∙∙ cong (B [_]ᵀ) (p-⟨⟩ a) ∙∙ []ᵀ-id B

    field
      q-⟨⟩ : (a : Tm Γ A) → PathP (λ i → Tm Γ ([]ᵀ-p-⟨⟩ A a i)) (q [ ⟨ a ⟩ ]ᵗ) a

    field
      U : Ty Γ
      U-[] : (γ : Sub Δ Γ) → U [ γ ]ᵀ ≡ U

      U-[]-∘ :
        (γ : Sub Δ Γ) (δ : Sub Θ Δ) →
        Square
          ([]ᵀ-∘ U γ δ)
          refl
          (U-[] (γ ∘ δ))
          (cong _[ δ ]ᵀ (U-[] γ) ∙ U-[] δ)
      U-[]-id : Square ([]ᵀ-id (U {Γ})) refl (U-[] id) refl

    []ᵘ-filler : (Â : Tm Γ U) (γ : Sub Δ Γ) (i : I) → Tm Δ (U-[] γ i)
    []ᵘ-filler {Δ = Δ} Â γ i =
      transport-filler (λ i → Tm Δ (U-[] γ i)) (Â [ γ ]ᵗ) i

    infixl 9 _[_]ᵘ
    _[_]ᵘ : Tm Γ U → Sub Δ Γ → Tm Δ U
    Â [ γ ]ᵘ = []ᵘ-filler Â γ i1

    []ᵘ-∘ :
      (Â : Tm Γ U) (γ : Sub Δ Γ) (δ : Sub Θ Δ) → Â [ γ ∘ δ ]ᵘ ≡ Â [ γ ]ᵘ [ δ ]ᵘ
    []ᵘ-∘ {Θ = Θ} Â γ δ i =
      comp (λ j → Tm Θ (U-[]-∘ γ δ j i))
        (λ where
          j (i = i0) → []ᵘ-filler Â (γ ∘ δ) j
          j (i = i1) →
            comp
              (λ i →
                Tm Θ (compPath-filler (cong _[ δ ]ᵀ (U-[] γ)) (U-[] δ) i j))
              (λ where
                i (j = i0) → Â [ γ ]ᵗ [ δ ]ᵗ
                i (j = i1) → []ᵘ-filler (Â [ γ ]ᵘ) δ i)
              ([]ᵘ-filler Â γ j [ δ ]ᵗ))
        ([]ᵗ-∘ Â γ δ i)

    []ᵘ-id : (Â : Tm Γ U) → Â [ id ]ᵘ ≡ Â
    []ᵘ-id {Γ = Γ} Â i =
      comp
        (λ j → Tm Γ (U-[]-id j i))
        (λ where
          j (i = i0) → []ᵘ-filler Â id j
          j (i = i1) → Â)
        ([]ᵗ-id Â i)

    field
      El : Tm Γ U → Ty Γ
      El-[] : (Â : Tm Γ U) (γ : Sub Δ Γ) → El Â [ γ ]ᵀ ≡ El (Â [ γ ]ᵘ)

      El-[]-∘ :
        (Â : Tm Γ U) (γ : Sub Δ Γ) (δ : Sub Θ Δ) →
        Square
          ([]ᵀ-∘ (El Â) γ δ)
          (cong El ([]ᵘ-∘ Â γ δ))
          (El-[] Â (γ ∘ δ))
          (cong _[ δ ]ᵀ (El-[] Â γ) ∙ El-[] (Â [ γ ]ᵘ) δ)
      El-[]-id :
        (Â : Tm Γ U) →
        Square ([]ᵀ-id (El Â)) (cong El ([]ᵘ-id Â)) (El-[] Â id) refl

      Π : (A : Ty Γ) → Ty (Γ ▹ A) → Ty Γ
      Π-[] :
        (A : Ty Γ) (B : Ty (Γ ▹ A)) (γ : Sub Δ Γ) →
        Π A B [ γ ]ᵀ ≡ Π (A [ γ ]ᵀ) (B [ γ ⁺ ]ᵀ)

      Π-[]-∘ :
        (A : Ty Γ) (B : Ty (Γ ▹ A)) (γ : Sub Δ Γ) (δ : Sub Θ Δ) →
        Square
          ([]ᵀ-∘ (Π A B) γ δ)
          (cong₂ Π ([]ᵀ-∘ A γ δ) ([]ᵀ-⁺-∘ B γ δ))
          (Π-[] A B (γ ∘ δ))
          (cong _[ δ ]ᵀ (Π-[] A B γ) ∙ Π-[] (A [ γ ]ᵀ) (B [ γ ⁺ ]ᵀ) δ)
      Π-[]-id :
        (A : Ty Γ) (B : Ty (Γ ▹ A)) →
        Square ([]ᵀ-id (Π A B)) (cong₂ Π ([]ᵀ-id A) ([]ᵀ-⁺-id B)) (Π-[] A B id) refl

      app : Tm Γ (Π A B) → Tm (Γ ▹ A) B
      lam : Tm (Γ ▹ A) B → Tm Γ (Π A B)
      lam-[] :
        (b : Tm (Γ ▹ A) B) (γ : Sub Δ Γ) →
        PathP (λ i → Tm Δ (Π-[] A B γ i)) (lam b [ γ ]ᵗ) (lam (b [ γ ⁺ ]ᵗ))

      Π-β : (b : Tm (Γ ▹ A) B) → app (lam b) ≡ b
      Π-η : (f : Tm Γ (Π A B)) → f ≡ lam (app f)

    []ᵀ-idr :
      (A : Ty Γ) (γ : Sub Δ Γ) →
      Square (cong (A [_]ᵀ) (idr γ)) ([]ᵀ-id (A [ γ ]ᵀ)) ([]ᵀ-∘ A γ id) refl
    []ᵀ-idr {Γ} {Δ} A γ i j =
      hcomp
        (λ where
          k (i = i0) → []ᵀ-id (A [ idr γ j ]ᵀ) k
          k (i = i1) → []ᵀ-id ([]ᵀ-id (A [ γ ]ᵀ) j) k
          k (j = i0) → []ᵀ-id ([]ᵀ-∘ A γ id i) k
          k (j = i1) → []ᵀ-id (A [ γ ]ᵀ) k)
        (hcomp
          (λ where
            k (i = i0) → []ᵀ-∘ A (idr γ j) id k
            k (i = i1) → []ᵀ-id (A [ γ ]ᵀ) j [ id ]ᵀ
            k (j = i0) →
              compPath-filler'
                ([]ᵀ-∘ A (γ ∘ id) id)
                (cong (_[ id ]ᵀ) ([]ᵀ-∘ A γ id))
                (~ k) i
            k (j = i1) → []ᵀ-∘ A γ id (i ∨ k))
          (hcomp
            (λ where
              k (i = i0) →
                A [ isSet→isSet'
                      (isSetSub Δ Γ)
                      (λ k → assoc γ id id k)
                      (λ k → γ ∘ id)
                      (λ j → γ ∘ idl id j)
                      (λ j → idr γ j ∘ id)
                      j k ]ᵀ
              k (i = i1) → []ᵀ-idl (A [ γ ]ᵀ) id k j
              k (j = i0) → []ᵀ-assoc A γ id id i k
              k (j = i1) → []ᵀ-∘ A γ id i)
            ([]ᵀ-∘ A γ (idl id j) i)))