Set Theory

Other disputed foundations for set theory could be taken as: ZFC, NBG, ETCS. We will disctinct syntetically: i) category theory; ii) set theory in univalent foundations; iii) topos theory, grothendieck topos, elementary topos.

Here is the -groupoid model of sets.

(Mere proposition, ). A type P is a mere proposition if for all we have :

(0-type). A type A is a 0-type is for all and we have .

(1-type). A type A is a 1-type if for all and and , we have .

(A set of elements, ). A type A is a if for all and , we have :

. If A is a set then A is a 1-type.

data N = Z  | S (n: N)

n_grpd (A: U) (n: N): U = (a b: A) -> rec A a b n where
   rec (A: U) (a b: A) : (k: N) -> U
     = split { Z -> Path A a b ; S n -> n_grpd (Path A a b) n }

isContr (A: U): U = (x: A) * ((y: A) -> Path A x y)
isProp  (A: U): U = n_grpd A Z
isSet   (A: U): U = n_grpd A (S Z)

PROP  : U = (X:U) * isProp X
SET   : U = (X:U) * isSet X

(-Contractability). if fiber is set then path space between any sections is contractible.

setPi  (A: U) (B: A -> U) (h: (x: A) -> isSet (B x)) (f g: Pi A B)
       (p q: Path (Pi A B) f g)
     : Path (Path (Pi A B) f g) p q

(-Contractability). if fiber is set then is set.

setSig (A:U) (B: A -> U) (sA: isSet A)
       (sB : (x:A) -> isSet (B x)) : isSet (Sigma A B)

(Unit type, ). The unit is a type with one element.

data unit = tt
unitRec (C: U) (x: C): unit -> C = split tt -> x
unitInd (C: unit -> U) (x: C tt): (z:unit) -> C z = split tt -> x

( is a proposition).

propUnit : isProp unit

( is a set).

setUnit : isSet unit