English
A specialized extensionality lemma for 1-step arrows with left/right data and a middle morphism equality.
Русский
Специализированная лемма экстенциональности для стрел уровня 1 с данными слева/справа и равенством среднего морфизма.
LaTeX
$$$\forall {F G : ComposableArrows C 1} (left : F.left = G.left) (right : F.right = G.right) (w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom right.symm), F = G$$$
Lean4
/-- Auxiliary definition for the action on maps of the functor `F.precomp f`.
It sends `0 ≤ 1` to `f` and `i + 1 ≤ j + 1` to `F.map' i j`. -/
def map : ∀ (i j : Fin (n + 1 + 1)) (_ : i ≤ j), obj F X i ⟶ obj F X j
| ⟨0, _⟩, ⟨0, _⟩, _ => 𝟙 X
| ⟨0, _⟩, ⟨1, _⟩, _ => f
| ⟨0, _⟩, ⟨j + 2, hj⟩, _ => f ≫ F.map' 0 (j + 1)
| ⟨i + 1, hi⟩, ⟨j + 1, hj⟩, hij => F.map' i j (by simpa using hij)
