Commit 2023-02-06 07:35 aa15ae0f

View on Github →

feat: port Order.Heyting.Hom (#2077) @[protect_proj] is currently unimplemented. Other than that, dangerous instances fixed in the standard way and not much else interesting going on here.

Estimated changes

added theorem BiheytingHom.coe_comp
added theorem BiheytingHom.coe_copy
added theorem BiheytingHom.coe_id
added theorem BiheytingHom.comp_id
added theorem BiheytingHom.copy_eq
added theorem BiheytingHom.ext
added theorem BiheytingHom.id_apply
added theorem BiheytingHom.id_comp
added structure BiheytingHom
added theorem CoheytingHom.coe_comp
added theorem CoheytingHom.coe_copy
added theorem CoheytingHom.coe_id
added theorem CoheytingHom.comp_id
added theorem CoheytingHom.copy_eq
added theorem CoheytingHom.ext
added theorem CoheytingHom.id_apply
added theorem CoheytingHom.id_comp
added structure CoheytingHom
added theorem HeytingHom.cancel_left
added theorem HeytingHom.coe_comp
added theorem HeytingHom.coe_copy
added theorem HeytingHom.coe_id
added def HeytingHom.comp
added theorem HeytingHom.comp_apply
added theorem HeytingHom.comp_assoc
added theorem HeytingHom.comp_id
added theorem HeytingHom.copy_eq
added theorem HeytingHom.ext
added theorem HeytingHom.id_apply
added theorem HeytingHom.id_comp
added structure HeytingHom
added theorem map_bihimp
added theorem map_compl
added theorem map_hnot
added theorem map_symmDiff