1: \begin{abstract}

2:   This is a foundation for algebraic geometry, developed internal to the Zariski topos, building on the work of Kock and Blechschmidt (\cite{kock-sdg}[I.12], \cite{ingo-thesis}).

3:   The Zariski topos consists of sheaves on the site opposite to the category of finitely presented algebras over a fixed ring, with the Zariski topology, i.e.\ generating covers are given by localization maps $A\to A_{f_1}$ for finitely many elements $f_1,\dots,f_n$ that generate the ideal $(1)=A\subseteq A$.

4:   We use homotopy type theory together with three axioms as the internal language of a (higher) Zariski topos.

5: 

6:   One of our main contributions is the use of higher types -- in the homotopical sense -- to define and reason about cohomology.

7:   Actually computing cohomology groups, seems to need a principle along the lines of our ``Zariski local choice'' axiom,

8:   which we justify as well as the other axioms using a cubical model of homotopy type theory.

9: \end{abstract}

10: