def CategoryTheory.NatTrans.isoOfCodGroupoid {A : Type u} [Category.{v, u} A] {B : Type u₁} [Groupoid B] {F G : Functor A B} (h : NatTrans F G) : F ≅ G

Equations

• h.isoOfCodGroupoid = { hom := h, inv := { app := fun (a : A) => CategoryTheory.Groupoid.inv (h.app a), naturality := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.isoOfCodGroupoid_inv_app {A : Type u} [Category.{v, u} A] {B : Type u₁} [Groupoid B] {F G : Functor A B} (h : NatTrans F G) (a : A) : h.isoOfCodGroupoid.inv.app a = Groupoid.inv (h.app a)

@[simp]

theorem CategoryTheory.NatTrans.isoOfCodGroupoid_hom {A : Type u} [Category.{v, u} A] {B : Type u₁} [Groupoid B] {F G : Functor A B} (h : NatTrans F G) : h.isoOfCodGroupoid.hom = h

def CategoryTheory.NatTrans.inv {A : Type u} [Category.{v, u} A] {B : Type u₁} [Groupoid B] {F G : Functor A B} (h : NatTrans F G) : G ⟶ F

Equations

• h.inv = h.isoOfCodGroupoid.inv

@[simp]

theorem CategoryTheory.NatTrans.inv_vcomp {A : Type u} [Category.{v, u} A] {B : Type u₁} [Groupoid B] {F G : Functor A B} (h : NatTrans F G) : vcomp h.inv h = NatTrans.id G

@[simp]

theorem CategoryTheory.NatTrans.vcomp_inv {A : Type u} [Category.{v, u} A] {B : Type u₁} [Groupoid B] {F G : Functor A B} (h : NatTrans F G) : h.vcomp h.inv = NatTrans.id F

theorem CategoryTheory.NatTrans.hext {A : Type u} [Category.{v, u} A] {B : Type u₁} [Groupoid B] {F F' G G' : Functor A B} (α : F ⟶ G) (β : F' ⟶ G') (hF : F = F') (hG : G = G') (happ : ∀ (x : A), α.app x ≍ β.app x) : α ≍ β

instance CategoryTheory.instGroupoidFunctor_hoTTLean {A : Type u_1} [Category.{u_3, u_1} A] {B : Type u_2} [Groupoid B] : Groupoid (Functor A B)

Equations

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