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

theory Properties : base:?Logic =
	include typedsets?SetCollection ❙
	
	prop_emptyInColl :  {G : type}collection G ⟶ prop ❘ = [G,C] ∅ ∈ C ❘ # prop_emptyInColl 2 ❙
	prop_fullInColl :  {G : type}collection G ⟶ prop ❘ = [G,C] (fullset G) ∈ C ❘ # prop_fullInColl 2 ❙
	prop_unionInColl : {G : type}collection G ⟶ prop ❘ = [G,C] ∀[S] S ⊑ C ⇒ UNION S ∈ C ❘ # prop_unionInColl 2 ❙
	prop_intersectionInColl : {G : type}collection G ⟶ prop ❘ = [G,C] ∀[S] S ⊑ C ∧ INTERSECT S ∈ C ❘ # prop_intersectionInColl  2❙
	prop_finiteIntersection : {G : type}collection G ⟶ prop ❘ = [G,C] ∀[A]∀[B] A ∈ C ∧ B ∈ C ⇒ (A ∩ B) ∈ C ❘ # prop_finiteIntersection 2❙
	prop_finiteUnion : {G : type}collection G ⟶ prop ❘ = [G,C] ∀[A]∀[B] A ∈ C ∧ B ∈ C ⇒ (A ∪ B) ∈ C ❘ # prop_finiteUnion 2❙
	prop_subsetClosed : {G : type}collection G ⟶ prop ❘ = [G,C] ∀[S] ∀[T] S ∈ C ∧ T ⊑ S ⇒ T ∈ C ❘ # prop_subsetClosed 2 ❙
	prop_cover : {G : type}collection G ⟶ set G ⟶ prop ❘ = [G,C,S] S ⊑ UNION C ❘ # 2 covers 3 ❙
	prop_subcover : {G : type}collection G ⟶ collection G ⟶ set G ⟶ prop ❘ = [G,C,D,S] C ⊑ D ∧ C covers S ❘ # 2 subcover 3 on 4 ❙
	prop_pairwiseDisjoint : {G : type}collection G ⟶ prop ❘ = [G,C] ∀[S] ∀[T] S ∈ C ∧ T ∈ C ⇒ disjoint S T ❘ # pairwiseDisjoint 2 ❙
	prop_closedUnderComplements : {G : type}collection G ⟶ prop ❘ = [G,C] ∀[S] (S ∈ C) ⇒ (compl S) ∈ C ❘ # prop_closedUnderComplements 2 ❙
❚

theory Partition : base:?Logic = 
  include ?Properties ❙
  include ☞base:?InformalProofs ❙

  prop_isPartition : {G : type} collection G ⟶ prop ❘
    = [G,C] C covers (fullset G) ∧ ¬ (prop_emptyInColl C) ∧ pairwiseDisjoint C ❘
	  # isPartition 2 ❙
	  
	theory partition_theory : base:?Logic > X : type ❘ =
		include typedsets?SetCollection/setColl_theory (X) ❙
		axiom_covers : ⊦ coll covers (fullset X) ❙
		axiom_nonEmpty : ⊦ ¬ (∅ ∈ coll) ❙
		axiom_pairwisedisjoint : ⊦ pairwiseDisjoint coll ❙
	❚
	partition = [X : type] Mod ☞?Partition/partition_theory (X) ❙
❚

// theory TaggedPartition : base:?Logic =
	include ?Partition ❙
	include ts:?TaggedCollectoin ❙
	
❚