Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-10 17:35 960fc8e3

View on Github →

feat(data/univariate/qpf): compositional data type framework for (co)inductive types (#3325) Define univariate QPFs (quotients of polynomial functors). This is the first part of #3317.

Estimated changes

added def functor.liftp
added def functor.liftr
added theorem functor.of_mem_supp
added def functor.supp
added inductive pfunctor.M.agree'
added theorem pfunctor.M.agree'_refl
added theorem pfunctor.M.approx_mk
added theorem pfunctor.M.bisim'
added theorem pfunctor.M.bisim
added theorem pfunctor.M.bisim_equiv
added theorem pfunctor.M.cases_mk
added theorem pfunctor.M.cases_on_mk
added theorem pfunctor.M.children_mk
added theorem pfunctor.M.coinduction
added theorem pfunctor.M.corec_def
added def pfunctor.M.dest
added theorem pfunctor.M.dest_corec
added theorem pfunctor.M.dest_mk
added theorem pfunctor.M.eq_of_bisim
added theorem pfunctor.M.ext'
added theorem pfunctor.M.ext
added theorem pfunctor.M.ext_aux
added def pfunctor.M.head
added theorem pfunctor.M.head_mk
added theorem pfunctor.M.head_succ
added inductive pfunctor.M.is_path
added theorem pfunctor.M.iselect_nil
added theorem pfunctor.M.mk_dest
added theorem pfunctor.M.mk_inj
added def pfunctor.M
added structure pfunctor.M_intl
added inductive pfunctor.approx.agree
added inductive pfunctor.approx.cofix_a
added def pfunctor.Idx
added def pfunctor.W.dest
added theorem pfunctor.W.dest_mk
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.liftr_iff
added def pfunctor.map
added def pfunctor.obj
added structure pfunctor
added def qpf.Mcongr
added def qpf.W_setoid
added theorem qpf.Wequiv.abs'
added theorem qpf.Wequiv.refl
added theorem qpf.Wequiv.symm
added inductive qpf.Wequiv
added def qpf.Wrepr
added theorem qpf.Wrepr_equiv
added theorem qpf.cofix.bisim'
added theorem qpf.cofix.bisim
added theorem qpf.cofix.bisim_rel
added def qpf.cofix.corec
added def qpf.cofix.dest
added theorem qpf.cofix.dest_corec
added def qpf.cofix
added def qpf.comp
added theorem qpf.comp_map
added def qpf.corecF
added theorem qpf.corecF_eq
added def qpf.fix.dest
added theorem qpf.fix.dest_mk
added theorem qpf.fix.ind
added theorem qpf.fix.ind_aux
added theorem qpf.fix.ind_rec
added def qpf.fix.mk
added theorem qpf.fix.mk_dest
added def qpf.fix.rec
added theorem qpf.fix.rec_eq
added theorem qpf.fix.rec_unique
added def qpf.fix
added def qpf.fix_to_W
added theorem qpf.has_good_supp_iff
added theorem qpf.id_map
added theorem qpf.is_lawful_functor
added def qpf.is_precongr
added def qpf.is_uniform
added theorem qpf.liftp_iff'
added theorem qpf.liftp_iff
added theorem qpf.liftr_iff
added theorem qpf.mem_supp
added def qpf.quotient_qpf
added def qpf.recF
added theorem qpf.recF_eq'
added theorem qpf.recF_eq
added theorem qpf.recF_eq_of_Wequiv
added theorem qpf.supp_eq
added theorem qpf.supp_map
added def quot.factor
added theorem quot.factor_mk_eq
added theorem ext
added theorem ex.equivalence_foo.R
added def ex.foo.R
added def ex.foo.map
added theorem ex.foo.map_mk'
added theorem ex.foo.map_mk
added theorem ex.foo.map_tt
added def ex.foo.mk
added def ex.foo
added theorem ex.foo_not_uniform
added def ex.prod.pfunctor
added theorem ex.supp_mk_ff'
added theorem ex.supp_mk_ff₀
added theorem ex.supp_mk_ff₁
added theorem ex.supp_mk_tt'
added theorem ex.supp_mk_tt
added def qpf.box
added def qpf.liftp'
added def qpf.supp'