Lean4
/-- composition of qpfs gives another qpf -/
def comp : QPF (Functor.Comp F₂ F₁) where
P := PFunctor.comp q₂.P q₁.P
abs
{α} := by
dsimp [Functor.Comp]
intro p
exact abs ⟨p.1.1, fun x => abs ⟨p.1.2 x, fun y => p.2 ⟨x, y⟩⟩⟩
repr
{α} := by
dsimp [Functor.Comp]
intro y
refine ⟨⟨(repr y).1, fun u => (repr ((repr y).2 u)).1⟩, ?_⟩
dsimp [PFunctor.comp]
intro x
exact (repr ((repr y).2 x.1)).snd x.2
abs_repr
{α} := by
dsimp [Functor.Comp]
intro x
conv =>
rhs
rw [← abs_repr x]
obtain ⟨a, f⟩ := repr x
dsimp
congr with x
rcases h' : repr (f x) with ⟨b, g⟩
dsimp; rw [← h', abs_repr]
abs_map {α β}
f := by
dsimp +unfoldPartialApp [Functor.Comp, PFunctor.comp]
intro p
obtain ⟨a, g⟩ := p; dsimp
obtain ⟨b, h⟩ := a; dsimp
symm
trans
· symm
apply abs_map
congr
rw [PFunctor.map_eq]
dsimp [Function.comp_def]
congr
ext x
rw [← abs_map]
rfl
