Theorems · Definition · category theory

CategoryTheory.Equivalence.induced

{D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] → {T : Type u_2} → (e : T ≃ D) → CategoryTheory.InducedCategory D ⇑e ≌ D

If T ≃ D is a bijection and D is a category, then InducedCategory D e is equivalent to D.

Defined in

Mathlib.CategoryTheory.EqToHom

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category