Categories.AW-MSciProject

Anna Williams, March 2026

This file corresponds to the paper

https://anna-maths.xyz/assets/papers/disp-categories.pdf


{-# OPTIONS --safe --without-K #-}

open import Categories.Wild
open import Categories.Pre
open import Categories.Univalent
open import Categories.Examples.Set
open import Categories.Examples.Magma

open import Categories.Functor
open import Categories.Functor-Composition

open import Categories.NaturalTransformation

open import Categories.Adjoint

open import Categories.Notation.Wild
open import Categories.Notation.Pre

open import Categories.Displayed.Pre
open import Categories.Displayed.Univalent
open import Categories.Displayed.Examples.Magma

open import Categories.Displayed.Functor

open import Categories.Displayed.Total

open import Categories.Displayed.Notation.Pre

module Categories.AW-MSciProject where

open import MLTT.Spartan
open import Notation.UnderlyingType
open import UF.DependentEquality
open import UF.FunExt
open import UF.Sets
open import UF.Subsingletons
open import UF.Univalence


## Chapter 3: Category Theory

### Section 3.1: Categories


Definition-3-1 : (𝓤 𝓥 : Universe) → (𝓤 ⊔ 𝓥) ⁺ ̇
Definition-3-1 = WildCategory

Example-3-2 : WildCategory (𝓤 ⁺) 𝓤
Example-3-2 = SetWildCategory

Example-3-3 : Fun-Ext → WildCategory (𝓤 ⁺) 𝓤
Example-3-3 = MagmaWildCategory

Definition-3-4 : (W : WildCategory 𝓤 𝓥)
               → (A B : obj W)
               → 𝓥 ̇
Definition-3-4 W A B = A ≅ B
 where
  open WildCategoryNotation W

module _ (W : WildCategory 𝓤 𝓥) where
 open WildCategoryNotation W

 Proposition-3-5 : (A B : obj W)
                 → (f : A ≅ B)
                 → (g h : inverse ⌜ f ⌝)
                 → pr₁ g ＝ pr₁ h
 Proposition-3-5 _ _ _ = at-most-one-inverse

Definition-3-6 : (W : WildCategory 𝓤 𝓥)
                 (p : is-precategory W)
               → Precategory 𝓤 𝓥
Definition-3-6 W p = W , p

Proposition-3-7 : (W : WildCategory 𝓤 𝓥)
                → Fun-Ext
                → is-prop (is-precategory W)
Proposition-3-7 = being-precat-is-prop

Example-3-8-Set : Fun-Ext → Precategory (𝓤 ⁺) 𝓤
Example-3-8-Set = SetPrecategory

Example-3-8-Magma : Fun-Ext → Precategory (𝓤 ⁺) 𝓤
Example-3-8-Magma = MagmaPrecategory

module _ (P : Precategory 𝓤 𝓥) where
 open PrecategoryNotation P

 Proposition-3-9-prop : {a b : obj P}
                        (f : hom a b)
                      → is-prop (inverse f)
 Proposition-3-9-prop = being-iso-is-prop P

 Proposition-3-9-set : {a b : obj P}
                     → is-set (a ≅ b)
 Proposition-3-9-set = isomorphism-type-is-set P

 Corollary-3-10 : {a b : obj P}
                  {f f' : a ≅ b}
                → ⌜ f ⌝ ＝ ⌜ f' ⌝
                → f ＝ f'
 Corollary-3-10 = to-≅-＝

 Proposition-3-11 : (a b : obj P)
                  → (a ＝ b → a ≅ b)
 Proposition-3-11 a b = id-to-iso a b

Definition-3-12 : (P : Precategory 𝓤 𝓥)
                  (p : is-category P)
                → Category 𝓤 𝓥
Definition-3-12 P p = P , p

Corollary-3-13 : (C : Category 𝓤 𝓥)
               → ((a b : obj C) → is-set (a ＝ b))
Corollary-3-13 = cat-objs-form-a-1-type

Example-3-15 : is-univalent 𝓤
             → Fun-Ext
             → Category (𝓤 ⁺) 𝓤
Example-3-15 = SetCategory

Example-3-16 : Fun-Ext
             → is-univalent 𝓤
             → Category (𝓤 ⁺) 𝓤
Example-3-16 = MagmaCategory


### Functors


Definition-3-17 : (P : Precategory 𝓤 𝓥)
                  (Q : Precategory 𝓦 𝓣)
                → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣 ̇
Definition-3-17 P Q = Functor P Q

Example-3-19 : (P : Precategory 𝓤 𝓥)
             → Functor P P
Example-3-19 P = id-functor P

module _ {A : Precategory 𝓤 𝓥}
         {B : Precategory 𝓤' 𝓥'}
         {C : Precategory 𝓦 𝓣}
         {D : Precategory 𝓦' 𝓣'} where

 Definition-3-20 : (G : Functor B C)
                   (F : Functor A B)
                 → Functor A C
 Definition-3-20 G F = G F∘ F

 Proposition-3-21-left : Fun-Ext
                       → (F : Functor A B)
                       → F F∘ (id-functor A) ＝ F
 Proposition-3-21-left = id-left-neutral-F∘

 Proposition-3-21-right : Fun-Ext
                        → (F : Functor A B)
                        → (id-functor B) F∘ F ＝ F
 Proposition-3-21-right = id-right-neutral-F∘

 Proposition-3-22 : Fun-Ext
                  → (F : Functor A B)
                    (G : Functor B C)
                    (H : Functor C D)
                  → H F∘ (G F∘ F) ＝ (H F∘ G) F∘ F
 Proposition-3-22 = assoc-F∘


### Section 3.3: Natural Transformations


module _ {A : Precategory 𝓤 𝓥}
         {B : Precategory 𝓦 𝓣}
         {C : Precategory 𝓤' 𝓥'}
         where

 Definition-3-23 : (F G : Functor A B)
                 → 𝓤 ⊔ 𝓥 ⊔ 𝓣 ̇
 Definition-3-23 F G = NaturalTransformation F G

 Example-3-25 : (F : Functor A B)
              → NaturalTransformation F F
 Example-3-25 F = id-natural-transformation F

 Definition-3-26 : {G H : Functor B C}
                   (μ : NaturalTransformation G H)
                   (F : Functor A B)
                 → NaturalTransformation (G F∘ F) (H F∘ F)
 Definition-3-26 = _·_

 Definition-3-27 : {F G H : Functor A B}
                   (γ : NaturalTransformation G H)
                   (μ : NaturalTransformation F G)
                 → NaturalTransformation F H
 Definition-3-27 = _N∘_


### Section 3.4: Adjoints


 Definition-3-28 : (F : Functor A B)
                 → Fun-Ext
                 → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⊔ 𝓣 ̇
 Definition-3-28 F = LeftAdjoint F


## Chapter 4: Displayed Category Theory

### Section 4.1: Displayed Categories


Definition-4-1 : (𝓦 𝓣 : Universe)
                 (P : Precategory 𝓤 𝓥)
               → (𝓦 ⊔ 𝓣 ⊔ 𝓤 ⊔ 𝓥) ⁺ ̇
Definition-4-1 𝓦 𝓣 P = DisplayedPrecategory 𝓦 𝓣 P

Example-4-2 : {fe : Fun-Ext}
            → DisplayedPrecategory 𝓤 𝓤 (SetPrecategory fe)
Example-4-2 {𝓤} {fe} = DispPreMagma {𝓤} {fe}

module _ {P : Precategory 𝓦 𝓣}
         {a b : obj P} where
 open PrecategoryNotation P

 Definition-4-3 : (D : DisplayedPrecategory 𝓤 𝓥 P)
                  (x : obj[ a ] D)
                  (y : obj[ b ] D)
                  (f : a ≅ b)
                → 𝓥 ̇
 Definition-4-3 D x y f = x ≅[ f ] y
  where
   open DisplayedPrecategoryNotation D


 module _ {D : DisplayedPrecategory 𝓤 𝓥 P} where
  open DisplayedPrecategoryNotation D

  Proposition-4-4 : {x : obj[ a ] D}
                    {y : obj[ b ] D}
                    {f : a ≅ b}
                    (𝕗 : x ≅[ f ] y)
                    (g h : D-inverse f D-⌜ 𝕗 ⌝)
                  → D-⌞ g ⌟ ＝ D-⌞ h ⌟
  Proposition-4-4 𝕗 g h = at-most-one-D-inverse D g h
  Proposition-4-5 : {x : obj[ a ] D}
                    {y : obj[ b ] D}
                    {f : a ≅ b}
                    {𝕗 𝕘 : x ≅[ f ] y}
                  → D-⌜ 𝕗 ⌝ ＝ D-⌜ 𝕘 ⌝
                  → 𝕗 ＝ 𝕘
  Proposition-4-5 = to-≅[-]-＝

  Proposition-4-6 : (x : obj[ a ] D)
                    (y : obj[ b ] D)
                    (e : a ＝ b)
                  → x ＝⟦ (λ - → obj[ - ] D) , e ⟧ y
                  → x ≅[ id-to-iso a b e ] y
  Proposition-4-6 x y e = D-id-to-iso D e x y

 Definition-4-7 : (D : DisplayedPrecategory 𝓤 𝓥 P)
                → is-displayed-category D
                → DisplayedCategory 𝓤 𝓥 P
 Definition-4-7 D p = D , p

 Example-4-8 : {fe : Fun-Ext}
             → DisplayedCategory 𝓤 𝓤 (SetPrecategory fe)
 Example-4-8 {𝓤} {fe} = DispCatMagma {𝓤} {fe}


### Section 4.2: Displayed Functor


Definition-4-9 : {P : Precategory 𝓦 𝓣}
                 {P' : Precategory 𝓦' 𝓣'}
                 (F : Functor P P')
                 (D : DisplayedPrecategory 𝓤 𝓥 P)
                 (D' : DisplayedPrecategory 𝓤' 𝓥' P')
               → 𝓦 ⊔ 𝓣 ⊔ 𝓤 ⊔ 𝓤' ⊔ 𝓥 ⊔ 𝓥' ̇
Definition-4-9 F D D' = DisplayedFunctor F D D'


### Section 4.3: Total Category


Proposition-4-10 : (P : Precategory 𝓤 𝓥)
                   (D : DisplayedPrecategory 𝓦 𝓣 P)
                 → Precategory (𝓤 ⊔ 𝓦) (𝓥 ⊔ 𝓣)
Proposition-4-10 P D = TotalPrecategory D

Proposition-4-11 : (C : Category 𝓤 𝓥)
                   (D : DisplayedCategory 𝓦 𝓣 ⟨ C ⟩)
                 → Category (𝓤 ⊔ 𝓦) (𝓥 ⊔ 𝓣)
Proposition-4-11 C D = TotalCategory {_} {_} {_} {_} {C} D

Example-4-12-pre : {𝓤 : Universe}
                   {fe : Fun-Ext}
                 → Precategory (𝓤 ⁺) 𝓤
Example-4-12-pre {𝓤} {fe} = MagmaTotalPre {𝓤} {fe}

Example-4-12-univ : {𝓤 : Universe}
                    {fe : Fun-Ext}
                  → is-univalent 𝓤
                  → Category (𝓤 ⁺) 𝓤
Example-4-12-univ {𝓤} {fe} = TotCatMagma {𝓤} {fe}