Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_hom_app_f

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  (ι : Type u_2) [inst_1 : Unique ι] {X S : C} (f : X ⟶ S) (X_1 : ↑(F.obj { as := Opposite.op S }).obj),
  ((CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso ι f).hom.app X_1).f =
    CategoryTheory.CategoryStruct.id ((F.map f.op.toLoc).l.toFunctor.obj X_1)

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryUnique