English
There is a dual induction principle for costructured arrows, mirroring the structured arrow induction, adapted to the opposite setup.
Русский
Существует двойственное индуктивное принцип для costructured стрелок, соответствующее индукции по структурированной стрелке, адаптированное к противному окружению.
LaTeX
$$$\forall P:\text{CostructuredArrow}(L)(L\!\mathrm{obj}Y)\to\mathrm{Prop},\ P(\text{CostructuredArrow.mk}(\mathrm{id}_{L Y})) \Rightarrow \cdots \Rightarrow \forall g\; P(g)$$$
Lean4
@[elab_as_elim]
theorem induction_costructuredArrow (hP₀ : P (CostructuredArrow.mk (𝟙 (L.obj Y))))
(hP₁ :
∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y),
P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk (L.map f ≫ φ)))
(hP₂ :
∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y),
P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk ((isoOfHom L W w hw).inv ≫ φ)))
(g : CostructuredArrow L (L.obj Y)) : P g :=
by
let g' := StructuredArrow.mk (T := L.op) (Y := op g.left) g.hom.op
change P (CostructuredArrow.mk g'.hom.unop)
induction g' using induction_structuredArrow L.op W.op with
| hP₀ => exact hP₀
| hP₁ f φ hφ => exact hP₁ f.unop φ.unop hφ
| hP₂ w hw φ hφ => simpa [isoOfHom_op_inv L W w hw] using hP₂ w.unop hw φ.unop hφ
