English
A specialization of sigmaSigmaSubtype where the second base is fixed by equality constraints is an equivalence with the fiber.
Русский
Специализация sigmaSigmaSubtype, где вторая база зафиксирована равенством, является эквивалентностью с волокном.
LaTeX
$$$\\text{Eq }(\\mathrm{sigmaSigmaSubtypeEq}\\ a\\ b) = \\mathrm{sigmaSigmaSubtypeEq}(a,b)$$$
Lean4
/-- A specialization of `sigmaSigmaSubtype` to the case where the second base
does not depend on the first, and the property being checked for is simple
equality. Useful e.g. when `γ` is `Hom` inside a category. -/
def sigmaSigmaSubtypeEq {α β : Type*} {γ : α → β → Type*} (a : α) (b : β) :
{ s : (a : α) × (b : β) × γ a b // s.1 = a ∧ s.2.1 = b } ≃ γ a b :=
have : Unique (@Subtype ((_ : α) × β) (fun ⟨a', b'⟩ ↦ a' = a ∧ b' = b)) :=
{ default := ⟨⟨a, b⟩, ⟨rfl, rfl⟩⟩
uniq := by rintro ⟨⟨a', b'⟩, ⟨rfl, rfl⟩⟩; rfl }
sigmaSigmaSubtype (fun ⟨a', b'⟩ ↦ a' = a ∧ b' = b) ⟨rfl, rfl⟩
