English
There is a canonical equivalence between the category of arrows in WalkingParallelFamily J and the type Option (Option J).
Русский
Существует каноническое эквивалентное отображение между категорией стрелок WalkingParallelFamily J и типом Option (Option J).
LaTeX
$$$$\\mathrm{Arrow}(\\mathrm{WalkingParallelFamily} \\ J) \\simeq \\mathrm{Option}(\\mathrm{Option}\\ J).$$$$
Lean4
/-- `Arrow (WalkingParallelFamily J)` identifies to the type obtained
by adding two elements to `T`. -/
def arrowEquiv : Arrow (WalkingParallelFamily J) ≃ Option (Option J)
where
toFun
f :=
match f.left, f.right, f.hom with
| zero, _, .id _ => none
| one, _, .id _ => some none
| zero, one, .line t => some (some t)
invFun
x :=
match x with
| none => Arrow.mk (𝟙 zero)
| some none => Arrow.mk (𝟙 one)
| some (some t) => Arrow.mk (.line t)
left_inv := by rintro ⟨(_ | _), _, (_ | _)⟩ <;> rfl
right_inv := by rintro (_ | (_ | _)) <;> rfl
