Theorems · Theorem · category theory

Types.monoOverEquivalenceSet_unitIso

∀ (α : Type u),
  (Types.monoOverEquivalenceSet α).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun f =>
        CategoryTheory.MonoOver.isoMk (Equiv.ofInjective ⇑(CategoryTheory.ConcreteCategory.hom f.obj.hom) ⋯).toIso ⋯)
      ⋯

Defined in

Mathlib.CategoryTheory.Subobject.Types

Cited by

0 results in Mathlib

Foundations

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