Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
67 lines (59 sloc) 2.04 KB
import Algebra.Magma
T Lattice {A : Type, s : Setoid(A)}
| lattice
{ meet : Op2(A)
, join : Op2(A)
, meet.commutative : Commutative(A,s,meet)
, meet.associative : Associative(A,s,meet)
, join.commutative : Commutative(A,s,join)
, join.associative : Associative(A,s,join)
, absorption : Absorption(A,s,meet,join)
}
T Semilattice {A : Type, s : Setoid(A)}
| semilattice
{ f : Op2(A)
, commutative : Commutative(A,s,f)
, associative : Associative(A,s,f)
, idempotent : Idempotent(A,s,f)
}
T BoundedLattice {A : Type, s : Setoid(A)}
| bounded_lattice
{ meet : Op2(A)
, join : Op2(A)
, e0 : A
, e1 : A
, meet.commutative : Commutative(A,s,meet)
, meet.associative : Associative(A,s,meet)
, meet.identity : Identity(A,s,meet,e1)
, join.commutative : Commutative(A,s,join)
, join.associative : Associative(A,s,join)
, join.identity : Identity(A,s,join,e0)
, absorption : Absorption(A,s,meet,join)
}
T ComplementedLattice {A : Type, s : Setoid(A)}
| complemeted_lattice
{ meet : Op2(A)
, join : Op2(A)
, e0 : A
, e1 : A
, meet.commutative : Commutative(A,s,meet)
, meet.associative : Associative(A,s,meet)
, meet.identity : Identity(A,s,meet,e1)
, meet.complement : Inverse(A,s,meet,e1,meet.identity)
, join.commutative : Commutative(A,s,join)
, join.associative : Associative(A,s,join)
, join.identity : Identity(A,s,join,e0)
, join.complement : Inverse(A,s,join,e0,join.identity)
, absorption : Absorption(A,s,meet,join)
}
T DistributiveLattice {A : Type, s : Setoid(A)}
| distributive_lattice
{ meet : Op2(A)
, join : Op2(A)
, meet.commutative : Commutative(A,s,meet)
, meet.associative : Associative(A,s,meet)
, join.commutative : Commutative(A,s,join)
, join.associative : Associative(A,s,join)
, absorption : Absorption(A,s,meet,join)
, distributive : Distributive(A,s,meet,join)
}
You can’t perform that action at this time.