Wild category theory
Content created by Fredrik Bakke and Vojtěch Štěpančík.
Created on 2024-06-16.
Last modified on 2024-09-06.
{-# OPTIONS --guardedness #-}
Instances of wild categories
Wild category | File |
---|---|
Types | foundation.wild-category-of-types |
Pointed types | structured-types.wild-category-of-pointed-types |
Files in the wild category theory folder
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-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).