OPEN Formalize Borceux Vol. 1
This task tracks our progress on formalizing the Handbook of Categorical Algebra 1.
TODO [#A] Examples 1.2.5 example topology analysis
TODO [#B] Examples 1.2.6 example
TODO [#C] Examples 1.2.7 example
TODO [#B] Examples 1.2.8 example
TODO [#A] Examples 1.3.6 example analysis
TODO [#A] Examples 1.4.3 example ag
TODO [#C] Proposition 1.6.3 proposition
OPEN [#C] Definition 1.7.5 definition
This is preservation/reflection of monos; we just need to update the page!
TODO [#A] Examples 1.7.7 example analysis topology
TODO [#A] Examples 1.8.5 example analysis topology
TODO [#A] Examples 1.9.6 example analysis topology
TODO [#A] Examples 1.10.3 example topology
TODO [#C] Exercises 1.11.2 exercise
TODO [#C] Exercises 1.11.3 exercise
TODO [#C] Exercises 1.11.4 exercise
TODO [#B] Exercises 1.11.7 exercise
TODO [#B] Exercises 1.11.10 exercise
TODO [#C] Exercises 1.11.12 exercise
TODO [#A] Examples 2.1.7 example topology analysis
TODO [#A] Examples 2.2.4 example topology analysis
TODO [#A] Examples 2.4.6 example topology analysis
TODO [#A] Proposition 2.7.1 proposition taboo
TODO [#B] Proposition 2.8.3 proposition
TODO [#B] Definition 2.8.4 definition
TODO [#B] Proposition 2.8.5 proposition
TODO [#A] Example 2.8.6 example analysis topology
TODO [#C] Proposition 2.9.2 proposition
TODO [#B] Proposition 2.9.8 proposition
TODO [#C] Proposition 2.9.9 proposition
TODO [#A] Examples 2.9.10 example topology analysis
TODO [#C] Definition 2.10.1 definition
TODO [#C] Proposition 2.10.2 proposition
TODO [#A] Examples 2.10.3 example fields
TODO [#C] Proposition 2.11.3 proposition
TODO [#C] Proposition 2.11.4 proposition
TODO [#C] Corollary 2.11.5 proposition
TODO [#C] Proposition 2.12.1 proposition
TODO [#C] Examples 2.12.2 borceux 1lab example
TODO [#A] Definition 2.13.1 definition filtered
This is the definition of a filtered category, which really should be filtered.
TODO [#A] Proposition 2.13.2 proposition filtered
TODO [#A] Proposition 2.13.3 proposition filtered
TODO [#A] Theorem 2.13.4 proposition filtered
TODO [#A] Proposition 2.13.5 proposition filtered
TODO [#A] Corollary 2.13.6 proposition filtered
TODO [#A] Proposition 2.13.7 proposition filtered
TODO [#A] Examples 2.13.8 example filtered
TODO [#A] Counterexample 2.13.9 example filtered topology
TODO [#C] Theorem 2.14.2 proposition
TODO [#C] Corollary 2.15.3 proposition
TODO [#C] Corollary 2.15.4 proposition filtered
TODO [#C] Proposition 2.15.5 proposition
TODO [#C] Examples 2.15.7 proposition
TODO [#C] Proposition 2.16.1 proposition
TODO [#C] Corollary 2.16.2 proposition
TODO [#C] Proposition 2.16.3 proposition
TODO [#C] Exercise 2.17.1 exercise
TODO [#C] Exercise 2.17.2 exercise
TODO [#C] Exercise 2.17.4 exercise
TODO [#C] Exercise 2.17.5 exercise
TODO [#C] Exercise 2.17.6 exercise
TODO [#C] Exercise 2.17.7 exercise
TODO [#C] Exercise 2.17.9 exercise
TODO [#C] Exercise 2.17.10 exercise
TODO [#C] Proposition 3.2.3 proposition
TODO [#C] Proposition 3.2.4 proposition
TODO [#C] Proposition 3.3.1 borceux 1lab proposition
TODO [#B] Theorem 3.3.4 proposition
TODO [#C] Corollary 3.3.5 proposition
TODO [#C] Corollary 3.3.6 proposition
TODO [#C] Corollary 3.3.7 proposition
TODO [#C] Corollary 3.3.8 proposition
TODO [#A] Examples 3.3.9 example topology analysis
TODO [#C] Proposition 3.4.2 proposition
TODO [#C] Proposition 3.4.3 proposition
TODO [#C] Proposition 3.4.5 proposition
TODO [#C] Definition 3.5.1 definition
TODO [#C] Proposition 3.5.3 proposition
TODO [#C] Definition 3.5.5 definition
TODO [#C] Definition 3.5.6 definition
TODO [#A] Proposition 3.5.7 proposition
TODO [#C] Proposition 3.8.1 borceux 1lab proposition
TODO [#C] Exercise 3.9.1 exercise
TODO [#C] Exercise 3.9.2 exercise
TODO [#C] Exercise 3.9.3 exercise
TODO [#C] Exercise 3.9.4 exercise
TODO [#C] Exercise 3.9.5 exercise
TODO [#C] Exercise 3.9.6 exercise
TODO [#C] Exercise 3.9.7 exercise
TODO [#C] Definition 4.1.1 borceux 1lab definition
TODO [#B] Definition 4.1.2 definition
The definition in Borceux uses is the set-theoretic definition of a well-powered category, which does not work very nicely in type-theoretic settings.