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

theory Relations : base:?Logic =
	include ☞arith:?NaturalArithmetics ❙
	include ?TypedSets ❙
	include ☞base:?ProductTypes ❙
	
	relation : type ⟶ type ⟶ type ❘ = [A,B] A ⟶ B ⟶ bool ❘ # relation 1 2 ❙ 
	relOn : type ⟶ type ❘ = [A] A ⟶ A ⟶ bool ❘ # relOn 1 ❙ 
	
	converse: {A,B} relation A B ⟶ relation B A ❘ = [A,B][R] [y,x] R x y❘ # converse 3 ❙
	relation_composition: {A,B,C} relation A B ⟶ relation B C  ⟶ relation A C ❘ = [A,B,C][R,S] [x,y] ∃[w] R x w ∧ S w y ❘ # 4 ^ 5 ❙
	range: {A,B} relation A B ⟶ set B ❘ # range 3 ❙
	// restriction: {A,B} relation A B ⟶ {C} relation C B  ❘ # 3 | 4 ❙
	prop_reflexive: {A} relOn A⟶ bool ❘ = [A][R] ∀[x] R x x❘ # reflexive 2 ❙
	prop_irreflexive: {A} relOn A⟶ bool ❘ = [A][R] ∀ [x] ¬ R x x❘ # irreflexive 2 ❙
	prop_symmetric: {A} relOn A⟶ bool ❘ = [A][R] ∀[x]∀[y] R x y ⇒ R y x❘ # symmetric 2 ❙
	prop_antisymmetric: {A} relOn A⟶ bool ❘ = [A][R] ∀[x]∀[y] R x y ∧ R y x ⇒ x ≐ y❘ # antisymmetric 2 ❙
	prop_asymmetric: {A} relOn A⟶ bool ❘ = [A][R] ∀[x]∀[y] R x y ⇒ ¬ R y x ❘ # asymmetric 2 ❙
	prop_total: {A} relOn A⟶ bool ❘ = [A][R] ∀[x]∀[y] x ≠ y ⇒ (R x y ∨ R y x)❘ # total 2 ❙
	prop_transitive: {A} relOn A⟶ bool ❘ = [A][R] ∀[x]∀[y]∀[z] R x y ∧ R y z ⇒ R x z❘ # transitive 2 ❙
	prop_equivalent: {A} relOn A⟶ bool ❘ = [A][R] (symmetric R) ∧ (transitive R) ∧ (reflexive R) ❘ # equivalent 2 ❙
	prop_preorder: {A} relOn A⟶ bool ❘ = [A][R] (reflexive R) ∧ (transitive R) ❘ # preorder 2 ❙
	// MiKo: I could not find any evidence for this name on the web
	prop_permutation: {A} relOn A⟶ bool ❘ = [A][R] (symmetric R) ∧ (transitive R) ❘ # permutation 2 ❙
	prop_commutes: {A} relOn A⟶ relOn A⟶ bool ❘ = [A,f,g] ∀ [x:A] ∀ [y:A] f x y ⇒ (∀ [z:A] g z y ⇒ ∃ [w:A] g w x ∧ f z w)  ❘ # 2 commute 3 ❙
	prop_preOrder: {A} relOn A⟶ bool ❘ = [A][R] (reflexive R) ∧ (transitive R) ❘ # preOrder 2 ❙
	prop_strictPreOrder: {A} relOn A⟶ bool ❘ = [A][R] (irreflexive R) ∧ (transitive R) ❘ # strictPreOrder 2 ❙
    prop_partialOrder: {A} relOn A⟶ bool ❘ = [A][R] (preOrder R) ∧ (antisymmetric R) ❘ # partialOrder 2 ❙
	prop_strictPartialOrder: {A} relOn A⟶ bool ❘ = [A][R] (irreflexive R) ∧ (transitive R) ❘ # strictPartialOrder 2 ❙
	prop_order: {A} relOn A⟶ bool ❘ = [A][R] (partialOrder R) ∧ (total R) ❘ # order 2 ❙
	prop_strictOrder: {A} relOn A⟶ bool ❘ = [A][R] (strictPartialOrder R) ∧ (total R) ❘ # strictOrder 2 ❙
    prop_linearOrder: {A} relOn A⟶ bool ❘ = [A][R] (partialOrder R) ∧ ∀ [a] ∀ [b] R a b ∨ R b a ❘ # linearOrder 2 ❙
    prop_wellfounded: {A} relOn A⟶ bool ❘ = [A][R] (partialOrder R) ∧ ∀ [B: set A] ∃ [b] b ∈ B ∧ ∀ [c] (R b c)  ❘ # wellfounded 2 ❙
    prop_wellOrder: {A} relOn A⟶ bool ❘ = [A][R] (linearOrder R) ∧ (wellfounded R)  ❘ # wellOrder 2 ❙
	// sameRelation: {A,B} relation A B ⟶ relation A B ⟶ bool ❘ = [A,B,f,g] (inclusion f g) ∧ (inclusion f g) ❘ # sameRelation 3 4 ❙
	
  	subrelation : {A,B} relation A B ⟶ relation A B ⟶ bool ❘ = [A,B][R,S] ∀ [x]∀[y] (R x y) ⇒ (S x y) ❘ # 3 sub 4 ❙
❚

theory RelationClosure : base:?Logic = 
  include ?Relations ❙
  include ?SetRelations ❙
  include ☞base:?DescriptionOperator ❙
  
  /T maybe factor out minimal-such-that? ❙
  closure :  {A} relOn A⟶ (relOn A⟶ bool) ⟶ relOn A❘
  	= [A,R,P] ι [S] R sub S ∧ P S ∧ ∀[T] (R sub T ∧ P T) ⇒ (S ≐ T) ❘ # closure 2 3❙ 
	symmetricClosure : {A} relOn A⟶ relOn A❘ = [A,R] closure R [x] symmetric x ❘ # symmetric_closure 2 ❙
	reflexiveClosure : {A} relOn A⟶relOn A❘ =  [A,R] closure R [x] reflexive x ❙
	transitiveClosure : {A} relOn A⟶relOn A❘ =  [A,R] closure R [x] transitive x ❙
  reflexiveTransitiveClosure  : {A} relOn A⟶ relOn A❘ = [A,R] closure R [r] reflexive r ∧ transitive r ❘ # 1^* ❙
  closureLemma : {A} ⊦ ∀[P : relOn A⟶ bool] ∀[R : relOn A] P (closure R P) ❙
  ❚
  
// theory QuotientSpace : base:?Logic = 
  include ?Relations ❙
  include ?PowerSet ❙
  include collections?Properties ❙
 
  // temporary workaround; use https://github.com/UniFormal/MMT/issues/358 later. ❙
  equivRel : type ❘ = {A} relOn A ❙
  equivalenceClass : {A} equivRel A ⟶ A ⟶ set A ❘ 
    = [A,R,a] ⟪ (fullset A) | ([x] R a x) ⟫ ❘
    # 3 _^ 2 ❙
  quotient : {A} set A ⟶ equivRel A ⟶ set (set A) ❘
    = [A,S,R] ⟪ (℘ (fullset A)) | ([T] ∀[x] x ∈ T ⇒ ∃[y] y ∈ S ∧ R x y) ⟫ ❘
    # 3 / 2 ❙
  projection : {A} equivRel ⟶ A ⟶ set A ❘
     = [A,R] [a] a _^ R ❘
    # π_2 ❙
  lemma_cover : {A} ⊦ ∀[R] ∀[S] S / R covers S ❙
  lemma_disjiont : {A} ⊦ ∀[R] ∀[S] ∀[X] ∀[Y] X ∈ S / R ∧ Y ∈ S ⇒ disjoint X Y ❙
  lemma_nonEmpty : {A} ⊦ ∀[R] ∀[S] ∀[X] X ∈ S / R ⇒ nonEmpty X ❙
❚
   
// Views to parametric theories are currently impossible; semantics is unclear ❙
// view PartitionQuotientspace : ?Partition -> ?Quotientspace  (R) =
  coll = quottientspace R ❙
  axiom_covers =  lemma_cover ❙
  axiom_nonEmpty =  lemma_nonEmtpy ❙
  axiom_pairwisedisjoint = lemma_disjoint ❙
❚