Homotopy Type Theory Heyting algebra > history (Rev #2)

Contents

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

Revision on April 20, 2022 at 20:22:14 by Anonymous?. See the history of this page for a list of all contributions to it.