English
A structured way to interpret a 0-length arrow as a general arrow between any 0-length vectors, using a dependent type β and equalities to reindex.
Русский
Структурированный способ интерпретации стрелки между нулевой длиной векторов через зависимый тип β и равенства для перенумерации.
LaTeX
$$$$\\forall n, \\forall v,v',fs,\\; \\beta(v,v',fs)$$$$
Lean4
/-- cases distinction for an arrow in the category of 0-length type vectors -/
def typevecCasesNil₃ {β : ∀ v v' : TypeVec 0, v ⟹ v' → Sort*} (f : β Fin2.elim0 Fin2.elim0 nilFun) :
∀ v v' fs, β v v' fs := fun v v' fs => by
refine cast ?_ f
have eq₁ : v = Fin2.elim0 := by funext i; contradiction
have eq₂ : v' = Fin2.elim0 := by funext i; contradiction
have eq₃ : fs = nilFun := by funext i; contradiction
cases eq₁; cases eq₂; cases eq₃; rfl
