Wild category theory
Content created by Fredrik Bakke and Vojtěch Štěpančík.
Created on 2024-06-16.
Last modified on 2024-09-23.
{-# OPTIONS --guardedness #-}
Instances of wild categories
| Wild category | File |
|---|---|
| Types | foundation.wild-category-of-types |
| Pointed types | structured-types.wild-category-of-pointed-types |
Modules in the wild category theory namespace
module wild-category-theory where open import wild-category-theory.colax-functors-noncoherent-large-wild-higher-precategories public open import wild-category-theory.colax-functors-noncoherent-wild-higher-precategories public open import wild-category-theory.isomorphisms-in-noncoherent-large-wild-higher-precategories public open import wild-category-theory.isomorphisms-in-noncoherent-wild-higher-precategories public open import wild-category-theory.maps-noncoherent-large-wild-higher-precategories public open import wild-category-theory.maps-noncoherent-wild-higher-precategories public open import wild-category-theory.noncoherent-large-wild-higher-precategories public open import wild-category-theory.noncoherent-wild-higher-precategories public
Recent changes
- 2024-09-23. Fredrik Bakke. Some typos, wording improvements, and brief prose additions (#1186).
- 2024-09-06. Fredrik Bakke. Define the noncoherent wild precategory of pointed types (#1179).
- 2024-06-16. Fredrik Bakke and Vojtěch Štěpančík. Noncoherent wild higher precategories (#1099).