Contents

foundations

(0,1)-category

(0,1)-topos

# Contents

## Idea

A family of axioms depending on parameters.

Axiom schemata are formalized in a deductive system by the use of inference rules which have hypotheses. For example, the axiom schema of replacement in set theory is given by the following inference rule:

$\frac{\Gamma, x, y \vdash \phi(x, y) \; \mathrm{prop} \quad \Gamma \vdash a \quad \Gamma \vdash \forall x.(x \in a) \implies \exists! y.\phi(x, y) \; \mathrm{true}}{\Gamma \vdash \{y \vert \exists x.(x \in a) \implies \phi(x, y)\}}$

Compare with the bare notion of axiom, which are inference rules without any hypotheses.

## Examples

$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A, y:B(x) \vdash P(x, y) \; \mathrm{type}}{\Gamma \vdash \mathrm{ac}_{A, B, P}:(\mathrm{isSet}(A) \times \Pi x:A.(\mathrm{isSet}(B(x)) \times \Pi y:B(x).\mathrm{isProp}(P(x, y)))) \to ((\exists y:B(x).P(x, y)) \to (\exists g:(\Pi x:A.B(x)).\Pi x:A.P(x, g(x))))}$