\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{cohesive homotopy type theory} \begin{quote}% under construction \end{quote} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory} [[!include type theory - contents]] \hypertarget{cohesive_toposes}{}\paragraph*{{Cohesive $\infty$-Toposes}}\label{cohesive_toposes} [[!include cohesive infinity-toposes - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{TheAxioms}{The Axioms}\dotfill \pageref*{TheAxioms} \linebreak \noindent\hyperlink{a_codiscrete_objects}{A) Codiscrete objects}\dotfill \pageref*{a_codiscrete_objects} \linebreak \noindent\hyperlink{b_discrete_objects}{B) Discrete objects}\dotfill \pageref*{b_discrete_objects} \linebreak \noindent\hyperlink{c_cohesion}{C) Cohesion}\dotfill \pageref*{c_cohesion} \linebreak \noindent\hyperlink{example_phenomena}{Example phenomena}\dotfill \pageref*{example_phenomena} \linebreak \noindent\hyperlink{GeometricSpacesAndTheirHomotopyTypes}{Geometric spaces and their cohesive homotopy types}\dotfill \pageref*{GeometricSpacesAndTheirHomotopyTypes} \linebreak \noindent\hyperlink{Structures}{Structures in cohesive homotopy type theory}\dotfill \pageref*{Structures} \linebreak \noindent\hyperlink{cohomology}{Cohomology}\dotfill \pageref*{cohomology} \linebreak \noindent\hyperlink{flat_cohomology_and_local_systems}{Flat cohomology and local systems}\dotfill \pageref*{flat_cohomology_and_local_systems} \linebreak \noindent\hyperlink{de_rham_cohomology}{de Rham cohomology}\dotfill \pageref*{de_rham_cohomology} \linebreak \noindent\hyperlink{differential_cohomology}{Differential cohomology}\dotfill \pageref*{differential_cohomology} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{References}{References}\dotfill \pageref*{References} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} \emph{Cohesive homotopy type theory} is an [[axiom|axiomatic]] [[theory]] of [[higher geometry]], the pairing of [[geometry]] in general and of [[differential geometry]] in particular with [[homotopy theory]]. The \emph{[[objects]]} or \emph{[[types]]} that it describes are \emph{[[cohesive topos|cohesive]] [[homotopy types]]}, hence [[cohesive ∞-groupoids]], such as for instance [[smooth ∞-groupoids]]. See also at \emph{[[motivation for cohesive toposes]]} for a non-technical discussion. To the extent that plain [[homotopy type theory]] is a formalization of [[homotopy theory]] in that it is the [[internal language of an (∞,1)-topos]], \emph{cohesive} homotopy type theory is the [[internal logic|internal language]] of a \emph{[[cohesive (∞,1)-topos]]}. One way to arrive at cohesive homotopy type theory is to start with the external axioms for [[cohesive toposes|cohesion]] on a given [[topos]] in terms of an [[adjoint quadruple]] of functors \emph{on} the given [[topos]] and attempt to formulate them instead in the [[internal logic|internal]] [[Mitchell-Bénabou language|Mitchell-Bénabou]] [[type theory]] language of the topos. This fails, since for formulating the [[reflective subcategories]] of [[discrete objects]] and [[codiscrete objects]] internally one needs instead of the [[type of propositions]] a full [[type of types]], as exists only in [[homotopy type theory]]. Passing to this, the axioms for cohesion can be formulated (\hyperlink{ShulmanInternalizing}{Shulman}) and are automatically that of [[cohesive (∞,1)-topos|homotopy cohesion]]. \hypertarget{TheAxioms}{}\subsection*{{The Axioms}}\label{TheAxioms} We discuss the formulation in [[homotopy type theory]] of the \href{http://ncatlab.org/nlab/show/cohesive+%28infinity%2C1%29-topos#InternalDefinition}{internal axioms} on a [[cohesive (∞,1)-topos]]. Cohesive homotopy type theory is a [[modal type theory]] which adds to [[homotopy type theory]] an [[adjoint triple]] of [[modalities]] \begin{displaymath} ʃ \dashv \flat \dashv \sharp \end{displaymath} called \begin{itemize}% \item [[shape modality]] $\dashv$ [[flat modality]] $\dashv$ [[sharp modality]], \end{itemize} where $ʃ$ and $\sharp$ are [[idempotent monad|idempotent]] [[monads (in computer science)|monads]] and where $\flat$ is an idempotent [[comonad]], subject to some compatibility condition. \hypertarget{a_codiscrete_objects}{}\subsubsection*{{A) Codiscrete objects}}\label{a_codiscrete_objects} \textbf{Axiom A.} \emph{The ambient [[homotopy type theory]] has a [[geometric embedding|left-exact]] [[reflective sub-(∞,1)-category]], to be called the [[base (∞,1)-topos]] ``of [[codiscrete objects]]''.} Coq code at \href{https://github.com/mikeshulman/HoTT/blob/master/Coq/Subcategories/Codiscrete.v}{Codiscrete.v} We write \begin{displaymath} X \to \sharp X \end{displaymath} for the [[reflector]] into codiscrete objects. The homotopy type theory of the [[codiscrete objects]] we call the \emph{external} theory. \hypertarget{b_discrete_objects}{}\subsubsection*{{B) Discrete objects}}\label{b_discrete_objects} \textbf{Axiom B.} There is also a [[coreflective sub-(∞,1)-category]] of \emph{[[discrete objects]]} such that with the codiscrete reflection it makes the ambient theory that of a [[local (∞,1)-topos]]. [[Coq]] code at \href{https://github.com/mikeshulman/HoTT/blob/master/Coq/Subcategories/LocalTopos.v}{LocalTopos.v}. The coreflector from discrete objects we write \begin{displaymath} \flat A \to A \,. \end{displaymath} \hypertarget{c_cohesion}{}\subsubsection*{{C) Cohesion}}\label{c_cohesion} \textbf{Axiom C} The discrete objects are also reflective, the reflector is [[left adjoint]] to the coreflector and preserves [[product types]]. [[Coq]] code at \href{https://github.com/mikeshulman/HoTT/blob/master/Coq/Subcategories/CohesiveTopos.v}{CohesiveTopos.v}. We write \begin{displaymath} X \to \Pi X \end{displaymath} for the reflector into [[discrete objects]]. \hypertarget{example_phenomena}{}\subsection*{{Example phenomena}}\label{example_phenomena} Before looking at the consequences of the axioms formally, we mention some example phenomena to illustrate the meaning of the axioms. \hypertarget{GeometricSpacesAndTheirHomotopyTypes}{}\subsubsection*{{Geometric spaces and their cohesive homotopy types}}\label{GeometricSpacesAndTheirHomotopyTypes} We indicate one central aspect of geometric homotopy theory that is not visible in plain [[homotopy type theory]], but is captured by its cohesive refinement. The standard [[interval]] $I = [0,1]$ in [[Top|topological spaces]] plays two rather different roles, depending on what kind of equivalence between spaces is considered. To make this more vivid, it serves to think of $[0,1]$ as equipped even with its canonical structure of a [[smooth manifold]] ([[manifold with boundary|with boundary]]). The canonical map $I \to *$ to the [[point]] is certainly not a [[diffeomorphism]], and from the point of view of [[differential geometry]] the interval carries non-trivial structure. Notably its endpoints $0,1 : I$ are not equivalent points ([[terms]]) in differential geometry, but are distinct. From the point of view of differential geometry the interval is a [[homotopy n-type|homotopy 0-type]] (has [[h-level]] 2) -- but one that is in some way equipped with geometric structure. This geometric structure, however, induces also a notion of \emph{[[path groupoid|geometric paths]]} in the interval, such that any two of its points are connected by such a path, after all. In other words, one can form the smooth [[fundamental ∞-groupoid]] $\Pi(I)$ of the interval and regard \emph{that} as a [[homotopy type]] \emph{without} further geometric structure (a [[discrete ∞-groupoid]]). This $\Pi(I)$ is an \emph{[[interval type]]}, while $I$ itself is not. As such, the canonical map $\Pi(I) \to *$ is an [[equivalence]] after all, namely a [[weak homotopy equivalence]]. Therefore, after application of $\Pi$, what used to be a geometric 0-type becomes a [[(-1)-groupoid|(-1)-type]] and actually a [[(-2)-groupoid|(-2)-type]] ([[h-level]] 0) -- up to equivalence the [[interval type]], but without any geometry. This latter property is what makes the interval important in bare [[homotopy theory]], where it serves to model notions such as [[cylinder objects]], [[left homotopies]], etc. The former property, however, is what makes the interval important in [[geometry]], where it serves to model [[Cartesian spaces]], [[manifolds]], etc. In cohesive homotopy type theory these two roles of the interval can both be seen, via the reflective embedding of [[discrete objects]], and the transition between them is present, via the [[fundamental infinity-groupoid in a locally infinity-connected (infinity,1)-topos|fundamental ∞-groupoid reflector]] $\mathbf{\Pi}$. Specifically, there is a [[model]] for [[cohesive (∞,1)-topos|homotopy cohesion]], called [[Smooth∞Grpd]], in which [[smooth manifolds]] ([[manifold with boundary|with boundary]]) are [[full and faithful functor|fully faithfully embedded]], where hence $I = [0,1]$ exists as a [[type]] that behaves as the interval in [[differential geometry]], and where $\mathbf{\Pi}(I)$ is equivalent to the [[unit type]]. More generally, in this model every [[smooth manifold]] $X$ is a [[homotopy n-type|homotopy 0-type]]/[[0-truncated]] object, but the type $\mathbf{\Pi}(X)$ is a [[discrete ∞-groupoid]] whose [[homotopy type]] is that of the topological space underlying $X$, as regarded in the [[model structure on topological spaces|standard]] [[homotopy category]] of topological spaces. In particular, the smooth [[circle]] $S^1$ in this model is a [[0-truncated|0-type]] such that $\mathbf{\Pi}(S^1)$ is the [[1-truncated|1-type]] $\mathbf{B}\mathbb{Z}$ (the [[delooping]] [[groupoid]] of the [[integers]]). One can turn this around and axiomatize a [[continuum]] [[line object]] in cohesive homotopy type theory as a [[ring object]] $\mathbb{Z} \hookrightarrow \mathbb{A}^1$ such that $\mathbf{\Pi}(\mathbb{A}^1) \simeq *$. \hypertarget{Structures}{}\subsection*{{Structures in cohesive homotopy type theory}}\label{Structures} We discuss implications of the axioms of cohesive homotopy type theory and go through the discussion of the various [[structures in a cohesive (∞,1)-topos]]. \hypertarget{cohomology}{}\subsubsection*{{Cohomology}}\label{cohomology} For $X$ and $A$ two [[types]], the externalization $\sharp(X \to A)$ of the [[function type]] $X \to A$ is the \emph{type of [[cocycles]]} on $X$ with coefficients in $A$. Its [[h-level]] 2 [[truncated|truncation]] $\tau_0 \sharp(X \to Y)$ is the [[cohomology]] of $X$ with coefficients in $A$. \hypertarget{flat_cohomology_and_local_systems}{}\subsubsection*{{Flat cohomology and local systems}}\label{flat_cohomology_and_local_systems} We give the [[Coq]]-formalization of \href{http://ncatlab.org/nlab/show/cohesive+%28infinity%2C1%29-topos+--+structures#FlatDifferentialCohomology}{Flat cohomology and local systems}. For $A$ a [[type]], we say that [[cohomology]] with coefficients in $\flat A$ is \emph{flat cohomology}. A [[cocycle]] [[term]] $c : \sharp(X \to \flat A)$ is called a [[local system]] of coefficients $A$ on $X$. (\ldots{}) \hypertarget{de_rham_cohomology}{}\subsubsection*{{de Rham cohomology}}\label{de_rham_cohomology} We give the [[Coq]]-formalization of \href{http://ncatlab.org/nlab/show/cohesive+%28infinity,1%29-topos+--+structures#deRhamCohomology}{intrinsic de Rham cohomology}. Let $A = \mathbf{B}G$ be a [[0-connected|connected]] [[type]]. The [[homotopy fiber]] type of the coreflection $\flat \mathbf{B}G \to \mathbf{B}G$ we call the \emph{de Rham coefficient type} of $G$, denoted $\flat_{dR} \mathbf{B}G$. So there is a [[fiber sequence]] \begin{displaymath} \flat_{dR} \mathbf{B}G \to \flat \mathbf{B}G \to \mathbf{B}G \,. \end{displaymath} [[Coq]]-code: \begin{verbatim}Require Import Homotopy Subtopos Codiscrete LocalTopos CohesiveTopos. Hypothesis BG : Type. Hypothesis BG_is_0connected : is_contr (pi0 BG). Hypothesis pt : BG. Definition flat_dR : #Type := ipullback ([[fun _:unit => pt]]) (from_flat ([BG])).\end{verbatim} \hypertarget{differential_cohomology}{}\subsubsection*{{Differential cohomology}}\label{differential_cohomology} We give the [[Coq]]-formalization of \href{http://ncatlab.org/nlab/show/cohesive+%28infinity%2C1%29-topos+--+structures#DifferentialCohomology}{Differential cohomology}. (\ldots{}) \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item [[geometric homotopy type theory]] \item [[modal homotopy type theory]] \item [[stable homotopy type]] \item [[differential homotopy type theory]] \end{itemize} \hypertarget{References}{}\subsection*{{References}}\label{References} A survey with discussion of applications to [[gauge theory]] and [[quantum field theory]] is at \begin{itemize}% \item [[Urs Schreiber]], [[Mike Shulman]], \emph{[[schreiber:Quantum gauge field theory in Cohesive homotopy type theory]]} \end{itemize} The formulation of [[cohesive topos|axiomatic cohesion]] on 1-[[categories]] is due to [[Bill Lawvere]], see \href{http://ncatlab.org/nlab/show/cohesive+topos#References}{there} for a detailed bibliography. The [[Coq]] formalization of [[cohesive (infinity,1)-topos|axiomatic homotopy cohesion]] is discussed in \begin{itemize}% \item [[Mike Shulman]], \emph{Internalizing the external, or The Joys of Codiscreteness} (\href{http://golem.ph.utexas.edu/category/2011/11/internalizing_the_external_or.html}{blog post}) \end{itemize} A formalization in homotopy type theory with [[adjoint logic]] added is in \begin{itemize}% \item [[Mike Shulman]], \emph{Brouwer's fixed-point theorem in real-cohesive homotopy type theory}, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (\href{https://arxiv.org/abs/1509.07584}{arXiv:1509.07584}, \href{https://doi.org/10.1017/S0960129517000147}{doi:10.1017/S0960129517000147}) \item [[Dan Licata]], [[Mike Shulman]], \emph{Adjoint logic with a 2-category of modes}, in \emph{\href{http://lfcs.info/lfcs-2016/}{Logical Foundations of Computer Science 2016}} (\href{http://dlicata.web.wesleyan.edu/pubs/ls15adjoint/ls15adjoint.pdf}{pdf}, \href{http://dlicata.web.wesleyan.edu/pubs/ls15adjoint/ls15adjoint-lfcs-slides.pdf}{slides}) \end{itemize} In the \href{http://en.wikipedia.org/wiki/Pseudocode}{pseudocode} formerly known as traditional mathematics, homotopy cohesion is discussed in \begin{itemize}% \item [[Urs Schreiber]], \emph{[[schreiber:differential cohomology in a cohesive topos]]} (\href{http://arxiv.org/abs/1310.7930}{arXiv:1310.7930}) \end{itemize} See also \begin{itemize}% \item [[Urs Schreiber]], \emph{[[schreiber:Modern Physics formalized in Modal Homotopy Type Theory ]]} \item [[Mike Shulman]], \emph{Comonadic modalities and cohesion}, talk at \emph{\href{http://www.andrew.cmu.edu/user/fwellen/modal-workshop.html}{Geometry in Modal Homotopy Type Theory}}, 2019 (\href{http://home.sandiego.edu/~shulman/papers/cmu2019a.pdf}{pdf slides}, \href{https://youtu.be/GA93Hjh-Alk}{talk recording}) \end{itemize} [[!redirects cohesive homotopy type theories]] [[!redirects cohesive homotopy type]] [[!redirects cohesive homotopy types]] \end{document}