Theorems · Theorem · category theory

CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient_symm_apply

∀ {G : Type v} [inst : Group G] (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u))
  (a : Quot ⇑(MulAction.orbitRel G (J.obj (CategoryTheory.SingleObj.star G)))),
  (CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient J).symm a =
    Quot.lift (fun x => Quot.mk J.ColimitTypeRel ⟨CategoryTheory.SingleObj.star G, x⟩) ⋯ a

Defined in

Mathlib.CategoryTheory.Limits.Shapes.SingleObj

Cited by

0 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Group