Theorems · Definition · category theory

CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.noConfusion

{P : Sort u_1} →
  {C : Type u} →
    {inst : CategoryTheory.Category.{v, u} C} →
      {F :
          CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
            (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)} →
        {ι : Type t} →
          {S : C} →
            {X : ι → C} →
              {f : (i : ι) → X i ⟶ S} →
                {D₁ D₂ : F.DescentDataAsCoalgebra f} →
                  {t : D₁.Hom D₂} →
                    {C' : Type u} →
                      {inst' : CategoryTheory.Category.{v, u} C'} →
                        {F' :
                            CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete C'ᵒᵖ)
                              (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)} →
                          {ι' : Type t} →
                            {S' : C'} →
                              {X' : ι' → C'} →
                                {f' : (i : ι') → X' i ⟶ S'} →
                                  {D₁' D₂' : F'.DescentDataAsCoalgebra f'} →
                                    {t' : D₁'.Hom D₂'} →
                                      C = C' →
                                        inst ≍ inst' →
                                          F ≍ F' →
                                            ι = ι' →
                                              S ≍ S' →
                                                X ≍ X' →
                                                  f ≍ f' →
                                                    D₁ ≍ D₁' →
                                                      D₂ ≍ D₂' →
                                                        t ≍ t' →
                                                          CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.noConfusionType
                                                            P t t'

Defined in

Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Cited by

0 results in Mathlib

Foundations

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