English
A compatibility identity for a higher recursor hrecOn₂' when lifting from a single element x to a quotient qb in the second coordinate.
Русский
Совместимость при использовании рекурсора hrecOn₂' при подъёме из mk'' x к qb во второй координате.
LaTeX
$$$(\\operatorname{Quotient}.mk'' x).hrecOn₂'\\ qb\\ f\\ c = qb.hrecOn'(f x)\\ (\\lambda _ _ \\rightarrow c\\_\\_)$$$
Lean4
@[simp]
theorem hrecOn₂'_mk'' {φ : Quotient s₁ → Quotient s₂ → Sort*} (f : ∀ a b, φ (Quotient.mk'' a) (Quotient.mk'' b))
(c : ∀ a₁ b₁ a₂ b₂, a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ ≍ f a₂ b₂) (x : α) (qb : Quotient s₂) :
(Quotient.mk'' x).hrecOn₂' qb f c = qb.hrecOn' (f x) fun _ _ ↦ c _ _ _ _ (Setoid.refl _) :=
rfl
