Commit 2026-09-03 15:14 af188809

View on Github →

chore(Data/PFunctor): fix defeq abuse in PFunctor.Obj (#43056) Fix defeq abuse with PFunctor.Obj by using explicit constructors and destructors.

Estimated changes

added theorem Functor.Comp.mk_run
added theorem Functor.Comp.run_mk
added theorem PFunctor.Obj.eta
added def PFunctor.Obj.fst
added theorem PFunctor.Obj.fst_mk
added def PFunctor.Obj.mk
added def PFunctor.Obj.rec
added theorem PFunctor.Obj.rec_mk
added def PFunctor.Obj.snd
added theorem PFunctor.Obj.snd_mk
modified def PFunctor.map
modified theorem PFunctor.M.children_mk
modified def PFunctor.M.dest
modified theorem PFunctor.M.head_mk