Pregroupoids
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-09-21.
Last modified on 2023-09-13.
module category-theory.pregroupoids where
Imports
open import category-theory.isomorphisms-in-precategories open import category-theory.precategories open import foundation.dependent-pair-types open import foundation.propositions open import foundation.universe-levels
Idea
A pregroupoid is a precategory in which every morphism is an isomorphism.
Definition
is-groupoid-Precategory-Prop : {l1 l2 : Level} (C : Precategory l1 l2) → Prop (l1 ⊔ l2) is-groupoid-Precategory-Prop C = Π-Prop ( obj-Precategory C) ( λ x → Π-Prop ( obj-Precategory C) ( λ y → Π-Prop ( type-hom-Precategory C x y) ( λ f → is-iso-Precategory-Prop C f))) is-groupoid-Precategory : {l1 l2 : Level} (C : Precategory l1 l2) → UU (l1 ⊔ l2) is-groupoid-Precategory C = type-Prop (is-groupoid-Precategory-Prop C) Pregroupoid : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) Pregroupoid l1 l2 = Σ (Precategory l1 l2) is-groupoid-Precategory
Recent changes
- 2023-09-13. Fredrik Bakke and Egbert Rijke. Refactor structured monoids (#761).
- 2023-05-06. Egbert Rijke. Big cleanup throughout library (#594).
- 2023-04-28. Fredrik Bakke. Miscellaneous refactoring and small additions (#579).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490).