ZFC.idr

module ZFC

class Set univ where
  member   : univ -> univ -> Type

data ExistsUnique : (a : Type) -> (P : a -> Type) -> Type where
  ExUniq_intro : {P : a -> Type} -> (x : a) -> P x -> ((y : a) -> P y -> x = y) -> ExistsUnique a P

getUniqWitness : {P : a -> Type} -> ExistsUnique a P -> a
getUniqWitness (ExUniq_intro a _ _) = a

getUniqProof : {P : a -> Type} -> (s : ExistsUnique a P) -> P (getUniqWitness s)
getUniqProof (ExUniq_intro _ p _) = p

uniqElim : {P : a -> Type} -> { b : a } -> (s : ExistsUnique a P) -> P b -> getUniqWitness s = b
uniqElim {b = b} (ExUniq_intro _ _ pf) pb = pf b pb

syntax [a] "∈" [b] = member a b
syntax [a] "∉" [b] = member a b -> _|_
syntax [a] "⊆" [b] = SubsetOf a b
syntax [a] "∧" [b] = Exists a (\_ => b)
syntax [a] "⇔" [b] = (a -> b) ∧ (b -> a)
syntax [a] "∨" [b] = Either a b
syntax "∃" {x} "∈" [c] ":" [body] = Exists _ (\x => ((x ∈ c) ∧ body))
syntax "∃"  {x} ":" [body] = Exists _ (\x => body)
syntax "∃!" {x} ":" [body] = ExistsUnique _ (\x => body)
syntax "∀" {x} ":" [body] = (x : _) -> body
syntax "∀" {x} "∈" [c] ":" [body] = ∀ x : ((x ∈ c) -> body)

data SubsetOf : {universe : Type} -> universe -> universe -> Type where
  MkSubSetOf : Set universe => {a : universe} -> {b : universe} -> ((c : universe) -> (c ∈ a) -> (c ∈ b)) -> SubsetOf a b

infixr 10 &&&
(&&&) : Type -> Type -> Type
(&&&) a b = Exists a (\_ => b)

class Set univ => Extensional univ where
  Extensionality : (a, b: univ) -> (a ⊆ b) -> (b ⊆ a) -> a = b
  EmptySet : ∃ O : {c : univ} -> (c ∉ O)

emptyset : Extensional univ => univ
emptyset = getWitness EmptySet

syntax "∅" = emptyset

class Extensional univ => HasPowerSet univ where
  PowerSet : (a : univ) -> ∃ Pa : ∀ c : (c ⊆ a) ⇔ (c ∈ Pa)

power : HasPowerSet univ => univ -> univ
power a = getWitness (PowerSet a)

class Extensional univ => HasPair univ where
  Pairing : (a : univ) -> (b : univ) -> ∃ c : ∀ z : ((z ∈ c) ⇔ ((z = a) ∨ (z = b)))

pair : HasPair univ => univ -> univ -> univ
pair a b = getWitness (Pairing a b)

singl : HasPair univ => univ -> univ
singl a = pair a a

syntax "{" [a] "}" = singl a
syntax "{" [a] "," [b] "}" = pair a b

class Extensional univ => HasSubset univ where
  Separation : (a : univ) -> (P : univ -> Type) -> ∃ c : ∀ b : (((b ∈ a) ∧ P b) ⇔ (b ∈ c))

syntax "{" {x} "∈" [a] "|" [body] "}" = getWitness (Separation a (\ x => body))

intersect : HasSubset univ => univ -> univ -> univ
intersect a b = { z ∈ a | z ∈ b }

syntax [a] "∩" [b] = intersect a b

class Extensional univ => HasUnion univ where
  Union : (a : univ) -> Exists univ (\c => (z : univ) -> ((Exists univ (\b => (b ∈ a) ∧ (z ∈ b))) ⇔  (z ∈ c)))

union : HasUnion univ => univ -> univ
union a = getWitness (Union a)

syntax [a] "∪" [b] = union ({ a , b })  
syntax [a] "≠" [b] = (a = b) -> _|_

class (HasSubset univ, HasPowerSet univ, HasUnion univ, HasPair univ) => Zermelo univ where
  Infinity : Exists univ (\c => (emptyset ∈ c) ∧ ((a : univ) -> (b : univ) -> (a ∈ c) -> (b ∈ c) -> ((pair a ({ b })) ∈ c) ))
  Foundation : (a : univ) -> (∃ y : y ∈ a) -> (∃ y : (y ∈ x) ∧ ((∃ z ∈ x : z ∈ y) -> _|_))

class Zermelo univ => ZF univ where
  Replacement : (a : univ) -> (F : univ -> univ)
               -> Exists univ (\z => (x : univ) -> ((x ∈ z) ⇔ ∃ b ∈ a : x = F b))

image : ZF univ => (univ -> univ) -> univ -> univ
image F a = getWitness (Replacement a F)
syntax [F] "[" [x] "]" = image F x