Displayed category

module category-theory.displayed-category where

open import foundations.universe
open import foundations.identity-type
open import foundations.set
open import foundations.transport
open import category-theory.category

record DisplayedCategoryData {o h} (𝒞 : CategoryData o h) o′ h′ : Type (o ⊔ h ⊔ lsuc o′ ⊔ lsuc h′) where
  private module 𝒞 = CategoryData 𝒞
  field
    Ob : 𝒞.Ob → Type o′
    Hom : ∀ {A B : 𝒞.Ob} (f : 𝒞.Hom A B) (X : Ob A) (Y : Ob B) → Type h′

    id : ∀ {A} (X : Ob A) → Hom (𝒞.id A) X X
    _∘_ : ∀ {A B C} {g : 𝒞.Hom B C} {f : 𝒞.Hom A B}
      → ∀ {X : Ob A} {Y : Ob B} {Z : Ob C}
      → (g′ : Hom g Y Z)
      → (f′ : Hom f X Y)
      → Hom (g 𝒞.∘ f) X Z

  infix  _∘_

record isDisplayedCategory {o h} (𝒞 : Category o h)
  {o′ h′} (𝒟 : DisplayedCategoryData (Category.𝒞 𝒞) o′ h′) : Type (o ⊔ h ⊔ o′ ⊔ h′) where
  open DisplayedCategoryData 𝒟
  private module 𝒞 = Category 𝒞
  field
    identˡ : ∀ {A B} {f : 𝒞.Hom A B} {X Y} (f′ : Hom f X Y)
      → subst (λ x → Hom x X Y) (𝒞.identˡ f) (id Y ∘ f′) ＝ f′
    identʳ : ∀ {A B} {f : 𝒞.Hom A B} {X Y} (f′ : Hom f X Y)
      → subst (λ x → Hom x X Y) (𝒞.identʳ f) (f′ ∘ id X) ＝ f′
    ident² : ∀ {A} X
      → subst (λ x → Hom x X X) (𝒞.ident² A) (id X ∘ id X) ＝ id X

    assoc : ∀ {A B C D} {f : 𝒞.Hom A B} {g : 𝒞.Hom B C} {h : 𝒞.Hom C D}
      → ∀ {X Y Z W} {f′ : Hom f X Y} {g′ : Hom g Y Z} {h′ : Hom h Z W}
      → subst (λ x → Hom x X W) 𝒞.assoc ((h′ ∘ g′) ∘ f′) ＝ h′ ∘ (g′ ∘ f′)
    sym-assoc : ∀ {A B C D} {f : 𝒞.Hom A B} {g : 𝒞.Hom B C} {h : 𝒞.Hom C D}
      → ∀ {X Y Z W} {f′ : Hom f X Y} {g′ : Hom g Y Z} {h′ : Hom h Z W}
      → subst (λ x → Hom x X W) 𝒞.sym-assoc (h′ ∘ (g′ ∘ f′)) ＝ (h′ ∘ g′) ∘ f′

    is-set-hom : ∀ {A B} {f : 𝒞.Hom A B} {X Y}
      → isSet (Hom f X Y)

record DisplayedCategory {o h} (𝒞 : Category o h) o′ h′ : Type (o ⊔ h ⊔ lsuc o′ ⊔ lsuc h′) where
  field
    𝒟 : DisplayedCategoryData (Category.𝒞 𝒞) o′ h′
    is-displayed-category : isDisplayedCategory 𝒞 𝒟

  open DisplayedCategoryData 𝒟 public
  open isDisplayedCategory is-displayed-category public

private variable
  o h : Level
  𝒞 : Category o h

oppositeDispCat : DisplayedCategory 𝒞 o h → DisplayedCategory (oppositeCat 𝒞) o h
oppositeDispCat 𝒟 = record
  { 𝒟 = record
    { Ob = Ob
    ; Hom = λ f X Y → Hom f Y X
    ; id = id
    ; _∘_ = λ g′ f′ → f′ ∘ g′
    }
  ; is-displayed-category = record
    { identˡ = identʳ
    ; identʳ = identˡ
    ; ident² = ident²
    ; assoc = sym-assoc
    ; sym-assoc = assoc
    ; is-set-hom = is-set-hom
    }
  }
  where
    open DisplayedCategory 𝒟

_ : ∀ {o h} {𝒞 : Category o h} {o′ h′} {𝒟 : DisplayedCategory 𝒞 o′ h′}
  → oppositeDispCat (oppositeDispCat 𝒟) ＝ 𝒟
_ = refl