{-
  Definition of a category displayed over another category.
  Some definitions were guided by those at https://1lab.dev
-}
module Cubical.Categories.Displayed.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Dependent
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Reflection.RecordEquiv
open import Cubical.Categories.Category.Base renaming (isIso to isCatIso)

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

-- Displayed categories with hom-sets
record Categoryᴰ (C : Category ℓC ℓC') ℓCᴰ ℓCᴰ' : Type (ℓ-suc (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓCᴰ ℓCᴰ'))) where
  no-eta-equality
  open Category C
  field
    ob[_] : ob → Type ℓCᴰ
    Hom[_][_,_] : {x y : ob} → Hom[ x , y ] → ob[ x ] → ob[ y ] → Type ℓCᴰ'
    idᴰ : ∀ {x} {p : ob[ x ]} → Hom[ id ][ p , p ]
    _⋆ᴰ_ : ∀ {x y z} {f : Hom[ x , y ]} {g : Hom[ y , z ]} {xᴰ yᴰ zᴰ}
      → Hom[ f ][ xᴰ , yᴰ ] → Hom[ g ][ yᴰ , zᴰ ] → Hom[ f ⋆ g ][ xᴰ , zᴰ ]

  infixr  _⋆ᴰ_
  infixr  _∘ᴰ_

  _≡[_]_ : ∀ {x y xᴰ yᴰ} {f g : Hom[ x , y ]} → Hom[ f ][ xᴰ , yᴰ ] → f ≡ g → Hom[ g ][ xᴰ , yᴰ ] → Type ℓCᴰ'
  _≡[_]_ {x} {y} {xᴰ} {yᴰ} fᴰ p gᴰ = PathP (λ i → Hom[ p i ][ xᴰ , yᴰ ]) fᴰ gᴰ

  infix  _≡[_]_

  field
    ⋆IdLᴰ : ∀ {x y} {f : Hom[ x , y ]} {xᴰ yᴰ} (fᴰ : Hom[ f ][ xᴰ , yᴰ ]) → idᴰ ⋆ᴰ fᴰ ≡[ ⋆IdL f ] fᴰ
    ⋆IdRᴰ : ∀ {x y} {f : Hom[ x , y ]} {xᴰ yᴰ} (fᴰ : Hom[ f ][ xᴰ , yᴰ ]) → fᴰ ⋆ᴰ idᴰ ≡[ ⋆IdR f ] fᴰ
    ⋆Assocᴰ : ∀ {x y z w} {f : Hom[ x , y ]} {g : Hom[ y , z ]}  {h : Hom[ z , w ]} {xᴰ yᴰ zᴰ wᴰ}
      (fᴰ : Hom[ f ][ xᴰ , yᴰ ]) (gᴰ : Hom[ g ][ yᴰ , zᴰ ]) (hᴰ : Hom[ h ][ zᴰ , wᴰ ])
      → (fᴰ ⋆ᴰ gᴰ) ⋆ᴰ hᴰ ≡[ ⋆Assoc f g h ] fᴰ ⋆ᴰ (gᴰ ⋆ᴰ hᴰ)
    isSetHomᴰ : ∀ {x y} {f : Hom[ x , y ]} {xᴰ yᴰ} → isSet Hom[ f ][ xᴰ , yᴰ ]

  -- composition: alternative to diagramatic order
  _∘ᴰ_ : ∀ {x y z} {f : Hom[ x , y ]} {g : Hom[ y , z ]} {xᴰ yᴰ zᴰ}
      → Hom[ g ][ yᴰ , zᴰ ] → Hom[ f ][ xᴰ , yᴰ ] → Hom[ f ⋆ g ][ xᴰ , zᴰ ]
  g ∘ᴰ f = f ⋆ᴰ g

-- Helpful syntax/notation
_[_][_,_] = Categoryᴰ.Hom[_][_,_]

module _ {C : Category ℓC ℓC'} (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where
  open Category C
  open Categoryᴰ Cᴰ

  record isIsoᴰ {a b : ob} {f : C [ a , b ]} (f-isIso : isCatIso C f)
    {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} (fᴰ : Hom[ f ][ aᴰ , bᴰ ])
    : Type ℓCᴰ'
    where
    constructor isisoᴰ
    open isCatIso f-isIso
    field
      invᴰ : Hom[ inv ][ bᴰ , aᴰ ]
      secᴰ : invᴰ ⋆ᴰ fᴰ ≡[ sec ] idᴰ
      retᴰ : fᴰ ⋆ᴰ invᴰ ≡[ ret ] idᴰ

  unquoteDecl isIsoᴰIsoΣ = declareRecordIsoΣ isIsoᴰIsoΣ (quote isIsoᴰ)

  CatIsoᴰ : {a b : ob} → CatIso C a b → ob[ a ] → ob[ b ] → Type ℓCᴰ'
  CatIsoᴰ (f , f-isIso) aᴰ bᴰ = Σ[ fᴰ ∈ Hom[ f ][ aᴰ , bᴰ ] ] isIsoᴰ f-isIso fᴰ

  isSetCatIsoᴰ : ∀ {a b : ob} {f : CatIso C a b} {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
    → isSet (CatIsoᴰ f aᴰ bᴰ)
  isSetCatIsoᴰ = isSetΣ isSetHomᴰ (λ fᴰ →
    isSetRetract (isIsoᴰIsoΣ .Iso.fun) (isIsoᴰIsoΣ .Iso.inv) (isIsoᴰIsoΣ .Iso.ret)
    (isSetΣSndProp isSetHomᴰ (λ fᴰ⁻ →
    isProp× (isOfHLevelPathP'  isSetHomᴰ _ _)
            (isOfHLevelPathP'  isSetHomᴰ _ _))))

  CatIsoⱽ : {a : ob} → ob[ a ] → ob[ a ] → Type ℓCᴰ'
  CatIsoⱽ = CatIsoᴰ idCatIso

  idᴰCatIsoᴰ : {x : ob} {xᴰ : ob[ x ]} → CatIsoᴰ idCatIso xᴰ xᴰ
  idᴰCatIsoᴰ = idᴰ , isisoᴰ idᴰ (⋆IdLᴰ idᴰ) (⋆IdLᴰ idᴰ)

  pathToIsoᴰ : ∀ {x y : ob} {xᴰ : ob[ x ]}{yᴰ : ob[ y ]}
    → (p : x ≡ y)
    → (pᴰ : PathP (λ i → ob[ p i ]) xᴰ yᴰ)
    → CatIsoᴰ (pathToIso p) xᴰ yᴰ
  pathToIsoᴰ {x} {y} {xᴰ} {yᴰ} p pᴰ = transport Type≡ idᴰCatIsoᴰ
    where
    Type≡ : CatIsoᴰ idCatIso xᴰ xᴰ ≡ CatIsoᴰ (pathToIso p) xᴰ yᴰ
    Type≡ i = CatIsoᴰ (transp (λ j → CatIso C x (p (i ∧ j))) (~ i) idCatIso) xᴰ (pᴰ i)

  isUnivalentᴰ : Type (ℓ-max (ℓ-max ℓC ℓCᴰ) ℓCᴰ')
  isUnivalentᴰ = ∀ x y (xᴰ : ob[ x ]) (yᴰ : ob[ y ])
    → isEquivOver {Q = λ f → CatIsoᴰ f xᴰ yᴰ}{f = pathToIso {C = C}} pathToIsoᴰ

module _ {C : Category ℓC ℓC'} (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where
  open Category
  private
    module Cᴰ = Categoryᴰ Cᴰ

  open Categoryᴰ
  _^opᴰ : Categoryᴰ (C ^op) ℓCᴰ ℓCᴰ'
  _^opᴰ .ob[_] x = Cᴰ.ob[ x ]
  _^opᴰ .Hom[_][_,_] f xᴰ yᴰ = Cᴰ.Hom[ f ][ yᴰ , xᴰ ]
  _^opᴰ .idᴰ = Cᴰ.idᴰ
  _^opᴰ ._⋆ᴰ_ fᴰ gᴰ = gᴰ Cᴰ.⋆ᴰ fᴰ
  _^opᴰ .⋆IdLᴰ = Cᴰ .⋆IdRᴰ
  _^opᴰ .⋆IdRᴰ = Cᴰ .⋆IdLᴰ
  _^opᴰ .⋆Assocᴰ fᴰ gᴰ hᴰ = symP (Cᴰ.⋆Assocᴰ _ _ _)
  _^opᴰ .isSetHomᴰ = Cᴰ .isSetHomᴰ