Theorems · Definition · category theory

CategoryTheory.Bicategory.Equivalence.noConfusionType

Sort u →
  {B : Type u₁} →
    [inst : CategoryTheory.Bicategory B] →
      {a b : B} →
        CategoryTheory.Bicategory.Equivalence a b →
          {B' : Type u₁} →
            [inst' : CategoryTheory.Bicategory B'] → {a' b' : B'} → CategoryTheory.Bicategory.Equivalence a' b' → Sort u

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory