Homotopy Type Theory Heyting algebra > history (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Contents

< Heyting algebra

Definition

A Heyting algebra is a distributive lattice (L,,,,,)(L, \leq, \bot, \vee, \top, \wedge) with

  • a function :L×LtoL\implies: L \times L to L

  • a family of dependent terms

    a:L,b:L(ba)aba:L, b:L \vdash (b \to a) \wedge a \leq b
  • a family of dependent terms

    a:L,b:Lab(ab)a:L, b:L \vdash a \leq b \to (a \wedge b)

representing the carteisan closed condition for the lattice.

See also

Last revised on June 9, 2022 at 19:23:54. See the history of this page for a list of all contributions to it.