open import Algebra.Group.Cat.FinitelyComplete
open import Algebra.Monoid.Category
open import Algebra.Group.Cat.Base
open import Algebra.Group.Free hiding (_◆_)
open import Algebra.Group.Ab

open import Cat.Morphism.Factorisation.Orthogonal
open import Cat.Diagram.Coequaliser.RegularEpi
open import Cat.Functor.Adjoint.Epireflective
open import Cat.Functor.Adjoint.Representable
open import Cat.Instances.Elements.Covariant renaming (∫ to ∫cov)
open import Cat.Instances.StrictCat.Cohesive hiding (Disc)
open import Cat.Monoidal.Instances.Cartesian
open import Cat.Diagram.Pullback.Properties
open import Cat.Internal.Instances.Discrete
open import Cat.Functor.Adjoint.Continuous
open import Cat.Functor.Adjoint.Reflective
open import Cat.Diagram.Colimit.Universal
open import Cat.Diagram.Coproduct.Indexed
open import Cat.Diagram.Projective.Strong
open import Cat.Diagram.Separator.Regular
open import Cat.Functor.Hom.Representable
open import Cat.Instances.Sets.Cocomplete
open import Cat.Diagram.Separator.Strong
open import Cat.Instances.Functor.Limits
open import Cat.CartesianClosed.Locally
open import Cat.Diagram.Limit.Equaliser
open import Cat.Diagram.Product.Indexed
open import Cat.Functor.Adjoint.Compose
open import Cat.Functor.FullSubcategory
open import Cat.Instances.Sets.Complete
open import Cat.Diagram.Colimit.Cocone
open import Cat.Diagram.Limit.Pullback
open import Cat.Functor.Hom.Properties
open import Cat.Instances.Localisation
open import Cat.Instances.MarkedGraphs
open import Cat.Instances.OuterFunctor
open import Cat.Internal.Functor.Outer
open import Cat.Morphism.Factorisation
open import Cat.Bi.Diagram.Adjunction renaming (_⊣_ to _⊣ᵇ_)
open import Cat.Functor.Adjoint.Monad
open import Cat.Functor.Kan.Pointwise
open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Limit.Finite
open import Cat.Functor.Conservative
open import Cat.Functor.Hom.Coyoneda
open import Cat.Diagram.Coequaliser
open import Cat.Functor.Adjoint.AFT
open import Cat.Functor.Adjoint.Hom
open import Cat.Functor.Adjoint.Kan
open import Cat.Functor.Equivalence
open import Cat.Functor.Kan.Adjoint
open import Cat.Functor.Subcategory
open import Cat.Instances.Delooping
open import Cat.Instances.StrictCat
open import Cat.Morphism.Orthogonal
open import Cat.Morphism.Strong.Epi
open import Cat.Bi.Instances.Spans
open import Cat.Diagram.Idempotent
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Limit.Cone
open import Cat.Functor.Hom.Yoneda
open import Cat.Functor.Properties
open import Cat.Instances.Discrete
open import Cat.Diagram.Equaliser
open import Cat.Diagram.Separator
open import Cat.Instances.Functor
open import Cat.Instances.Karoubi
open import Cat.Instances.Product
open import Cat.Internal.Opposite
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Functor.Constant
open import Cat.Functor.Kan.Base
open import Cat.Functor.Morphism
open import Cat.Instances.Graphs
open import Cat.Diagram.Initial
open import Cat.Diagram.Product
open import Cat.Diagram.Pushout
open import Cat.Functor.Adjoint
open import Cat.Functor.Compose
open import Cat.Instances.Comma
open import Cat.Instances.Slice
open import Cat.Functor.Closed
open import Cat.Instances.Free
open import Cat.Instances.Sets
open import Cat.Morphism.Lifts
open import Cat.Diagram.Monad
open import Cat.Functor.Final
open import Cat.Functor.Joint
open import Cat.Internal.Base
open import Cat.Functor.Base
open import Cat.Functor.Hom
open import Cat.Morphism
open import Cat.Bi.Base
open import Cat.Prelude
open import Cat.Strict

open import Data.Set.Surjection

open import Order.Cat

module Borceux where

Though the 1Lab is not purely a formalization of category theory, it does aim to be a useful reference on the subject. However, the 1Lab organizes content in a highly non-linear fashion; this can make it somewhat difficult to use as a companion to more traditional resources.

This page attempts to (somewhat) rectify this situation by gathering all of the results from Francis Borceux’s “Handbook of Categorical Algebra” (Borceux 1994) in a single place.¹

Volume 1🔗

1 The language of categories🔗

1.1 Logical foundations of the theory🔗

• Proposition 1.1: Russell’s paradox

1.2 Categories and functors🔗

_ = Precategory
_ = Functor
_ = is-strict
_ = Strict-cats
_ = Sets
_ = Groups
_ = poset→category
_ = Disc
_ = B
_ = Slice
_ = Ab↪Sets
_ = Hom[_,-]
_ = Const

• Definition 1.2.1: Precategory
• Definition 1.2.2: Functor
• Definition 1.2.3: is-strict
• Proposition 1.2.4: Strict-cats
• Examples 1.2.5:
  • 1. Sets
  • 3. Groups
• Examples 1.2.6:
  • 2. poset→category
  • 3. Disc
  • 4. B
• Examples 1.2.7:
  • 1. Slice
• Examples 1.2.8:
  • 1. Ab↪Sets
  • 4. Hom[_,-]
  • 5. Const

1.3 Natural transformations🔗

_ = _=>_
_ = Cat[_,_]
_ = _◆_
_ = ◆-interchange
_ = よcov₁
_ = yo-is-equiv
_ = yo-naturalr
_ = yo-naturall
_ = constⁿ

• Definition 1.3.1: _=>_
• Proposition 1.3.2: Cat[_,_]
• Theorem 1.3.3:
  • 1. yo-is-equiv
  • 2. yo-naturalr
  • 3. yo-naturall
• Proposition 1.3.4: _◆_
• Proposition 1.3.5: ◆-interchange
• Examples 1.3.6:
  • 3. よcov₁
  • 4. constⁿ

1.4 Contravariant functors🔗

Borceux defines contravariant functors as a distinct object rather than functors from ${\mathcal{C}}^{\mathrm{op}}\text{;}$ this makes it somewhat difficult to map definitions on a 1-1 basis.

_ = _^op
_ = よcov
_ = よ₀
_ = よ₁
_ = よ

• Definition 1.4.1: _^op
• Definition 1.4.2: _^op
• Examples 1.4.3:
  • 1. よcov
  • 2. よ₀
  • 3. よ₁
  • 4. よ

1.5 Full and faithful functors🔗

_ = is-faithful
_ = is-full
_ = is-fully-faithful
_ = is-precat-iso
_ = よ-is-fully-faithful
_ = よcov-is-fully-faithful
_ = Subcat
_ = Restrict

• Definition 1.5.1:
  • 1. is-faithful
  • 2. is-full
  • 3. is-fully-faithful
  • 4. is-precat-iso
• Proposition 1.5.2:
  • 1. よ-is-fully-faithful
  • 2. よcov-is-fully-faithful
• Definition 1.5.3: Subcat
• Definition 1.5.4: Restrict

1.6 Comma categories🔗

_ = _↓_
_ = Dom
_ = Cod
_ = θ
_ = ∫cov
_ = _×ᶜ_
_ = Cat⟨_,_⟩

• Definition 1.6.1: _↓_
• Proposition 1.6.2:
  • 1. Dom
  • 2. Cod
  • 3. θ
• Definition 1.6.4: ∫cov
• Definition 1.6.5: _×ᶜ_
• Proposition 1.6.6: Cat⟨_,_⟩

1.7 Monomorphisms🔗

_ = is-monic
_ = id-monic
_ = ∘-is-monic
_ = monic-cancell
_ = has-section
_ = has-retract
_ = has-retract→monic
_ = faithful→reflects-mono
_ = embedding→monic
_ = monic→is-embedding

• Definition 1.7.1: is-monic
• Proposition 1.7.2:
  • 1. id-monic
  • 2. ∘-is-monic
  • 3. monic-cancell
• Definition 1.7.3:
  • 1. has-section
  • 2. has-retract
• Proposition 1.7.4: has-retract→monic
• Proposition 1.7.6: faithful→reflects-mono
• Examples 1.7.7:
  • 1. embedding→monic, monic→is-embedding

1.8 Epimorphisms🔗

_ = is-epic
_ = id-epic
_ = ∘-is-epic
_ = epic-cancelr
_ = has-section→epic
_ = faithful→reflects-epi
_ = surjective→regular-epi
_ = epi→surjective

• Definition 1.8.1: is-epic
• Proposition 1.8.2:
  • 1. id-epic
  • 2. ∘-is-epic
  • 3. epic-cancelr
• Proposition 1.8.3: has-section→epic
• Proposition 1.8.4: faithful→reflects-epi
• Examples 1.8.5:
  • 1. surjective→regular-epi, epi→surjective

1.9 Isomorphisms🔗

_ = is-invertible
_ = id-invertible
_ = invertible-∘
_ = invertible→monic
_ = invertible→epic
_ = has-retract+epic→invertible
_ = F-iso.F-map-invertible
_ = is-ff→is-conservative
_ = equiv≃iso

• Definition 1.9.1: is-invertible
• Proposition 1.9.2:
  • 1. id-invertible
  • 2. invertible-∘
  • 3. invertible→monic, invertible→epic
• Proposition 1.9.3: has-retract+epic→invertible
• Proposition 1.9.4: F-iso.F-map-invertible
• Proposition 1.9.5: is-ff→is-conservative
• Examples 1.9.6:
  • 1. equiv≃iso

1.10 The duality principle🔗

_ = Hom[-,-]

• Definition 1.10.1: _^op
• Examples 1.10.3:
  • 1. Hom[-,-]

1.11 Exercises🔗

_ = thin-functor
_ = よ-preserves-mono
_ = よcov-reverses-epi
_ = Curry
_ = Uncurry
_ = has-section+monic→invertible

• Exercise 1.11.1: 🚧 thin-functor
• Exercise 1.11.5: よ-preserves-mono
• Exercise 1.11.6: よcov-reverses-epi
• Exercise 1.11.8: 🚧 Curry, Uncurry
• Exercise 1.11.9: has-section+monic→invertible

2 Limits🔗

2.1 Products🔗

_ = is-product
_ = ×-Unique
_ = Binary-products.swap-is-iso
_ = Cartesian-monoidal
_ = is-indexed-product
_ = Indexed-product-unique
_ = is-indexed-product-assoc

• Definition 2.1.1: is-product
• Proposition 2.1.2: ×-Unique
• Proposition 2.1.3:
  • 1. Binary-products.swap-is-iso
  • 2. Cartesian-monoidal
• Definition 2.1.4: is-indexed-product
• Proposition 2.1.5: Indexed-product-unique
• Proposition 2.1.6: is-indexed-product-assoc

2.2 Coproducts🔗

_ = is-indexed-coproduct
_ = is-indexed-coproduct→iso
_ = is-indexed-coproduct-assoc

• Definition 2.2.1: is-indexed-coproduct
• Proposition 2.2.2: is-indexed-coproduct→iso
• Proposition 2.2.3: is-indexed-coproduct-assoc

2.3 Initial and terminal objects🔗

_ = is-initial
_ = is-terminal
_ = Sets-initial
_ = Sets-terminal
_ = Zero-group-is-zero

• Definition 2.3.1:
  • 1. is-terminal
  • 2. is-initial
• Examples 2.3.2:
  • 1. Sets-initial, Sets-terminal
  • 2. 🚧 Zero-group-is-zero

2.4 Equalizers, coequalizers🔗

_ = is-equaliser
_ = is-equaliser→iso
_ = is-equaliser→is-monic
_ = id-is-equaliser
_ = equaliser+epi→invertible

• Definition 2.4.1: is-equaliser
• Proposition 2.4.2: is-equaliser→iso
• Proposition 2.4.3: is-equaliser→is-monic
• Proposition 2.4.4: id-is-equaliser
• Proposition 2.4.5: equaliser+epi→invertible

2.5 Pullbacks, pushouts🔗

_ = is-pullback
_ = Pullback-unique
_ = is-monic→pullback-is-monic
_ = is-invertible→pullback-is-invertible
_ = is-kernel-pair
_ = is-kernel-pair→epil
_ = is-kernel-pair→epir
_ = monic→id-kernel-pair
_ = id-kernel-pair→monic
_ = same-kernel-pair→id-kernel-pair
_ = is-effective-epi.is-effective-epi→is-regular-epi
_ = is-regular-epi→is-effective-epi
_ = pasting-left→outer-is-pullback
_ = Sets-pullbacks

• Definition 2.5.1: is-pullback
• Proposition 2.5.2: Pullback-unique
• Proposition 2.5.3:
  • 1. is-monic→pullback-is-monic
  • 2. is-invertible→pullback-is-invertible
• Definition 2.5.4: is-kernel-pair
• Proposition 2.5.5: is-kernel-pair→epil, is-kernel-pair→epir
• Proposition 2.5.6:
  • (1 ⇒ 2): monic→id-kernel-pair
  • (2 ⇒ 1): id-kernel-pair→monic
  • (3 ⇒ 2): same-kernel-pair→id-kernel-pair
• Proposition 2.5.7: is-effective-epi.is-effective-epi→is-regular-epi
• Proposition 2.5.8: is-regular-epi→is-effective-epi
• Proposition 2.5.9:
  • 1. pasting-left→outer-is-pullback
• Examples 2.5.10
  • 1. Sets-pullbacks

2.6 Limits and colimits🔗

_ = Cone
_ = is-limit
_ = limits-unique
_ = is-limit.unique₂
_ = Cocone
_ = is-colimit
_ = Limit→Equaliser
_ = Equaliser→Limit
_ = Limit→Pullback
_ = Pullback→Limit

• Definition 2.6.1: Cone
• Definition 2.6.2: is-limit
• Proposition 2.6.3: limits-unique
• Proposition 2.6.4: is-limit.unique₂
• Definition 2.6.5: Cocone
• Definition 2.6.6: is-colimit
• Examples 2.6.7:
  • 2. Limit→Equaliser, Equaliser→Limit
  • 3. Limit→Pullback, Pullback→Limit

2.7 Complete categories🔗

_ = is-complete

• Definition 2.7.2: is-complete

2.8 Existence theorem for limits🔗

_ = with-equalisers
_ = with-pullbacks

• Proposition 2.8.2:
  • 2. with-equalisers
  • 3. with-pullbacks

2.9 Limit preserving functors🔗

_ = preserves-limit
_ = is-lex.pres-monos
_ = corepresentable-preserves-limits
_ = representable-reverses-colimits
_ = reflects-limit
_ = conservative-reflects-limits

• Definition 2.9.1: preserves-limit
• Proposition 2.9.3: is-lex.pres-monos
• Proposition 2.9.4: corepresentable-preserves-limits
• Proposition 2.9.5: representable-reverses-colimits
• Definition 2.9.6: reflects-limit
• Proposition 2.9.7: conservative-reflects-limits

2.10 Absolute colimits🔗

2.11 Final functors🔗

_ = is-final
_ = extend-is-colimit
_ = is-colimit-restrict

• Definition 2.11.1: is-final
• Proposition 2.11.2: extend-is-colimit, is-colimit-restrict

2.12 Interchange of limits🔗

2.13 Filtered colimits🔗

2.14 Universality of colimits🔗

_ = has-stable-colimits

• Definition 2.14.1: has-stable-colimits

2.15 Limits in categories of functors🔗

_ = functor-limit
_ = Functor-cat-is-complete
_ = coyoneda

• Proposition 2.15.1: functor-limit
• Theorem 2.15.2: Functor-cat-is-complete
• Proposition 2.15.6: coyoneda

2.16 Limits in comma categories🔗

2.17 Exercises🔗

_ = Cone→cone

• Exercise 2.17.3: 🚧 Cone→cone
• Exercises 2.17.8: extend-is-colimit, is-colimit-restrict

3 Adjoint functors🔗

3.1 Reflection along a functor🔗

_ = Free-object
_ = free-object-unique
_ = free-objects→left-adjoint
_ = _⊣_
_ = free-objects≃left-adjoint
_ = hom-iso→adjoints
_ = make-free-group
_ = Free-monoid⊣Forget
_ = Disc⊣Γ
_ = Γ⊣Codisc

• Definition 3.1.1: Free-object
• Proposition 3.1.2: free-object-unique
• Proposition 3.1.3: free-objects→left-adjoint
• Definition 3.1.4: _⊣_
• Theorem 3.1.5: free-objects≃left-adjoint, hom-iso→adjoints
• Examples 3.1.6:
  • 1. Free-monoid⊣Forget
  • 2. make-free-group
  • 11. Disc⊣Γ, Γ⊣Codisc

3.2 Properties of adjoint functors🔗

_ = LF⊣GR
_ = right-adjoint-is-continuous

• Proposition 3.2.1: LF⊣GR
• Proposition 3.2.2: right-adjoint-is-continuous

3.3 The adjoint functor theorem🔗

_ = Solution-set
_ = solution-set→left-adjoint

• Definition 3.3.2: Solution-set
• Theorem 3.3.3: solution-set→left-adjoint

3.4 Fully faithful adjoint functors🔗

_ = is-reflective→counit-is-iso
_ = is-counit-iso→is-reflective
_ = is-equivalence

• Proposition 3.4.1:
  • (⇒). is-reflective→counit-is-iso
  • (⇐). is-counit-iso→is-reflective
• Definition 3.4.4: is-equivalence

3.5 Reflective subcategories🔗

_ = is-reflective

• Definition 3.5.2: is-reflective

3.6 Epireflective subcategories🔗

_ = is-epireflective
_ = epireflective+strong-mono→unit-invertible
_ = factor+strong-mono-unit-invertible→epireflective
_ = is-strong-epireflective
_ = strong-epireflective+mono→unit-invertible
_ = factor+mono-unit-invertible→strong-epireflective

• Definition 3.6.1: is-epireflective
• Proposition 3.6.2:
  • (1 ⇒ 2): epireflective+strong-mono→unit-invertible
  • (2 ⇒ 1): factor+strong-mono-unit-invertible→epireflective
• Definition 3.6.2: is-strong-epireflective
• Proposition 3.6.4:
  • (1 ⇒ 2): strong-epireflective+mono→unit-invertible
  • (2 ⇒ 1): factor+mono-unit-invertible→strong-epireflective

3.7 Kan extensions🔗

_ = is-lan
_ = is-ran
_ = cocomplete→lan
_ = ff→pointwise-lan-ext
_ = left-adjoint→preserves-lan
_ = is-initial-cocone→is-colimit
_ = is-colimit→is-initial-cocone
_ = is-colimit→is-initial-cocone
_ = adjoint→is-lan-id
_ = adjoint→is-absolute-lan

• Definition 3.7.1: is-lan
• Theorem 3.7.2: cocomplete→lan
• Proposition 3.7.3: ff→pointwise-lan-ext
• Proposition 3.7.4: left-adjoint→preserves-lan
• Proposition 3.7.5:
  • (⇒) is-initial-cocone→is-colimit
  • (⇐) is-colimit→is-initial-cocone
• Proposition 3.7.6:
  • (1 ⇒ 2) adjoint→is-lan-id, adjoint→is-absolute-lan

3.8 Tensor products of set-valued functors🔗

3.9 Exercises🔗

_ = right-adjoint→objectwise-rep
_ = corepresentable→left-adjoint
_ = Karoubi-is-completion

• Exercise 3.9.2:
  • (⇒) corepresentable→left-adjoint
  • (⇐) right-adjoint→objectwise-rep
• Exercise 3.9.3: Karoubi-is-completion

4 Generators and Projectives🔗

4.1 Well-powered categories🔗

4.2 Intersection and union🔗

4.3 Strong epimorphisms🔗

_ = is-regular-epi
_ = is-strong-epi
_ = ∘-is-strong-epic
_ = strong-epi-cancelr
_ = strong-epi+mono→invertible
_ = is-regular-epi→is-strong-epi
_ = is-strong-epi→is-extremal-epi
_ = equaliser-lifts→is-strong-epi
_ = is-extremal-epi→is-strong-epi

• Definition 4.3.1: is-regular-epi
• Definition 4.3.5: is-strong-epi
• Proposition 4.3.6:
  • 1. ∘-is-strong-epic
  • 2. strong-epi-cancelr
  • 3. strong-epi-mono→invertible
  • 4. is-regular-epi→is-strong-epi
  • 5. is-strong-epi→is-extremal-epi
• Proposition 4.3.7:
  • 1. equaliser-lifts→is-strong-epi
  • 2. is-extremal-epi→is-strong-epi

4.4 Epi-mono factorizations🔗

4.5 Generators🔗

_ = is-separating-family
_ = is-separator
_ = separating-family→epi
_ = epi→separating-family
_ = is-strong-separating-family
_ = is-regular-separating-family
_ = is-dense-separating-family
_ = is-dense-separator
_ = dense-separator→regular-separator
_ = regular-separator→strong-separator
_ = is-jointly-faithful
_ = is-jointly-conservative
_ = separating-family→jointly-faithful
_ = jointly-faithful→separating-family
_ = separator→faithful
_ = faithful→separator
_ = strong-separating-family→jointly-conservative
_ = lex+jointly-conservative→strong-separating-family
_ = strong-separator→conservative
_ = lex+conservative→strong-separator
_ = equalisers+jointly-conservative→separating-family
_ = dense-separating-family→jointly-ff
_ = jointly-ff→dense-separating-family
_ = zero+separating-family→separator

• Definition 4.5.1:
  • is-separating-family
  • is-separator
• Proposition 5.4.2:
  • (⇒) separating-family→epic
  • (⇐) epic→separating-family
• Definition 4.5.3:
  • is-strong-separating-family
  • is-regular-separating-family
• Definition 4.5.4:
  • is-dense-separating-family
  • is-dense-separator
• Proposition 4.5.5:
  • dense-separator→regular-separator
  • regular-separator→strong-separator
• Definition 4.5.7:
  • is-jointly-faithful
  • is-jointly-conservative
• Proposition 4.5.8:
  • (⇒) separating-family→jointly-faithful
  • (⇐) jointly-faithful→separating-family {.Agda}
• Proposition 4.5.9:
  • (⇒) separator→faithful
  • (⇐) faithful→separator
• Proposition 4.5.10:
  • (⇒) strong-separating-family→jointly-conservative
  • (⇐) lex+jointly-conservative→strong-separating-family
• Proposition 4.5.11:
  • (⇒) strong-separator→conservative
  • (⇐) lex+conservative→strong-separator
• Proposition 4.5.12: equalisers+jointly-conservative→separating-family
• Proposition 4.5.14
  • (⇒) dense-separating-family→jointly-ff
  • (⇐) jointly-ff→dense-separating-family
• Proposition 4.5.16: zero+separating-family→separator

4.6 Projectives🔗

_ = is-strong-projective
_ = preserves-strong-epis→strong-projective
_ = strong-projective→preserves-strong-epis
_ = indexed-coproduct-strong-projective
_ = retract→strong-projective
_ = Strong-projectives
_ = strong-projective-separating-faily→strong-projectives
_ = zero+indexed-coproduct-strong-projective→strong-projective

• Definition 4.6.1: is-strong-projective
• Proposition 4.6.2: Note that there is a slight typo in Borceux here: $\mathcal{C}(P,-)$ must preserve strong epimorphisms. (⇒) preserves-strong-epis→strong-projective (⇐) strong-projective→preserves-strong-epis
• Proposition 4.6.3: indexed-coproduct-strong-projective
• Proposition 4.6.4: retract→strong-projective
• Definition 4.6.5: Strong-projectives
• Proposition 4.6.6: strong-projective-separating-faily→strong-projectives
• Proposition 4.6.7:
  • (⇒) zero+indexed-coproduct-strong-projective→strong-projective
  • (⇐) indexed-coproduct-strong-projective

4.7 Injective cogenerators🔗

4.8 Exercises🔗

5 Categories of fractions🔗

5.1 Graphs and path categories🔗

_ = Graph
_ = Graph-hom
_ = Path-in
_ = Path-category
_ = Free-category
_ = Marked-graph
_ = Marked-graphs
_ = Marked-free-category

• Definition 5.1.1: Graph
• Definition 5.1.2: Graph-hom
• Definition 5.1.3: Path-in
• Proposition 5.1.4: Path-category, Free-category
• Definition 5.1.5: Marked-graph, Marked-graphs
• Proposition 5.1.6: Marked-free-category

5.2 Calculus of fractions🔗

_ = Localisation

• Proposition 5.2.2: Localisation

5.3 Reflective subcategories as categories of fractinos🔗

5.4 The orthogonal subcategory problem🔗

_ = Orthogonal
_ = object-orthogonal-!-orthogonal
_ = in-subcategory→orthogonal-to-inverted
_ = orthogonal-to-ηs→in-subcategory
_ = in-subcategory→orthogonal-to-ηs

• Definition 5.4.1: m⊥m
• Definition 5.4.2:
  1. Orthogonal
  2. Orthogonal
• Proposition 5.4.3: object-orthogonal-!-orthogonal
• Proposition 5.4.4:
  • • (a ⇒ b) in-subcategory→orthogonal-to-inverted
    • (a ⇒ c) in-subcategory→orthogonal-to-ηs

5.5 Factorisation systems🔗

_ = is-ofs
_ = factorisation-essentially-unique
_ = L-is-⊥R
_ = in-intersection≃is-iso

• Definition 5.5.1: is-factorisation-system
• Proposition 5.5.2: factorisation-essentially-unique
• Proposition 5.5.3: 🚧 E-is-⊥M
• Proposition 5.5.4:
  • 3. in-intersection≃is-iso

5.6 The case of localisations🔗

5.7 Universal closure operations🔗

5.8 The calculus of bidense morphisms🔗

5.9 Exercises🔗

6 Flat functors and Cauchy completeness🔗

6.1 Exact functors🔗

_ = is-lex

• Definition 6.1.1: is-lex

6.2 Left exact reflection of a functor🔗

6.3 Flat functors🔗

6.4 The relevance of regular cardinals🔗

6.5 The splitting of idempotents🔗

_ = is-idempotent
_ = is-split→is-idempotent
_ = is-split
_ = is-idempotent-complete

• Definition 6.5.1: is-idempotent
• Proposition 6.5.2: is-split→is-idempotent
• Definition 6.5.3: is-split
• Definition 6.5.8: is-idempotent-complete
• Proposition 6.5.9: Karoubi-is-completion

6.6 The more general adjoint functor theorem🔗

6.7 Exercises🔗

7 Bicategories and distributors🔗

7.1 2-categories🔗

7.2 2-functors and 2-natural transformations🔗

7.3 Modifications and n-categories🔗

7.4 2-limits and bilimits🔗

7.5 Lax functors and pseudo-functors🔗

7.6 Lax limits and pseudo-limits🔗

7.7 Bicategories🔗

_ = Prebicategory
_ = _⊣ᵇ_
_ = Spanᵇ

• Definition 7.7.1: Prebicategory
• Definition 7.7.2: _⊣ᵇ_
• Example 7.7.3: Spanᵇ

7.8 Distributors🔗

7.9 Cauchy completeness versus distributors🔗

7.10 Exercises🔗

8 Internal category theory🔗

8.1 Internal categories and functors🔗

_ = Internal-cat
_ = Internal-functor
_ = _=>i_
_ = Disci
_ = _^opi

• Definition 8.1.1: Internal-cat
• Definition 8.1.2: Internal-functor
• Definition 8.1.3: _=>i_
• Examples 8.1.6:
  • 1. Disci
  • 3. _^opi

8.2 Internal base-valued functors🔗

_ = Outer-functor
_ = _=>o_
_ = Outer-functors
_ = ConstO
_ = const-nato

• Definition 8.2.1: Outer-functor
• Definition 8.2.2: _=>o_
• Proposition 8.2.3: Outer-functors
• Example 8.2.4: ConstO, const-nato

8.3 Internal limits and colimits🔗

8.4 Exercises🔗

• Exercise 8.4.6:
  • (⇒) dependent-product→lcc
  • (⇐) lcc→dependent-product