namespace http://mathhub.info/MitM/core/algebra ❚
import base http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/core/typedsets ❚

theory SemiLattice : base:?Logic = 
	include ☞base:?InformalProofs ❙
	include ☞ts:?Relations ❙
	include algebra/bands?Band❙
	
  theory semilattice_theory : base:?Logic = 
     include algebra/bands?Band/band_theory ❙
     
     axiom_commutative : ⊦ prop_commutative op ❙
     // order : U ⟶ U ⟶ bool ❘ = [a,b] a ≐ a ∘ b ❘ # 1 < 2 ❙
     // axiom_reflexive : ⊦ reflexive (order) ❘ = sketch "trivial" ❙
     // axiom_transitive : ⊦ transitive (order)❘ = sketch "trivial"  ❙
     // axiom_antisymmetric : ⊦ antisymmetric (order) ❘ = sketch "trivial" ❙
  ❚
  semilattice = Mod ☞?SemiLattice/semilattice_theory ❘ role abbreviation ❙
❚


// view POSetIsMeetSemiLattice : ?SemiLattice/semilattice_theory -> ts:?POSetBounds/posetBounds_theory =
  universe = universe ❙
  op = meet ❙                               
  axiom_idempotent = meetIdempotent ❙
  axiom_associative = meetAssociative ❙
  axiom_commutative = meetCommutative ❙
❚

// view POSetIsJoinSemiLattice : ?SemiLattice/semilattice_theory -> ts:?POSetBounds/posetBounds_theory =
  universe = universe ❙
  op = join ❙                               
  axiom_idempotent = joinIdempotent ❙
  axiom_associative = joinAssociative ❙
  axiom_commutative = joinCommutative ❙
❚

/T MiKo: probably need to say that the meet order is the same as the join-order, i.e. 
in theory SemiLattice/semilattice_theory
  biviewMeet : ⊢ SemilatticeIsPOSet (POSetIsMeetSemiLattice op ) ≐ op 
  biviewJoin : ⊢ SemilatticeIsPOSet (POSetIsJoinSemiLattice op ) ≐ op 

  and in 

theory ts:?POSet/poset_theory
  biviewMeet : ⊢ POSetIsMeetSemiLattice (SemilatticeIsPOSet ord ) ≐ ord 
  biviewMeet : ⊢ POSetIsMeetSemiLattice (SemilatticeIsPOSet ord ) ≐ ord 
❚

theory Lattice : base:?Logic = 
   include ?OperationProps ❙
   include ?SemiLattice ❙
   include ☞ts:?POSet ❙
   
   // implicit view SemilatticeIsPOSet : ts:?POSet/poset_theory -> ?SemiLattice/semilattice_theory =
    include ☞ts:?SetStructures ❙
   // ord = [a,b] a ≐ a ∘ b ❙
   // axiom_reflexive = sketch "trivial" ❙
   // axiom_transitive = sketch "trivial" ❙
   // axiom_antisymmetric = sketch "trivial" ❙


   include ☞ts:?SetStructures ❙
   
   theory lattice_theory : base:?Logic = 
   	include ☞ts:?SetStructures/setstruct_theory ❙
    implicit structure meetstruct : ?SemiLattice/semilattice_theory =
        universe = ☞ts:?SetStructures/setstruct_theory?universe ❙
        op @ meet ❘ # 1 ⊓ 2 ❙
    ❚
    structure joinstruct : ?SemiLattice/semilattice_theory =
        universe = ☞ts:?SetStructures/setstruct_theory?universe ❙
        op @ join ❘ # 1 ⊔ 2 ❙
        // order = ☞http://mathhub.info/MitM/core/typedsets?PrOSet/proset_theory?order ❙
    ❚
    prop_absorption1 : bool ❘ = prop_absorption meet join ❙
    prop_absorption2 : bool ❘ = prop_absorption join meet ❙
    axiom_absorption : ⊦ prop_absorption1 ∧ prop_absorption2 ❙
   ❚
   lattice = Mod ☞?Lattice/lattice_theory ❙
❚

theory DistributiveLattice : base:?Logic =
	include ?Lattice ❙
	include ?Ringoid ❙
  theory distributiveLattice_theory : base:?Logic = 
     include ?Lattice/lattice_theory ❙
     structure ringoid : ?Ringoid/ringoid_theory =
     	R = ☞ts:?SetStructures/setstruct_theory?universe ❙
        // plus = join ❙
        // times = meet ❙
     ❚
  ❚
  distributiveLattice = Mod ☞?DistributiveLattice/distributiveLattice_theory ❙
❚

theory BoundedLattice : base:?Logic = 
   include ?Lattice❙
   theory boundedLattice_theory : base:?Logic = 
      include ?Lattice/lattice_theory ❙
      top : U ❘ # ⊤ ❙
      bot : U❘ # ⊥ ❙
      // axiom_top : ⊦ ∀[a] a ≼ ⊤ ❙ // imported implicitly via SemilatticeIsPOSet ❙
      // axiom_bot : ⊦ ∀[a] ⊥ ≼ a ❙
   ❚
   boundedLattice = Mod ☞?BoundedLattice/boundedLattice_theory ❙
❚


theory ComplementedLattice : base:?Logic = 
   include ?BoundedLattice❙
   theory complementedLattice_theory : base:?Logic =
     include ?BoundedLattice/boundedLattice_theory ❙
     complement : U ⟶ U ⟶ bool ❘ = [a,c] a ⊔ c ≐ ⊤ ∧ a ⊓ c ≐ ⊥ ❘ # comp 1 2❙
     prop_complemented : bool ❘ = ∀[a] ∃[c] comp a c ❙
     axiom_complemented : ⊦ prop_complemented ❙
  ❚
  complementedLattice = Mod ☞?ComplementedLattice/complementedLattice_theory ❙
❚ 

theory BooleanAlgebra : base:?Logic =
  include ?ComplementedLattice❙
  include ?DistributiveLattice ❙
  theory booleanAlgebra_theory : base:?Logic = 
     include ?ComplementedLattice/complementedLattice_theory ❙
     include ?DistributiveLattice/distributiveLattice_theory ❙
  ❚
  booleanalgebra = Mod ☞?BooleanAlgebra/booleanAlgebra_theory ❙
❚