English
If F is a QPF and G is a type family with surjective and compatible maps FG_abs and FG_repr intertwining F and G, then G inherits a QPF structure via q.map and abs/repr transported along FG_abs and FG_repr. This transports a QPF structure across a surjective map.
Русский
Если F — QPF, а G — семейство типов с сюръективными и совместимыми переходами FG_abs и FG_repr, связывающими F и G, то G наследует структуру QPF через q.map и перенос abs/repr вдоль FG_abs и FG_repr.
LaTeX
$$$\\\\text{quotientQPF}(FG_{abs}_{repr}, FG_{abs}_{map}) : MvQPF G.$$$
Lean4
/-- If `F` is a QPF then `G` is a QPF as well. Can be used to
construct `MvQPF` instances by transporting them across
surjective functions -/
def quotientQPF (FG_abs_repr : ∀ {α} (x : G α), FG_abs (FG_repr x) = x)
(FG_abs_map : ∀ {α β} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x) : MvQPF G
where
P := q.P
abs p := FG_abs (abs p)
repr x := repr (FG_repr x)
abs_repr x := by rw [abs_repr, FG_abs_repr]
abs_map f p := by rw [abs_map, FG_abs_map]
