Built with
Alectryon. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl.
(** * Groupoid, the precategory of strict groupoid categories *)
Require Import Functor.Core Category.Strict.
Require Import Cat.Core.
Require Import GroupoidCategory.Core.
Require Import Functor.Paths.
Set Implicit Arguments.
Generalizable All Variables.
Local Open Scope functor_scope.
Section groupoid_cat.
Context `{Funext}.
Let P : PreCategory -> Type
:= fun C => IsGroupoid C /\ IsStrictCategory C.
Let HF : forall C D, P C -> P D -> IsHSet (Functor C D)
:= fun C D HC HD => @trunc_functor _ C D _ (snd HD) _.
(** There is a full precategory of [cat] which is the strict groupoid precategories *)
Definition groupoid_cat : PreCategory
:= @sub_pre_cat _ P HF.
End groupoid_cat.