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

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

theory TypedSets : fnd:?Logic =
	 // include base:?Lists ❙
  include ?SetTypeConversions ❙
  include ?Powerset ❙
  include ?Separation ❙
  include ☞fnd:?Subtyping ❙
  /T the type operator of sets along with its constructors ❙
  setOf: type ⟶ type ❘ = [A] ⟨ x : set | ⊦ x ∈ (℘ (asSet A)) ⟩ ❙
  fromPred : {A : type} (A ⟶ prop) ⟶ setOf A ❘ = [A,P] ⟪ ℘ (asSet A) | ([x] P (asTerm (asSet A) x)) ⟫ ❘ # asSet 2 ❙
  asPred : {A} setOf A ⟶ A ⟶ prop ❘ = [A,s] [x] (asElem x) ∈ s ❘ # asPred 2 ❙

  // setCons: {A} A ⟶ set A ⟶ set A ❘ = [A] [a,P] [x] P x ∨ x ≐ a❘ # 3 <- 2 ❙
  // setList : {A} List A ⟶  set A ❘ # ≪ 2 ≫ ❙
  // inSet : {A : type} A ⟶ set A ⟶ prop ❘ = [A][a,P] P a ❘ # 2 ∈ 3 ❙
  // bsetst : {A} set A ⟶ (A ⟶ prop) ⟶ set A ❘ = [A][P,Q] [x] P x ∧ Q x ❘ # ⟪ 2 | 3 ⟫ ❙
  // fullset : {A} set A ❘ = [A] [x] true ❘ # fullset 1 ❙
   // TODO, need a lot of congruence rules that make sure that setcons ACI ❙
❚