namespace http://mathhub.info/MitM/core/typedsets ❚
import base http://mathhub.info/MitM/Foundation ❚
import ar http://mathhub.info/MitM/core/arithmetics ❚

theory PrOSet : base:?Logic = 
	include ?Relations ❙
	include ☞base:?NaturalDeduction ❙
	include ☞base:?InformalProofs ❙
	include ?AllSets ❙
	
  theory proset_theory : base:?Logic = 
     include ?SetStructures/setstruct_theory ❙
     ord : U ⟶ U ⟶ bool ❘ # 1 ≼ 2  prec 5 ❙
     axiom_reflexive : ⊦ reflexive ord ❙
     axiom_transitive : ⊦ transitive ord ❙
     lemma_preOrder : ⊦ preOrder ord ❘ = and_introduction axiom_reflexive axiom_transitive ❙
     strictord : U ⟶ U ⟶ bool ❘ = [a,b] ord a b ∧ ¬ a ≐ b ❘ # 1 ≺ 2 prec 5 ❙
     strict_lemma : ⊦ strictPreOrder strictord ❘ = sketch "by construction" ❙
     
     prop_upperBound : set U ⟶ U ⟶ bool ❘ = [S,b] ∀[s] S s ⇒ (s ≼ b) ❙
     prop_lowerBound : set U ⟶ U ⟶ bool ❘ = [S,b] ∀[s] S s ⇒ (b ≼ s) ❙
     prop_directed : bool ❘ = ∀[a] ∀[b] ∃[c] a ≼ c ∧ b ≼ c ❙
     prop_directedSubset : (U ⟶ bool) ⟶ bool ❘ = [F] ∀[a] ∀[b] F a ∧ F b ⇒ ∃[c] F c ∧ a ≼ c ∧ b ≼ c ❙
   ❚
  proset = Mod ☞?PrOSet/proset_theory ❘ role abbreviation ❙
❚  

theory LeastMost : base:?Logic = 
   include ☞base:?DescriptionOperator ❙
   include ?Relations ❙
	include ?AllSets ❙
	
    prop_isLeast : {A : type} A ⟶ (A ⟶ bool) ⟶ (A ⟶ A ⟶ bool) ⟶ bool ❘ = [A,x,P,R] P x ∧ ∀[y] P y ⇒ R x y ❘ # isLeast 2 3 4 ❙ 
    least : {A : type} (A ⟶ bool) ⟶ (A ⟶ A ⟶ bool) ⟶ A ❘ = [A,P,R] ι [x] isLeast x P R ❘ # least 2 3❙   
    prop_isGreatest : {A : type} A ⟶ (A ⟶ bool) ⟶ (A ⟶ A ⟶ bool) ⟶ bool ❘ = [A,x,P,R] isLeast x P (converse R) ❘ # isGreatest 2 3 4 ❙ 
    greatest : {A : type} (A ⟶ bool) ⟶ (A ⟶ A ⟶ bool) ⟶ A ❘ = [A,P,R] ι [x] isGreatest x P R ❘ # greatest 2 3❙
    // least/greatest assume that there is a unique least element. Instead minimal/maximal return a set of minimal elements (a singleton
    // if there is a unique one). ❙
    minimal: {A : type} (A ⟶ bool) ⟶ (A ⟶ A ⟶ bool) ⟶ set A ❘ = [A,P,R] ι [s] ∀[x] x ∈ s ⇒ isLeast x P R ❘ # minimal 2 3❙
    maximal: {A : type} (A ⟶ bool) ⟶ (A ⟶ A ⟶ bool) ⟶ set A ❘ = [A,P,R] ι [s] ∀[x] x ∈ s ⇒ isGreatest x P R ❘ # maximal 2 3❙
    
❚

theory DirectedSet : base:?Logic =
	include algebra?OperationProps ❙
	include ☞base:?InformalProofs ❙
	include ?LeastMost ❙
	include ?PrOSet ❙
	
	theory directedSet_theory : base:?Logic =
   		include ?PrOSet/proset_theory ❙
   		lub : set U ⟶ U ❘ = [S] least (prop_upperBound S) ord ❙
   		glb : set U ⟶ U ❘ = [S] greatest (prop_lowerBound S) ord ❙
   		meet : U ⟶ U ⟶ U ❘ = [a,b] lub [x] x ≐ a ∧ x ≐ b ❙
   		join : U ⟶ U ⟶ U ❘ = [a,b] glb [x] x ≐ a ∨ x ≐ b ❙
      axiom_directed : ⊦ prop_directed ❙
   		meetIdenpotent : ⊦ prop_idempotent meet ❘ =  sketch "by idempotence of conjunction" ❙
   		meetAssociative : ⊦ prop_associative meet ❘ = sketch "by associativity of conjunction" ❙
   		meetCommutative : ⊦ prop_commutative meet ❘ = sketch "by commutativity of conjunction" ❙
   		joinIdempotent : ⊦ prop_idempotent join ❘ =  sketch "by idempotence of disjunction" ❙
   		joinAssociative : ⊦ prop_associative join ❘ = sketch "by associativity of disjunction" ❙
   		joinCommutative : ⊦ prop_commutative join ❘ = sketch "by commutativity of disjunction" ❙
   ❚
   directedSet = Mod ☞?DirectedSet/directedSet_theory ❘ role abbreviation ❙
❚

theory Fixpoints : base:?Logic =
	include ?AllSets ❙
	isFixpoint: {A:type, f:A ⟶ A, a:A} prop ❘ = [A,f,a] f a  ≐  a ❙
	fixpoints: {A:type} (A ⟶ A) ⟶ set A ❘ = [A,f] ι [s] ∀[x] x ∈ s ⇒ isFixpoint A f x ❙
❚

theory POSet : base:?Logic = 
  include ?PrOSet ❙
  
  theory poset_theory : base:?Logic = 
     include ?PrOSet/proset_theory ❙
     axiom_antisymmetric : ⊦ antisymmetric ord ❙
     lemma_partialOrder : ⊦ partialOrder ord ❘ = and_introduction lemma_preOrder axiom_antisymmetric❙
     strict_lemma : ⊦ strictPartialOrder strictord ❘ = sketch "by construction" ❙
  ❚
  poset = Mod ☞?POSet/poset_theory ❘ role abbreviation ❙
❚

theory SupremumReal : base:?Logic =
	include ?AllSets ❙
	include ?LeastMost ❙
	include ☞ar:?ExtendedReals ❙
		
	supremumReal : set ℝ ⟶ ℝ❘= [s] least ([a] ∀[x] x ∈ s ⇒ x ≤ a)  ([a,b] a ≤ b)   ❘# supR 1 ❙
❚