@[reducible, inline]

abbrev CategoryTheory.Grpd.chosenTerminal : Grpd

The chosen terminal object in Grpd.

Equations

• CategoryTheory.Grpd.chosenTerminal = CategoryTheory.Grpd.of (CategoryTheory.Discrete PUnit.{?u.2 + 1})

def CategoryTheory.Grpd.chosenTerminalIsTerminal : Limits.IsTerminal chosenTerminal

The chosen terminal object in Grpd is terminal.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Grpd.prodCone (C D : Grpd) : Limits.BinaryFan C D

The chosen product of categories C × D yields a product cone in Grpd.

Equations

• C.prodCone D = CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Prod.fst ↑C ↑D) (CategoryTheory.Prod.snd ↑C ↑D)

def CategoryTheory.Grpd.isLimitProdCone (X Y : Grpd) : Limits.IsLimit (X.prodCone Y)

The product cone in Grpd is indeed a product.

Equations

• X.isLimitProdCone Y = CategoryTheory.Limits.BinaryFan.isLimitMk (fun (S : CategoryTheory.Limits.BinaryFan X Y) => CategoryTheory.Functor.prod' S.fst S.snd) ⋯ ⋯ ⋯

instance CategoryTheory.Grpd.instCartesianMonoidalCategory_groupoidModel : CartesianMonoidalCategory Grpd

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Grpd.id_eq_id (X : Grpd) : CategoryStruct.id X = Functor.id ↑X

The identity in the category of groupoids equals the identity functor.

theorem CategoryTheory.Grpd.comp_eq_comp {X Y Z : Grpd} (F : X ⟶ Y) (G : Y ⟶ Z) : CategoryStruct.comp F G = Functor.comp F G

Composition in the category of groupoids equals functor composition.

theorem CategoryTheory.Grpd.eqToHom_obj {C1 C2 : Grpd} (x : ↑C1) (eq : C1 = C2) : (eqToHom eq).obj x = cast ⋯ x

@[simp]

theorem CategoryTheory.Grpd.map_id_obj {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {x : Γ} {a : ↑(A.obj x)} : (A.map (CategoryStruct.id x)).obj a = a

@[simp]

theorem CategoryTheory.Grpd.map_id_map {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {x : Γ} {a b : ↑(A.obj x)} {f : a ⟶ b} : (A.map (CategoryStruct.id x)).map f = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp f (eqToHom ⋯))

@[simp]

theorem CategoryTheory.Grpd.map_comp_obj {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {x y z : Γ} {f : x ⟶ y} {g : y ⟶ z} {a : ↑(A.obj x)} : (A.map (CategoryStruct.comp f g)).obj a = (A.map g).obj ((A.map f).obj a)

@[simp]

theorem CategoryTheory.Grpd.map_comp_map {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {x y z : Γ} {f : x ⟶ y} {g : y ⟶ z} {a b : ↑(A.obj x)} {φ : a ⟶ b} : (A.map (CategoryStruct.comp f g)).map φ = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((A.map g).map ((A.map f).map φ)) (eqToHom ⋯))

theorem CategoryTheory.Grpd.map_comp_map' {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {x y z : Γ} {f : x ⟶ y} {g : y ⟶ z} {a b : ↑(A.obj x)} {φ : a ⟶ b} : (A.map g).map ((A.map f).map φ) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((A.map (CategoryStruct.comp f g)).map φ) (eqToHom ⋯))

@[simp]

theorem CategoryTheory.Grpd.id_obj {C : Grpd} (X : ↑C) : (CategoryStruct.id C).obj X = X

@[simp]

theorem CategoryTheory.Grpd.comp_obj {C D E : Grpd} (F : C ⟶ D) (G : D ⟶ E) (X : ↑C) : (CategoryStruct.comp F G).obj X = G.obj (F.obj X)

theorem CategoryTheory.Grpd.map_eqToHom_obj {Γ : Type u} [Category.{v, u} Γ] (F : Functor Γ Grpd) {x y : Γ} (h : x = y) (t : ↑(F.obj x)) : (F.map (eqToHom h)).obj t = cast ⋯ t

theorem CategoryTheory.Grpd.eqToHom_hom_aux {C1 C2 : Grpd} (x y : ↑C1) (eq : C1 = C2) : (x ⟶ y) = ((eqToHom eq).obj x ⟶ (eqToHom eq).obj y)

This is the proof of equality used in the eqToHom in Grpd.eqToHom_hom

theorem CategoryTheory.Grpd.eqToHom_hom {C1 C2 : Grpd} {x y : ↑C1} (f : x ⟶ y) (eq : C1 = C2) : (eqToHom eq).map f = cast ⋯ f

This is the turns the hom part of eqToHom functors into a cast

@[simp]

theorem CategoryTheory.Grpd.map_eqToHom_map {Γ : Type u} [Category.{v, u} Γ] (F : Functor Γ Grpd) {x y : Γ} (h : x = y) {t s : ↑(F.obj x)} (f : t ⟶ s) : (F.map (eqToHom h)).map f = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (cast ⋯ f) (eqToHom ⋯))

@[simp]

theorem CategoryTheory.Grpd.eqToHom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F G : Functor C D) (h : F = G) (X : C) : (eqToHom h).app X = eqToHom ⋯