namespace http://mathhub.info/MitM/Foundation/sets ❚

import fnd http://mathhub.info/MitM/Foundation ❚

import rules scala://rules.mitm.mmt.kwarc.info ❚

theory SetTypeConversions : fnd:?Logic =
	include ?Sets ❙

	elem : set ⟶ type ❙
	asSet : type ⟶ set ❙
	setAsElem : {A,a} ⊦ a ∈ A ⟶ elem A ❘ # asTerm 1 2 %I3 ❙
	elemAsSet : {A : type} A ⟶ set ❘ # asElem 2❙

	axiom_asElemIsElem : {A,a : A} ⊦ (asElem a) ∈ (asSet A) ❙
	axiom_inverses1 : {s} ⊦ asSet (elem s) ≐ s ❘ role Simplify ❙
	axiom_inverses2 : {t} ⊦ elem (asSet t) ≐ t ❘ role Simplify ❙
	axiom_asTermElem1 : {A,a:A} ⊦ asTerm (asSet A) (asElem a) ≐ a ❘ role Simplify ❙
	axiom_asTermElem2 : {A,a,p:⊦a ∈ A} ⊦ asElem (asTerm A a) ≐ a ❘ role Simplify ❙

	// rule rules?SetCoercionRule ❙
❚

theory LiftSeparation : fnd:?Logic =
    include ?SetTypeConversions ❙
    include ?Separation ❙
    include ☞fnd:?Subtyping ❙

    axiom_sepIsPredSub : {s,P : set ⟶ prop} ⊦ elem ⟪ s | P ⟫ ≐ ⟨ x : (elem s) | ⊦ P (asElem x) ⟩ ❘ role Simplify ❙
    axiom_predSubIsSep : {t,P : t ⟶ prop} ⊦ asSet ⟨ x : t | ⊦ P x ⟩ ≐ ⟪ asSet t | ([x] P (asTerm (asSet t) x)) ⟫ ❘ role Simplify ❙
❚

theory LiftProduct : fnd:?Logic =
    include ?CartesianProduct ❙
    include ?KuratowskiPairs ❙
    include ?SetTypeConversions ❙
    include ☞fnd:?ProductTypes ❙

    // axiom_productType : {s,t} ⊦ elem (product s t) ≐ (elem s) × (elem t) ❘ role Simplify ❙
    rule rules?LiftProductType ❙
    axiom_productSet : {s,t} ⊦ asSet (s × t) ≐ product (asSet s) (asSet t) ❘ role Simplify ❙
    axiom_pairType : {s,t,S,T} ⊦ asTerm (product S T) (pair s t) ≐ ⟨ (asTerm S s) , (asTerm T t) ⟩ ❘ role Simplify ❙
    axiom_pairSet : {S,T,s : S,t : T} ⊦ asElem ⟨ s , t ⟩ ≐ pair (asElem s) (asElem t) ❘ role Simplify ❙
❚

// theory LiftRelations : fnd:?Logic =
    include ?Relations ❙
    include ?LiftProduct ❙


    axiom_relType : {a:set,b:set} ⊦ elem (℘ (product a b)) ≐ (elem a ⟶ elem b ⟶ prop) ❘ role Simplify ❙
    axiom_relSet : {A,B} ⊦ asSet (A ⟶ B ⟶ prop) ≐ ℘ (product (asSet A) (asSet B)) ❘ role Simplify ❙
    axiom_relType2 : {a:set,b:set,r: relation a b} ⊦ eq (elem a ⟶ elem b ⟶ prop) (asTerm (℘ (product a b)) r) ([x : elem a, y : elem b] (pair (asElem x) (asElem y)) ∈ r ) ❘ role Simplify ❙
    axiom_relSet2 : {A,B,R : A ⟶ B ⟶ prop} ⊦ asElem R ≐ ⟪ ℘ (product (asSet A) (asSet B)) | ([x] ∃[a] ∃[b] x ≐ pair a b ∧ R (asTerm (asSet A) a) (asTerm (asSet B) b) ) ⟫ ❘ role Simplify ❙
❚

theory LiftOmega : fnd:?Logic =
    include ?SetTypeConversions ❙
    include ?Infinity ❙
    include ☞fnd:?NatLiterals ❙

    axiom_lift_omega : ⊦ elem ω ≐ ℕ ❘ role Simplify ❙
    axiom_lift_Nat : ⊦ asSet ℕ ≐ ω ❘ role Simplify ❙
    axiom_lift_zero : ⊦ asTerm ω ∅ ≐ 0 ❘ role Simplify ❙
    axiom_lower_zero : ⊦ asElem 0 ≐ ∅ ❘ role Simplify ❙
    axiom_lift_succ : {n} ⊦ asTerm ω (set_succ n) ≐ succ_nat_lit (asTerm ω n) ❘ role Simplify ❙
    axiom_lower_succ : {n} ⊦ asElem (succ_nat_lit n) ≐ set_succ (asElem n) ❘ role Simplify ❙
❚