English
If a functor F with the QPF structure satisfies a compatibility condition on mapConst, then F is a lawful functor: map_const, id_map, and comp_map satisfy the functor laws.
Русский
Если функтор F с QPF-структурой удовлетворяет условию совместимости для mapConst, то F — законный функтор: выполняются законы map_const, id_map, comp_map.
LaTeX
$$$LawfulFunctor F = \\{ map_{const}, id_{map}, comp_{map} \\}$ with the given compatibility condition.$$
Lean4
theorem lawfulFunctor (h : ∀ α β : Type u, @Functor.mapConst F _ α _ = Functor.map ∘ Function.const β) :
LawfulFunctor F :=
{ map_const := @h
id_map := @id_map F _
comp_map := @comp_map F _ }
/-
Lifting predicates and relations
-/
