Theorems · Theorem · category theory

Types.monoOverEquivalenceSet_inverse_map

∀ (α : Type u) {s t : Set α} (b : s ⟶ t),
  (Types.monoOverEquivalenceSet α).inverse.map b = CategoryTheory.MonoOver.homMk (TypeCat.ofHom fun w => ⟨↑w, ⋯⟩) ⋯

Defined in

Mathlib.CategoryTheory.Subobject.Types

Cited by

0 results in Mathlib

Foundations

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