Commit 2023-01-25 09:05 6a60a653

View on Github →

feat: port data.pfunctor.univariate.basic (#1823)

Estimated changes

added def PFunctor.IdxCat
added def PFunctor.Obj
added def PFunctor.W.dest
added theorem PFunctor.W.dest_mk
added def PFunctor.W.head
added def PFunctor.W.mk
added theorem PFunctor.W.mk_dest
added def PFunctor.W
added def PFunctor.comp.mk
added def PFunctor.comp
added theorem PFunctor.fst_map
added theorem PFunctor.iget_map
added theorem PFunctor.liftp_iff'
added theorem PFunctor.liftp_iff
added theorem PFunctor.liftr_iff
added def PFunctor.map
added theorem PFunctor.supp_eq
added structure PFunctor