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.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.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
- 1. Groups
Examples 1.2.6:
- 1. poset→category
- 1. Disc
- 1. B
Examples 1.2.7:
- 1. Slice
Examples 1.2.8:
- 1. Ab↪Sets
- 1. Hom[_,-]
- 1. 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
- 1. yo-naturalr
- 1. yo-naturall
Proposition 1.3.4: _◆_
Proposition 1.3.5: ◆-interchange
Examples 1.3.6:
- 1. よcov₁
- 1. constⁿ

1.4 Contravariant functors🔗

Borceux defines contravariant functors as a distinct object rather than functors from $C^{op};$ 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
- 1. よ₀
- 1. よ₁
- 1. よ

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
- 1. is-full
- 1. is-fully-faithful
- 1. is-precat-iso
Proposition 1.5.2:
- 1. よ-is-fully-faithful
- 1. よ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
- 1. Cod
- 1. θ
Definition 1.6.4: ∫cov
Definition 1.6.5: _×ᶜ_
Proposition 1.6.6: Cat⟨_,_⟩

1.7 Monomorphisms🔗

_ = is-monic
_ = id-monic
_ = 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
- 1. monic-∘
- 1. monic-cancell
Definition 1.7.3:
- 1. has-section
- 1. 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
_ = 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
- 1. epic-∘
- 1. 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
- 1. invertible-∘
- 1. 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
- 1. 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
- 1. is-initial
Examples 2.3.2:
- 1. Sets-initial, Sets-terminal
- 1. 🚧 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
- 1. 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:
- 1. Limit→Equaliser, Equaliser→Limit
- 1. 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:
- 1. with-equalisers
- 1. 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🔗

Warning

Borceux uses some outdated terminology here, and also uses a condition that is overly powerful. We opt to stick with the terminology from the nLab instead.

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

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

_ = 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
- 1. make-free-group
- 1. 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→left-extension
_ = 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→left-extension
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

_ = is-regular-epi
_ = is-strong-epi
_ = strong-epi-∘
_ = 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. strong-epi-∘
- 1. strong-epi-cancelr
- 1. strong-epi-mono→invertible
- 1. is-regular-epi→is-strong-epi
- 1. is-strong-epi→is-extremal-epi
Proposition 4.3.7:
- 1. equaliser-lifts→is-strong-epi
- 1. 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🔗

Warning

Borceux uses the term “projective” to refer to strong 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: $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

_ = 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🔗

_ = m⊥m
_ = m⊥o
_ = o⊥m
_ = 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. m⊥o
2. o⊥m
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-factorisation-system
_ = factorisation-essentially-unique
_ = E-is-⊥M
_ = 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:
- 1. in-intersection≃is-iso

_ = is-lex

Definition 6.1.1: is-lex

_ = 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

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

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

_ = 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
- 1. _^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

marked graph homomorphism

It also serves as an excellent place to find possible contributions!↩︎

References

Borceux, Francis. 1994. Handbook of Categorical Algebra. Vol. 1. Encyclopedia of Mathematics and Its Applications. Cambridge University Press. https://doi.org/10.1017/CBO9780511525858.