naming help

Stream: general

[Sean Leather]

What names would you give these definitions?

universes u v

def unknown₁ {α : Type u} (β : α → Type v) : Prop :=
∀ ⦃s t : sigma β⦄ (h : s.1 = t.1), (eq.rec_on h s.2 : β t.1) = t.2

def unknown₂ {α₁ α₂ : Type u} {β₁ : α₁ → Type v} {β₂ : α₂ → Type v} (f : sigma β₁ → sigma β₂) : Prop :=
∀ ⦃s t : sigma β₁⦄, (f s).1 = (f t).1 → s.1 = t.1

[Sean Leather]

The first says a sigma β should be considered a function: equal arguments (fsts) produce equal results (snds).

[Sean Leather]

The second says that a function on sigmas preserves (injective) equality on the fsts.