Model.Type.Core

{-# OPTIONS --without-K #-}
module Model.Type.Core where

open import Cats.Category
open import Relation.Binary using (IsEquivalence)

open import Model.RGraph as RG using (RGraph)
open import Util.HoTT.Equiv
open import Util.HoTT.FunctionalExtensionality
open import Util.HoTT.HLevel
open import Util.HoTT.Homotopy
open import Util.HoTT.Univalence
open import Util.Prelude hiding (id) renaming (_∘_ to _∘F_)
open import Util.Relation.Binary.LogicalEquivalence using
  ( _↔_ ; forth ; back ; ↔-reflexive )
open import Util.Relation.Binary.PropositionalEquality using
  ( Σ-≡⁺ ; Σ-≡⁻ ; cast ; subst-subst ; subst-sym-subst ; subst-subst-sym )

open Category._≅_ public
open RG._⇒_


infixr 0 _⇒_
infix  4 _≈_ _≈⟦Type⟧_
infixr 9 _∘_


private
  variable Δ Γ Ψ : RGraph


-- This is an RGraph-indexed family of RGraphs.
record ⟦Type⟧ (Δ : RGraph) : Set₁ where
  no-eta-equality
  field
    ObjHSet : Δ .RG.Obj → HSet 0ℓ

  private
    module M₀ δ = HLevel (ObjHSet δ)
    module M₁ {δ} = HLevel (ObjHSet δ)

  open M₀ public using () renaming
    ( type to Obj )
  open M₁ public using () renaming
    ( level to Obj-IsSet )

  field
    eqHProp : ∀ {δ δ′} → Δ .RG.eq δ δ′ → Obj δ → Obj δ′ → HProp 0ℓ

  private
    module M₂ {δ δ′} (δ≈δ′ : Δ .RG.eq δ δ′) x y   = HLevel (eqHProp δ≈δ′ x y)
    module M₃ {δ δ′} {δ≈δ′ : Δ .RG.eq δ δ′} {x y} = HLevel (eqHProp δ≈δ′ x y)

  open M₂ public using () renaming
    ( type to eq )
  open M₃ public using () renaming
    ( level to eq-IsProp )

  field
    eq-refl : ∀ {δ} (x : Obj δ) → eq (Δ .RG.eq-refl δ) x x

open ⟦Type⟧ public


private
  variable T U V W : ⟦Type⟧ Δ


open RGraph


transportEq : ∀ (T : ⟦Type⟧ Δ) {δ γ} {δ≈γ₀ δ≈γ₁ : Δ .eq δ γ} {x y}
  → T .eq δ≈γ₀ x y → T .eq δ≈γ₁ x y
transportEq {Δ} T = subst (λ p → T .eq p _ _) (Δ .eq-IsProp _ _)


transportObj : ∀ (T : ⟦Type⟧ Δ) {δ γ}
  → δ ≡ γ
  → T .Obj δ
  → T .Obj γ
transportObj T = subst (T .Obj)


abstract
  transportObj-resp : ∀ (T : ⟦Type⟧ Δ) {δ γ}
    → (δ≡γ₀ δ≡γ₁ : δ ≡ γ)
    → ∀ {x y}
    → x ≡ y
    → transportObj T δ≡γ₀ x ≡ transportObj T δ≡γ₁ y
  transportObj-resp {Δ} T refl δ≡γ₁ x≡y
    rewrite Δ .Obj-IsSet δ≡γ₁ refl = x≡y


transportObj-resp-eq : ∀ (T : ⟦Type⟧ Δ) {δ₀ γ₀ δ₁ γ₁}
  → (δ₀≡γ₀ : δ₀ ≡ γ₀) (δ₁≡γ₁ : δ₁ ≡ γ₁)
  → ∀ {x y} {δ₀≈δ₁ : Δ .eq δ₀ δ₁} {γ₀≈γ₁ : Δ .eq γ₀ γ₁}
  → T .eq δ₀≈δ₁ x y
  → T .eq γ₀≈γ₁ (transportObj T δ₀≡γ₀ x) (transportObj T δ₁≡γ₁ y)
transportObj-resp-eq {Δ} T refl refl {δ₀≈δ₁ = δ₀≈δ₁} {γ₀≈γ₁} x≈y
  = transportEq T x≈y


abstract
  transportObj∘transportObj : ∀ (T : ⟦Type⟧ Δ) {δ δ′ δ″}
    → (p : δ ≡ δ′) (q : δ′ ≡ δ″) {x : T .Obj δ}
    → transportObj T q (transportObj T p x) ≡ transportObj T (trans p q) x
  transportObj∘transportObj T p q = subst-subst p


  transportObj-refl : ∀ (T : ⟦Type⟧ Δ) {δ}
    → (p : δ ≡ δ) {x : T .Obj δ}
    → transportObj T p x ≡ x
  transportObj-refl {Δ} T p rewrite Δ .Obj-IsSet p refl = refl


record _⇒_ (T U : ⟦Type⟧ Δ) : Set where
  no-eta-equality
  field
    fobj : ∀ {δ} → Obj T δ → Obj U δ
    feq : ∀ {δ δ′} (δ≈δ′ : Δ .RG.eq δ δ′) {x y}
      → eq T δ≈δ′ x y
      → eq U δ≈δ′ (fobj x) (fobj y)

open _⇒_ public


record _≈_ (f g : T ⇒ U) : Set where
  no-eta-equality
  constructor ≈⁺
  field
    ≈⁻ : ∀ δ (x : Obj T δ) → f .fobj x ≡ g .fobj x

open _≈_ public


≈-isEquivalence : (T U : ⟦Type⟧ Δ) → IsEquivalence (_≈_ {T = T} {U})
≈-isEquivalence T U = record
  { refl = ≈⁺ λ γ x → refl
  ; sym = λ f≈g → ≈⁺ λ γ x → sym (f≈g .≈⁻ γ x)
  ; trans = λ f≈g g≈h → ≈⁺ λ γ x → trans (f≈g .≈⁻ γ x) (g≈h .≈⁻ γ x)
  }


⇒Canon : (T U : ⟦Type⟧ Δ) → Set
⇒Canon {Δ} T U
  = Σ[ fobj ∈ (∀ {δ} → T .Obj δ → U .Obj δ) ]
      (∀ {δ δ′} (δ≈δ′ : Δ .RG.eq δ δ′) {x y}
        → T .eq δ≈δ′ x y → U .eq δ≈δ′ (fobj x) (fobj y))


⇒≅⇒Canon : (T ⇒ U) ≅ ⇒Canon T U
⇒≅⇒Canon = record
  { forth = λ f → f .fobj , f .feq
  ; isIso = record
    { back = λ f → record { fobj = f .proj₁ ; feq = f .proj₂ }
    ; back∘forth = λ where
        record { fobj = fo ; feq = fe } → refl
    ; forth∘back = λ x → refl
    }
  }


⇒Canon-IsSet : (T U : ⟦Type⟧ Δ) → IsSet (⇒Canon T U)
⇒Canon-IsSet T U = Σ-IsSet
  (∀∙-IsSet λ δ → →-IsSet (U .Obj-IsSet))
  (λ _ → ∀∙-IsSet λ δ → ∀∙-IsSet λ δ′ → ∀-IsSet λ δ≈δ′ → ∀∙-IsSet λ x
    → ∀∙-IsSet λ y → →-IsSet (IsProp→IsSet (U .eq-IsProp)))


⇒-IsSet : IsSet (T ⇒ U)
⇒-IsSet {T = T} {U} = ≅-pres-IsOfHLevel 2 (≅-sym ⇒≅⇒Canon) (⇒Canon-IsSet T U)


≈→≡Canon : {f g : T ⇒ U}
  → f ≈ g → ⇒≅⇒Canon .forth f ≡ ⇒≅⇒Canon .forth g
≈→≡Canon {U = U} f≈g = Σ-≡⁺
  ( (funext∙ (funext (λ x → f≈g .≈⁻ _ x)))
  , funext∙ (funext∙ (funext λ a → funext∙ (funext∙
      (funext λ eq → U .eq-IsProp _ _)))) )


≈→≡ : {f g : T ⇒ U} → f ≈ g → f ≡ g
≈→≡ f≈g = ≅-Injective ⇒≅⇒Canon (≈→≡Canon f≈g)


private
  open module M₀ {Δ} {T U : ⟦Type⟧ Δ}
    = IsEquivalence (≈-isEquivalence T U)
    public using () renaming
    ( refl to ≈-refl
    ; sym to ≈-sym
    ; trans to ≈-trans
    ; reflexive to ≈-reflexive )


id : {T : ⟦Type⟧ Δ} → T ⇒ T
id = record
  { fobj = λ x → x
  ; feq = λ γ≈γ′ x → x
  }


_∘_ : {T U V : ⟦Type⟧ Δ} → U ⇒ V → T ⇒ U → T ⇒ V
_∘_ {Γ} f g = record
  { fobj = f .fobj ∘F g .fobj
  ; feq = λ γ≈γ′ → f .feq γ≈γ′ ∘F g .feq γ≈γ′
  }


⟦Types⟧ : RGraph → Category (lsuc 0ℓ) 0ℓ 0ℓ
⟦Types⟧ Δ = record
  { Obj = ⟦Type⟧ Δ
  ; _⇒_ = _⇒_
  ; _≈_ = _≈_
  ; id = id
  ; _∘_ = _∘_
  ; equiv = ≈-isEquivalence _ _
  ; ∘-resp = λ {Δ Γ Ψ f g h i} f≈g h≈i
    → ≈⁺ λ γ x → trans (f≈g .≈⁻ γ (h .fobj x)) (cong (g .fobj) (h≈i .≈⁻ γ x))
  ; id-r = ≈⁺ λ γ x → refl
  ; id-l = ≈⁺ λ γ x → refl
  ; assoc = ≈⁺ λ γ x → refl
  }


module ⟦Types⟧ {Γ} = Category (⟦Types⟧ Γ)


_≈⟦Type⟧_ : (T U : ⟦Type⟧ Δ) → Set₁
_≈⟦Type⟧_ = ⟦Types⟧._≅_


private
  open module M₁ {Δ} = ⟦Types⟧.≅ {Δ} public using () renaming
    ( refl to ≈⟦Type⟧-refl
    ; sym to ≈⟦Type⟧-sym
    ; trans to ≈⟦Type⟧-trans
    ; reflexive to ≈⟦Type⟧-reflexive )

module ≅-Reasoning = ⟦Types⟧.≅-Reasoning
module ≈-Reasoning = ⟦Types⟧.≈-Reasoning


⟦Type⟧Canon : RGraph → Set₁
⟦Type⟧Canon Δ
  = Σ[ ObjHSet ∈ (Δ .Obj → HSet 0ℓ) ]
    Σ[ eq ∈ (∀ {δ δ′} (δ≈δ′ : Δ .eq δ δ′)
        → (x : ObjHSet δ .type) (y : ObjHSet δ′ .type) → HProp 0ℓ) ]
    (∀ {δ} (x : ObjHSet δ .type) → eq (Δ .eq-refl δ) x x .type)


⟦Type⟧≅⟦Type⟧Canon : ∀ {Δ} → ⟦Type⟧ Δ ≅ ⟦Type⟧Canon Δ
⟦Type⟧≅⟦Type⟧Canon {Δ} = record
  { forth = λ T → T .ObjHSet , T .eqHProp , T .eq-refl
  ; isIso = record
    { back = λ T → record
      { ObjHSet = T .proj₁
      ; eqHProp = T .proj₂ .proj₁
      ; eq-refl = T .proj₂ .proj₂
      }
    ; back∘forth = λ where
        record { ObjHSet = x ; eqHProp = y ; eq-refl = z } → refl
    ; forth∘back = λ x → refl
    }
  }


proj₁∘subst : ∀ {α β γ} {A : Set α} (B : A → Set β) (C : ∀ a → B a → Set γ)
  → ∀ {a a′} (p : a ≡ a′) (x : Σ (B a) (C a))
  → proj₁ (subst (λ a → Σ (B a) (C a)) p x) ≡ subst B p (proj₁ x)
proj₁∘subst B C refl x = refl


≈⟦Type⟧→≡Canon
  : T ≈⟦Type⟧ U
  → ⟦Type⟧≅⟦Type⟧Canon .forth T ≡ ⟦Type⟧≅⟦Type⟧Canon .forth U
≈⟦Type⟧→≡Canon {Δ} {T} {U} T≈U
  = Σ-≡⁺ (T≡U , Σ-≡⁺ (T≈≡U≈ , funext∙ (funext (λ x → U .eq-IsProp _ _))))
  where
    T≅U : ∀ δ → T .Obj δ ≅ U .Obj δ
    T≅U δ = record
      { forth = T≈U .forth .fobj
      ; isIso = record
        { back = T≈U .back .fobj
        ; back∘forth = λ x → T≈U .back-forth .≈⁻ _ _
        ; forth∘back = λ x → T≈U .forth-back .≈⁻ _ _
        }
      }


    T≡U : T .ObjHSet ≡ U .ObjHSet
    T≡U = funext λ δ → HLevel-≡⁺ _ _ (≅→≡ (T≅U δ))


    -- "HoTT makes everything so much nicer", they said. "It's all automatic",
    -- they said.
    abstract
      subst-type : ∀ {α n} (A B : HLevel n α)
        → (p : A .type ≡ B .type)
        → (x : A .type)
        → subst type (HLevel-≡⁺ A B p) x ≡ cast p x
      subst-type A B refl x with IsOfHLevel-IsProp _ (A .level) (B .level)
      ... | refl = refl


      -- I believe this equation would be definitional in Cubical TT.
      subst-T≡U : ∀ {δ} x
        → subst (λ T → T δ .type) T≡U x ≡ T≈U .forth .fobj x
      subst-T≡U {δ} x
        = trans (subst-funext (λ δ T → T .type) _ x)
          (trans (subst-type (T .ObjHSet δ) (U .ObjHSet δ) (≅→≡ (T≅U δ)) x)
            (cast-≅→≡ (T≅U δ)))


      go : (Δ : Set) (T U : Δ → HSet 0ℓ) (eqΔ : Δ → Δ → Set)
        → (eqT : ∀ δ δ′ → eqΔ δ δ′ → T δ .type → T δ′ .type → HProp 0ℓ)
        → (eqU : ∀ δ δ′ → eqΔ δ δ′ → U δ .type → U δ′ .type → HProp 0ℓ)
        → (T≡U : T ≡ U)
        → (∀ δ δ′ (δ≈δ′ : eqΔ δ δ′) (x : T δ .type) (y : T δ′ .type)
            → eqT _ _ δ≈δ′ x y .type
            ↔ eqU _ _ δ≈δ′
                (subst (λ T → T δ .type) T≡U x)
                (subst (λ T → T δ′ .type) T≡U y)
                .type)
        → _≡_ {A = ∀ {δ δ′} → eqΔ δ δ′ → U δ .type → U δ′ .type → HProp 0ℓ}
            (subst (λ T → ∀ {δ δ′} → eqΔ δ δ′ → T δ .type → T δ′ .type → HProp 0ℓ)
              T≡U (λ {δ δ′} → eqT δ δ′))
            (λ {δ δ′} → eqU δ δ′)
      go Δ T U eqΔ eqT eqU refl eq = funext∙ λ {δ} → funext∙ λ {δ′}
        → funext λ δ≈δ′ → funext λ x → funext λ y
        → HProp-≡⁺ _ _ (eq δ δ′ δ≈δ′ x y)


      T≈≡U≈ : _
      T≈≡U≈
        = trans
            (proj₁∘subst
              (λ T → ∀ {δ δ′} → Δ .eq δ δ′ → T δ .type → T δ′ .type → HProp 0ℓ)
              (λ T eq → ∀ {δ} (x : T δ .type) → eq (Δ .eq-refl δ) x x .type)
              T≡U
              ((λ {δ δ′} → T .eqHProp {δ} {δ′}), (λ {δ} x → T .eq-refl {δ} x)))
            (go (Δ .Obj) (T .ObjHSet) (U .ObjHSet) (Δ .eq)
              (λ δ δ′ → T .eqHProp {δ} {δ′})
              (λ δ δ′ → U .eqHProp {δ} {δ′})
              T≡U
              λ δ δ′ δ≈δ′ x y → record
                { forth = λ x≈y
                    → subst₂ (λ x y → U .eq δ≈δ′ x y) (sym (subst-T≡U x))
                        (sym (subst-T≡U y)) (T≈U .forth .feq δ≈δ′ x≈y)
                ; back = λ x≈y
                    → subst₂ (λ x y → T .eq δ≈δ′ x y)
                        (trans (cong (T≈U .back .fobj) (subst-T≡U x))
                          (T≈U .back-forth .≈⁻ δ x))
                        (trans (cong (T≈U .back .fobj) (subst-T≡U y))
                          (T≈U .back-forth .≈⁻ δ′ y))
                        (T≈U .back .feq δ≈δ′ x≈y)
                })


≈⟦Type⟧→≡ : T ≈⟦Type⟧ U → T ≡ U
≈⟦Type⟧→≡ T≈U = ≅-Injective ⟦Type⟧≅⟦Type⟧Canon (≈⟦Type⟧→≡Canon T≈U)


subT : ∀ {Δ Ω} → Δ RG.⇒ Ω → ⟦Type⟧ Ω → ⟦Type⟧ Δ
subT {Γ} {Ω} f T = record
  { ObjHSet = T .ObjHSet ∘F f .fobj
  ; eqHProp = T .eqHProp ∘F f .feq
  ; eq-refl = λ x
      → subst (λ p → T .eq p x x) (Ω .eq-IsProp _ _) (T .eq-refl x)
  }


subt : ∀ {Δ Ω} (f : Δ RG.⇒ Ω) {T U : ⟦Type⟧ Ω}
  → T ⇒ U
  → subT f T ⇒ subT f U
subt f g = record
  { fobj = g .fobj
  ; feq = λ γ≈γ′ → g .feq (f .feq γ≈γ′)
  }


subt-∘ : ∀ {Δ Ω} (f : Δ RG.⇒ Ω) {T U V : ⟦Type⟧ Ω}
  → (g : U ⇒ V) (h : T ⇒ U)
  → subt f (g ∘ h) ≈ subt f g ∘ subt f h
subt-∘ f g h = ≈⁺ λ δ γ → refl


subT∘subT : ∀ {Δ Γ Ψ}
  → {f : Δ RG.⇒ Ψ} {g : Γ RG.⇒ Δ} {T : ⟦Type⟧ Ψ}
  → subT g (subT f T) ≈⟦Type⟧ subT (f RG.∘ g) T
subT∘subT = record
  { forth = record { fobj = λ x → x ; feq = λ _ x → x }
  ; back = record { fobj = λ x → x ; feq = λ _ x → x }
  ; back-forth = ≈⁺ λ γ x → refl
  ; forth-back = ≈⁺ λ γ x → refl
  }


castObj : {T U : ⟦Type⟧ Δ} → T ≡ U → ∀ {δ} → Obj T δ → Obj U δ
castObj p {δ} = subst (λ T → Obj T δ) p


≡→≈⟦Type⟧ : {T U : ⟦Type⟧ Δ} → T ≡ U → T ≈⟦Type⟧ U
≡→≈⟦Type⟧ {Δ} {T} {U} T≡U = record
  { forth = record
    { fobj = λ {δ} → castObj T≡U
    ; feq = λ δ≈δ′ x≈y → go T≡U x≈y
    }
  ; back = record
    { fobj = λ {δ} → castObj (sym T≡U)
    ; feq = λ δ≈δ′ x≈y → go (sym T≡U) x≈y
    }
  ; back-forth = ≈⁺ λ δ x → subst-sym-subst T≡U
  ; forth-back = ≈⁺ λ δ x → subst-subst-sym T≡U
  }
  where
    go : {T U : ⟦Type⟧ Δ} (p : T ≡ U) → ∀ {δ δ′} {δ≈δ′ : Δ .eq δ δ′} {x y}
      → eq T δ≈δ′ x y
      → eq U δ≈δ′ (castObj p x) (castObj p y)
    go refl x≈y = x≈y