Precategories with attributes

Content created by Daniel Gratzer, Egbert Rijke, Elisabeth Stenholm and Fredrik Bakke.

Created on 2023-11-27.
Last modified on 2024-02-06.

module type-theories.precategories-with-attributes where
open import category-theory.commuting-squares-of-morphisms-in-precategories
open import category-theory.functors-precategories
open import category-theory.natural-transformations-functors-precategories
open import category-theory.opposite-precategories
open import category-theory.precategories
open import category-theory.precategory-of-elements-of-a-presheaf
open import category-theory.presheaf-categories
open import category-theory.pullbacks-in-precategories

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.category-of-sets
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.sections
open import foundation.sets
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.universe-levels


A precategory with attributes consists of:

  • a precategory C, which we think of as a category of contexts and context morphisms
  • a presheaf Ty on C, which we think of as giving the types in each context
  • a functor ext from ∫ Ty to C, which we think of as context extension
  • a natural transformation p from ext to the projection from ∫ Ty to C such that
  • the naturality squares of p are pullback squares

This is a reformulation of Definition 1, slide 24 of

    (l1 l2 l3 : Level) :
    UU (lsuc l1  lsuc l2  lsuc l3)

    ctx-category : Precategory l1 l2

  Ctx : UU l1
  Ctx = obj-Precategory ctx-category

  Sub : Ctx  Ctx  UU l2
  Sub = hom-Precategory ctx-category

    ty-presheaf : presheaf-Precategory ctx-category l3

  Ty : Ctx  UU l3
  Ty Γ = element-presheaf-Precategory ctx-category ty-presheaf Γ

  ∫Ty : Precategory (l1  l3) (l2  l3)
  ∫Ty = precategory-of-elements-presheaf-Precategory ctx-category ty-presheaf

  obj-∫Ty : UU (l1  l3)
  obj-∫Ty = obj-Precategory ∫Ty

  hom-∫Ty : obj-∫Ty  obj-∫Ty  UU (l2  l3)
  hom-∫Ty = hom-Precategory ∫Ty

  proj-∫Ty : functor-Precategory ∫Ty ctx-category
  proj-∫Ty =
      ( ctx-category)
      ( ty-presheaf)

  _·_ : {Δ Γ : Ctx} (A : Ty Γ) (γ : Sub Δ Γ)  Ty Δ
  A · γ = action-presheaf-Precategory ctx-category ty-presheaf γ A

  preserves-comp-Ty :
    {Δ Δ' Γ : Ctx} (A : Ty Γ) (γ : Sub Δ' Γ) (δ : Sub Δ Δ') 
    A · comp-hom-Precategory ctx-category γ δ  (A · γ) · δ
  preserves-comp-Ty A γ δ =
    preserves-comp-action-presheaf-Precategory ctx-category ty-presheaf γ δ A

  preserves-id-Ty :
    {Γ : Ctx} (A : Ty Γ)  A · id-hom-Precategory ctx-category  A
  preserves-id-Ty {Γ} =
    preserves-id-action-presheaf-Precategory ctx-category ty-presheaf

    ext-functor : functor-Precategory ∫Ty ctx-category

  ext : (Γ : Ctx) (A : Ty Γ)  Ctx
  ext Γ A = obj-functor-Precategory ∫Ty ctx-category ext-functor (Γ , A)

  ⟨_,_⟩ : {Γ Δ : Ctx} (σ : Sub Γ Δ) (A : Ty Δ)  Sub (ext Γ (A · σ)) (ext Δ A)
   σ , A  = hom-functor-Precategory ∫Ty ctx-category ext-functor (σ , refl)

    p-natural-transformation :
      natural-transformation-Precategory ∫Ty ctx-category ext-functor proj-∫Ty

  p : (Γ : Ctx) (A : Ty Γ)  Sub (ext Γ A) Γ
  p Γ A = pr1 p-natural-transformation (Γ , A)

  naturality-p :
    {x y : obj-∫Ty} (f : hom-∫Ty x y) 
      ( ctx-category)
      ( hom-functor-Precategory ∫Ty ctx-category ext-functor f)
      ( p (pr1 x) (pr2 x))
      ( p (pr1 y) (pr2 y))
      ( hom-functor-Precategory ∫Ty ctx-category proj-∫Ty f)
  naturality-p =
      ( precategory-of-elements-presheaf-Precategory
        ( ctx-category)
        ( ty-presheaf))
      ( ctx-category)
      ( ext-functor)
      ( proj-functor-precategory-of-elements-presheaf-Precategory
        ( ctx-category)
          ( ty-presheaf))
      ( p-natural-transformation)

    is-pullback-p :
      (x y : obj-∫Ty) (f : hom-∫Ty x y) 
      is-pullback-obj-Precategory ctx-category _ _ _ _ _ _ _ _ (naturality-p f)

The terms are defined as sections to ext.

  module _
    (Γ : Ctx) (A : Ty Γ)

    Tm : UU l2
    Tm =
      Σ ( Sub Γ (ext Γ A))
        ( λ t 
          comp-hom-Precategory ctx-category (p Γ A) t 
          id-hom-Precategory ctx-category)

    is-set-Tm : is-set Tm
    is-set-Tm =
        ( λ t 
            ( hom-set-Precategory ctx-category Γ Γ)
            ( comp-hom-Precategory ctx-category (p Γ A) t)
            ( id-hom-Precategory ctx-category))
        ( is-set-hom-Precategory ctx-category Γ (ext Γ A))

    Tm-Set : Set l2
    pr1 Tm-Set = Tm
    pr2 Tm-Set = is-set-Tm

  _[_] :
    {Γ Δ : Ctx} {A : Ty Δ} (t : Tm Δ A) (σ : Sub Γ Δ)  Tm Γ (A · σ)
  _[_] {Γ} {Δ} {A} (s , eq) σ =
    ( pr1 gap-map , pr1 (pr2 gap-map))
    sq :
      comp-hom-Precategory ctx-category σ (id-hom-Precategory ctx-category) 
      comp-hom-Precategory ctx-category
        ( p Δ A)
        ( comp-hom-Precategory ctx-category s σ)
    sq =
        comp-hom-Precategory ctx-category σ (id-hom-Precategory ctx-category)
           σ by right-unit-law-comp-hom-Precategory ctx-category σ
              (id-hom-Precategory ctx-category)
              σ by inv (left-unit-law-comp-hom-Precategory ctx-category σ)
           comp-hom-Precategory ctx-category
              (comp-hom-Precategory ctx-category (p Δ A) s)
              σ by ap  k  comp-hom-Precategory ctx-category k σ) (inv eq)
           comp-hom-Precategory ctx-category
              (p Δ A)
              (comp-hom-Precategory ctx-category s σ)
              by associative-comp-hom-Precategory ctx-category _ _ _

    gap-map :
      Σ ( Sub Γ (ext Γ (A · σ)))
        ( λ g 
          ( comp-hom-Precategory ctx-category (p Γ (A · σ)) g 
            id-hom-Precategory ctx-category) ×
          ( ( comp-hom-Precategory ctx-category
              ( pr1 (pr2 ext-functor) (σ , refl))
              ( g)) 
            ( comp-hom-Precategory ctx-category s σ)))
    gap-map =
        ( is-pullback-p
          ( Γ , (A · σ))
          ( Δ , A)
          ( σ , refl)
          ( Γ)
          ( id-hom-Precategory ctx-category)
          ( comp-hom-Precategory ctx-category s σ)
          ( sq))

Recent changes