English
A subtype of a dependent triple which pins down both bases is equivalent to the respective fiber.
Русский
Подтип зависимого тройного типа, фиксирующий обе основы, эквивалентен соответствующему волокну.
LaTeX
$$$ { s : (a : \\alpha) \\times (b : \\beta a) \\times \\gamma a b // p s.1 } \\simeq \\gamma a b $$$
Lean4
/-- A subtype of a dependent triple which pins down both bases is equivalent to the
respective fiber. -/
@[simps! +simpRhs apply]
def sigmaSigmaSubtype {α : Type*} {β : α → Type*} {γ : (a : α) → β a → Type*} (p : (a : α) × β a → Prop)
[uniq : Unique { ab // p ab }] {a : α} {b : β a} (h : p ⟨a, b⟩) :
{ s : (a : α) × (b : β a) × γ a b // p ⟨s.1, s.2.1⟩ } ≃ γ a b :=
calc
{ s : (a : α) × (b : β a) × γ a b // p ⟨s.1, s.2.1⟩ }
_ ≃ _ :=
(subtypeEquiv (p := fun ⟨a, b, c⟩ ↦ p ⟨a, b⟩) (q := (p ·.1)) (sigmaAssoc γ).symm fun s ↦ by simp [sigmaAssoc])
_ ≃ _ := (subtypeSigmaEquiv _ _)
_ ≃ _ := (uniqueSigma (fun ab ↦ γ (Sigma.fst <| Subtype.val ab) (Sigma.snd <| Subtype.val ab)))
_ ≃ γ a b := Equiv.cast <| by rw [← show ⟨⟨a, b⟩, h⟩ = uniq.default from uniq.uniq _]
