# 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

```
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
```

```
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
```

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

```
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
```

`propUnit : isProp unit`

```
setUnit : isSet unit
```