English
For α countable, the hom-sets in the small category structure on Morphisms are countable.
Русский
Для α счетной, гом-наборы в малой категории Морфизмы счётны.
LaTeX
$$$\operatorname{Countable}(\mathrm{Hom} \text{(HomAsType)}(\alpha))$$$
Lean4
/-- An isomorphism in `Dial C` can be induced by isomorphisms on the source and target,
which respect the respective relations on `X` and `Y`.
-/
@[simps]
def isoMk {X Y : Dial C} (e₁ : X.src ≅ Y.src) (e₂ : X.tgt ≅ Y.tgt)
(eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel) : X ≅ Y
where
hom :=
{ f := e₁.hom
F := π₂ ≫ e₂.inv
le := by rw [eq, ← Subobject.pullback_comp]; apply le_of_eq; congr; ext <;> simp }
inv :=
{ f := e₁.inv
F := π₂ ≫ e₂.hom
le := by rw [eq, ← Subobject.pullback_comp]; apply le_of_eq; congr; ext <;> simp }
