Sigma.ext
theorem Sigma.ext : ∀ {α : Type u_1} {β : α → Type u_2} {x y : Sigma β}, x.fst = y.fst → HEq x.snd y.snd → x = y := by
sorry
This theorem, `Sigma.ext`, states that for any types `α` and `β` (where `β` is a function that takes a value of type `α` and returns a type), and any two elements `x` and `y` of the dependent pair type `Sigma β`, if the first components (`fst`) of `x` and `y` are equal and the second components (`snd`) of `x` and `y` are heterogeneously equal (HEq), then `x` is equal to `y`. In other words, it establishes that Sigma types, which are pairs consisting of a value and a value of a type dependent on the first, are equal if and only if both their components are correspondingly equal.
More concisely: If `x` and `y` are elements of the dependent pair type `Σβ` such that `fst x = fst y` and `HEq (snd x) (snd y)`, then `x = y`.
|
PUnit.ext
theorem PUnit.ext : ∀ (x y : PUnit.{u_1}), x = y
This theorem, `PUnit.ext`, states that for any two elements `x` and `y` of type `PUnit` in any universe `u_1`, `x` is equal to `y`. In other words, all elements of `PUnit` are equal to each other. This makes sense because `PUnit` is a type with only one element, typically denoted by `*`.
More concisely: For any `x, y : PUnit`, `x = y` holds in any universe `u_1`. (All elements of `PUnit` are equal.)
|
Prod.ext
theorem Prod.ext : ∀ {α : Type u_1} {β : Type u_2} {x y : α × β}, x.1 = y.1 → x.2 = y.2 → x = y
This theorem states that for any two pairs of types `α` and `β`, represented as `x` and `y`, if the first elements (accessed by `x.1` and `y.1`) of the pairs are equal and the second elements (accessed by `x.2` and `y.2`) of the pairs are also equal, then the pairs themselves (`x` and `y`) are equal.
More concisely: If `x` and `y` are pairs such that `x.1 = y.1` and `x.2 = y.2`, then `x = y`.
|