feat(data/quot): add `map'`, `hrec_on'`, and `hrec_on₂'` (#3148)
feat(data/quot): add `map'`, `hrec_on'`, and `hrec_on₂'` (#3148)

Also add a few `simp` lemmas





leanprover-community/mathlib,leanprover-community/mathlib