Theorems · Definition · category theory

CategoryTheory.ReflQuiv.isoOfEquiv

{V W : Type u} →
  [inst : CategoryTheory.ReflQuiver V] →
    [inst_1 : CategoryTheory.ReflQuiver W] →
      (e : V ≃ W) →
        (he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)) →
          (∀ (X : V), (he X X) (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (e X)) →
            (CategoryTheory.ReflQuiv.of V ≅ CategoryTheory.ReflQuiv.of W)

Compatible equivalences of types and hom-types induce an isomorphism of reflexive quivers.

Defined in

Mathlib.CategoryTheory.Category.ReflQuiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.ReflQuiverCategoryTheory.ReflQuiver