Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-08 03:03 51cbe888

View on Github →

feat(order/category/HeytAlg): The category of Heyting algebras (#16250) Define HeytAlg, the category of Heyting algebras with Heyting morphisms.

Estimated changes

Modified src/order/category/BoolAlg.lean

Created src/order/category/HeytAlg.lean

added theorem HeytAlg.coe_of

added def HeytAlg.iso.mk

added def HeytAlg.of

added def HeytAlg