English
Given Z: J → Sort*, and transport rules along morphisms, one can transport an element x: Z(j0) to Z(j) for any j.
Русский
Для Z: J → Sort* и правил переноса вдоль морфизмов можно перенести элемент x: Z(j0) в Z(j).
LaTeX
$$$\\lbrack IsPreconnected(J) \\rbrack \\Rightarrow \\forall Z:\\, J\\to\\mathrm{Sort}^*,\\, (h_1,h_2)\\Rightarrow \\forall x:\\, Z(j_0), \\; \\exists\\,\\text{Nonempty}(Z(j)).$$$
Lean4
/-- Another induction principle for `IsPreconnected J`:
given a type family `Z : J → Sort*` and
a rule for transporting in *both* directions along a morphism in `J`,
we can transport an `x : Z j₀` to a point in `Z j` for any `j`.
-/
theorem isPreconnected_induction [IsPreconnected J] (Z : J → Sort*) (h₁ : ∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), Z j₁ → Z j₂)
(h₂ : ∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), Z j₂ → Z j₁) {j₀ : J} (x : Z j₀) (j : J) : Nonempty (Z j) :=
(induct_on_objects {j | Nonempty (Z j)} ⟨x⟩ (fun f => ⟨by rintro ⟨y⟩; exact ⟨h₁ f y⟩, by rintro ⟨y⟩; exact ⟨h₂ f y⟩⟩)
j :)
