English
Lifting a relation through map: given a relation R betweenβ and β', the map respects R via the lifted relation LiftR'.
Русский
Поднять отношение через map: отображение сохраняет отношение R через LiftR'.
LaTeX
$$$\\forall \\alpha \\beta, F', [MvFunctor F'] [LawfulMvFunctor F'], R:\\; \\beta \\otimes \\beta \\Rightarrow Prot, x:\\; F'\\alpha, f,g:\\; \\alpha \\Rightarrow \\beta, h:\\; \\alpha \\Rightarrow Subtype_{R}, hh:\\; subtypeVal _ \\circ h = (f \\otimes' g) \\circ \\mathrm{prod.diag} \\Rightarrow \\, LiftR' R (f <$$> x) (g <$$> x).$$$
Lean4
theorem liftR_map {α β : TypeVec n} {F' : TypeVec n → Type u} [MvFunctor F'] [LawfulMvFunctor F']
(R : β ⊗ β ⟹ «repeat» n Prop) (x : F' α) (f g : α ⟹ β) (h : α ⟹ Subtype_ R)
(hh : subtypeVal _ ⊚ h = (f ⊗' g) ⊚ prod.diag) : LiftR' R (f <$$> x) (g <$$> x) :=
by
rw [LiftR_def]
exists h <$$> x
rw [MvFunctor.map_map, comp_assoc, hh, ← comp_assoc, fst_prod_mk, comp_assoc, fst_diag]
rw [MvFunctor.map_map, comp_assoc, hh, ← comp_assoc, snd_prod_mk, comp_assoc, snd_diag]
dsimp [LiftR']; constructor <;> rfl
