Nuprl Definition : distributive-lattice-cat

BddDistributiveLattice ==
  Cat(ob = BoundedDistributiveLattice;
      arrow(G,H) = Hom(G;H);
      id(G) = λx.x;
      comp(G,H,K,f,g) = g o f)

Definitions occuring in Statement : bdd-distributive-lattice: BoundedDistributiveLattice, bounded-lattice-hom: Hom(l1;l2), mk-cat: mk-cat, compose: f o g, lambda: λx.A[x]
Definitions occuring in definition : bdd-distributive-lattice: BoundedDistributiveLattice, bounded-lattice-hom: Hom(l1;l2), lambda: λx.A[x], compose: f o g
FDL editor aliases : distributive-lattice-cat

Latex:
BddDistributiveLattice == Cat(ob = BoundedDistributiveLattice; arrow(G,H) = Hom(G;H); id(G) = \mlambda{}x.x; comp(G,H,K,f,g) = g o f) Date html generated: 2020_05_20-AM-09_00_07 Last ObjectModification: 2020_01_16-PM-05_04_31 Theory : lattices Home Index