\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*{dependent linear type theory}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{dependent_linear_type_theory}{}\section*{{Dependent linear type theory}}\label{dependent_linear_type_theory}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{syntax}{Syntax}\dotfill \pageref*{syntax} \linebreak
\noindent\hyperlink{semantics}{Semantics}\dotfill \pageref*{semantics} \linebreak
\noindent\hyperlink{nonhomotopy_version}{Non-homotopy version}\dotfill \pageref*{nonhomotopy_version} \linebreak
\noindent\hyperlink{LinearHomotopyTypeTheory}{Homotopy version}\dotfill \pageref*{LinearHomotopyTypeTheory} \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{Dependent linear [[type theory]]} should be some kind of combination of \emph{[[dependent type theory]]} and \emph{[[linear type theory]]}. Dependent linear \emph{homotopy} type theory should additionally combine this with [[homotopy type theory]]. But there are various things that such combinations might mean, and various attempts to make it precise.

One of the most important is a theory that includes both ``linear types'' and ``nonlinear types'', where the linear types may be dependent on the nonlinear types. The nonlinear types might also be allowed to depend on each other, but in this theory the linear types are not allowed to depend on each other.

There are other approaches to dependent linear type theory that do allow some sort of dependence between linear types, but we will not (yet) discuss them on this page.

\hypertarget{syntax}{}\subsection*{{Syntax}}\label{syntax}

Details are still somewhat in the making: An extension of the [[LF]] [[syntax]] by dependent linear types appears in (\hyperlink{Pfenning96}{Pfenning 96}, \hyperlink{WCFW03}{WCFW 03}) and a dependent linear extension of [[system L]] in (\hyperlink{Spiwack14}{Spiwack 14, section 5}).

Proposals for an actual [[syntax]] for dependent linear type theory appear in (\hyperlink{Vakar14}{V\'a{}k\'a{}r 14}, \hyperlink{KPB15}{KPB 15}).

\hypertarget{semantics}{}\subsection*{{Semantics}}\label{semantics}

Dependent linear type theory should have [[categorical semantics]] in [[indexed monoidal (∞,1)-categories]] -- see there for detailed discussion.

\hypertarget{nonhomotopy_version}{}\subsubsection*{{Non-homotopy version}}\label{nonhomotopy_version}

Notice that the following relation between syntax and semantics are well established (see at \emph{[[relation between type theory and category theory]]} for details):

\newline | [[dependent type theory]] | [[locally cartesian closed categories]] |

Here the correspondence in the first line works by interpreting [[types]] $X$ in the [[linear type theory]] as [[objects]] $[X]$ in a [[monoidal category]] $\mathcal{C}^{\otimes}$ and by interpreting the [[conjunctions]] (as far as they exist) as follows:

\begin{tabular}{l|l}
[[type theory]]&[[category theory]]\\
\hline 
$\otimes$ [[multiplicative conjunction]]&$\otimes$ [[tensor product]]\\
$\multimap$ [[linear implication]]&$[-,-]$ [[internal hom]]\\
$(-)^\bot$ [[linear negation]]&$(-)^\ast$ [[dual object]]\\
\end{tabular}

The correspondence in the second line works by forming for any [[locally cartesian closed category]] $\mathcal{C}$ its system of [[slice categories]] $[\Gamma] \mapsto \mathcal{C}_{/[\Gamma]}$, each of which is a [[cartesian monoidal category|cartesian]] [[closed monoidal category]], and then interpreting that as the [[semantics]] for [[dependent type theory]] in the [[context]] $\Gamma$:

\begin{displaymath}
\left\{
    \Gamma \vdash a \colon A
  \right\}
  \leftrightarrow
  \left\{
     (\ast \stackrel{[a]}{\longrightarrow} [A])
     \in Mor(\mathcal{C}_{/[\Gamma]})
  \right\}
  \,.
\end{displaymath}
Moreover, the system of slice categories has good [[base change]] in that for every morphism $[f] \colon [\Gamma_1]\to [\Gamma_2]$ in $\mathcal{C}$ there is an [[adjoint triple]] of [[functors]]

\begin{displaymath}
\mathcal{C}_{[\Gamma_1]}
    \stackrel{\stackrel{[f]_!}{\longrightarrow}}{\stackrel{\overset{[f]^\ast}{\longleftarrow}}{\underset{[f]_\ast}{\longrightarrow}}}
    \mathcal{C}_{[\Gamma_2]}
\end{displaymath}
satisfying [[Frobenius reciprocity]]. These serve as the semantics for the the [[context extension]] along a map $f\colon \Gamma_1 \to \Gamma_2$ of contexts, and for the [[dependent sum]] $\sum$, and the [[dependent product]] of the dependent type theory syntax, respectively:

\begin{displaymath}
\left\{
     \underset{f^{-1}(-)}{\sum}
     , \; f \;,
     \underset{f^{-1}(-)}{\prod}
  \right\}
  \leftrightarrow
  \left\{
    [f]_! \dashv [f]^\ast \dashv [f]_\ast
  \right\}
  \,.
\end{displaymath}
Now since a [[cartesian monoidal category]] is in particular a ([[symmetric monoidal category|symmetric]] [[closed monoidal category|closed]]) [[monoidal category]], this immediately suggest to generalize the assignments $[\Gamma] \mapsto (\mathcal{C}_{/[\Gamma]})^\times$ to assignments $[\Gamma] \mapsto (\mathcal{C}_{[\Gamma]})^\otimes$ of ([[symmetric monoidal category|symmetric]] [[closed monoidal category|closed]]) [[monoidal categories]] (possibly but not necessarily the [[slice categories]] of $\mathcal{C}$) such that there still is good [[base change]] in the above way.

More explicitly, following the notion of [[hyperdoctrine]], the [[categorical semantics]] of dependent linear type theory should have for each [[context]] $\Gamma$ a [[linear type theory]]/possibly-non-[[cartesian monoidal category|cartesian]] [[symmetric monoidal category|symmetric]] [[closed monoidal category]] $(\mathcal{C}_{\Gamma}, \otimes, 1)$ and for each [[homomorphism]] of [[contexts]] $f \;\colon\; \Gamma_1 \longrightarrow \Gamma_2$ functorially an [[adjoint triple]] of [[functors]]

\begin{displaymath}
(f_! \dashv f^\ast \dashv f_\ast)
    \;\colon\;
   \mathcal{C}_{\Gamma_1}
    \stackrel{\stackrel{f_!}{\longrightarrow}}{\stackrel{\overset{f^\ast}{\longleftarrow}}{\underset{f_\ast}{\rightarrow}}}
    \mathcal{C}_{\Gamma_2}
  \,.
\end{displaymath}
where $f^\ast$ is [[context extension]] and where the [[left adjoint]] $f_!$ and [[right adjoint]] $f_\ast$ are to be thought of as linear analogs of [[dependent sum]] and [[dependent product]], respectively. Moreover this should satisfy [[Frobenius reciprocity]], hence $f^\ast$ should be a strong [[closed monoidal functor]]. Typically one would in addition demand the [[Beck-Chevalley condition]] for consecutive such adjoint triples.

Equivalently this is an [[indexed closed monoidal category]]; in the homotopical version, it would be an [[indexed monoidal (∞,1)-category]]. See those pages for more extensive discussion of the mathematics that takes place in such models that should be internalizable in dependent linear (homotopy) type theory once it exists.

In [[geometry]]/[[topos theory]] such a ``linear hyperdoctrine'' is known as \emph{[[six operations]] yoga in [[Wirthmüller context|Wirtmüller flavor]]}. In fact there this appears in [[geometric homotopy theory]] (``[[derived functors]] on [[quasicoherent sheaves]]'') hence as \emph{dependent linear [[homotopy type theory]]}.

Details (of what?) are written out in (\hyperlink{Vakar14}{Vakar 14}).

\begin{remark}
\label{}\hypertarget{}{}
That $f^\ast$ is a morphism of [[monoidal categories]] means that it is a [[strong monoidal functor]], preserving the [[tensor product]]

\begin{displaymath}
f^\ast(X\otimes Y)\simeq (f^\ast X)\otimes (f^\ast Y)
  \,.
\end{displaymath}
If monoidal categories involved are [[closed monoidal categories]] then the condition of [[Frobenius reciprocity]] is equivalent to $f^\ast$ also being a [[strong closed functor]] in that it preserves the [[internal hom]]

\begin{displaymath}
f^\ast [X,Y] \simeq [f^\ast X, f^\ast Y]
  \,.
\end{displaymath}
\end{remark}
\begin{defn}
\label{}\hypertarget{}{}
In view of the perspective of semantics for type theory, we may omit the notational distinction between contexts and the objects that interpret them, and between dependent sum/product and the functors that interpret them. We will write the [[base change]] as

\begin{displaymath}
\left(
     \underset{f}{\sum}
     \dashv
     f^\ast
     \dashv
     \underset{f}{\prod}
   \right)
    \;\colon\;
   Mod(\Gamma_1)
    \stackrel{\stackrel{f_!}{\longrightarrow}}{\stackrel{\overset{f^\ast}{\longleftarrow}}{\underset{f_\ast}{\longrightarrow}}}
    Mod(\Gamma_2)
  \,.
\end{displaymath}
The statement of [[Frobenius reciprocity]] then equivalently reads like this:

\begin{displaymath}
\underset{f}{\sum}
  \left(
    X \otimes f^\ast Y
  \right)
  \simeq
  \left(
    \underset{f}{\sum} X
  \right)
  \otimes
  Y
  \,.
\end{displaymath}
For $f\colon X\to Y$ a morphism in $\mathcal{C}$, we write

\begin{displaymath}
\epsilon_f
  \colon
  \underset{f}{\sum}f^\ast (-)
  \longrightarrow
  (-)
\end{displaymath}
for the [[counit of an adjunction|adjunction counit]] of $(\sum_f \dashv f^\ast)$.

Notice that $\underset{f}{\sum}$ has the interpretation of summing over all the [[fibers]] of the morphism $f$, as the elements in its [[codomain]] vary. Therefore it is sometime suggestive to use the notation

\begin{displaymath}
\underset{f^{-1}(-)}{\sum}
  \coloneqq
  \underset{f}{\sum}
  \,.
\end{displaymath}
In this vein, for $X \in \mathcal{C}$ any object and $p_X \colon X \to \ast$ the canonical morphism to the [[terminal object]], we abbreviate as

\begin{displaymath}
\underset{X}{\sum}
  \coloneqq
  \underset{p_X}{\sum}
  \,.
\end{displaymath}
\end{defn}
\hypertarget{LinearHomotopyTypeTheory}{}\subsubsection*{{Homotopy version}}\label{LinearHomotopyTypeTheory}

This discussion of dependent linear type theory \hyperlink{DependentLinearTypeTheory}{above} has an evident straightforward refinement to [[homotopy theory]]. To appreciate this, notice that the following relation is well established (see again at \emph{[[relation between type theory and category theory]]} for details):

\begin{tabular}{l|l}
[[syntax]]&[[semantics]]\\
\hline 
[[homotopy type theory]]&[[locally cartesian closed (∞,1)-categories]]\\
[[homotopy type theory]] with [[univalence&univalent]] weak [[type universes]]\\
\end{tabular}

This works very much along the lines of the above relation between [[dependent type theory]] and [[locally cartesian closed categories]]. The central new ingredient is that one requires the locally cartesian closed category $\mathcal{C}$ to be equipped with a suitable structure of a [[model category]]. Using this there is then a notation of [[fibrant replacement]] of morphisms. The key point is that where in [[extensional type theory]] the [[identity type]] $(X \vdash Id_X \colon Type)$ of a type $X$ has semantics given by the [[diagonal]] morphism $\Delta_{[X]} \in \mathcal{C}_{/{[X]}}$, here in [[homotopy type theory]] it has semantics in the [[fibrant replacement]] $\hat \Delta_{[X]} \in \mathcal{C}_{/X}$. Such a fibrant replacement of the diagonal is [[path space object]] of $X$, reflecting the [[equivalences]]/[[homotopies]] ``inside'' the type $X$.

\begin{remark}
\label{}\hypertarget{}{}
Since the Grothendieck construction of the standard indexed monoidal $(\infty,1)$-category of parametrized spectra is a [[tangent (∞,1)-toposes]], one model for linear types depending on other \emph{linear} types might be higher [[jet (∞,1)-category|jet (∞,1)-topos]]. This remains to be thought about.

\end{remark}
What should be the [[categorical semantics]] of dependent linear type theory was discussed in (\hyperlink{Shulman08}{Shulman 08}, \hyperlink{PontoShulman12}{Ponto-Shulman 12}, \hyperlink{Shulman12}{Shulman 12}, \hyperlink{Schreiber14}{Schreiber 14}).

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[indexed monoidal (∞,1)-category]]

\end{itemize}
\hypertarget{References}{}\subsection*{{References}}\label{References}

A [[syntax]] extending [[LF]] with linear dependent types was first published in

\begin{itemize}%
\item Iliano Cervesato, [[Frank Pfenning]], \emph{A Linear Logical Framework}, 1996, (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.1152}{web})

\end{itemize}
Note that this framework was restricted to the \emph{negative} fragment of [[intuitionistic linear logic]] and [[dependent type theory]] (i.e., $\multimap$, $\&$ and $\Pi$). The problem of extending [[LF]] to positive connectives ($\otimes,1,!,\exists$) while retaining a reasonable notion of [[canonical form]] was later addressed by

\begin{itemize}%
\item Kevin Watkins, Iliano Cervesato, [[Frank Pfenning]], David Walker, \emph{A concurrent logical framework I: Judgments and properties}, CMU technical report CMU-CS-02-101, revised May 2003 (\href{http://www.cs.cmu.edu/~fp/papers/CMU-CS-02-101.pdf}{web})

\end{itemize}
A dependent linear version of [[system L]] is considered in

\begin{itemize}%
\item [[Arnaud Spiwack]], section 5 of \emph{A dissection of L}, preprint \href{http://assert-false.net/arnaud/papers/A%20dissection%20of%20L.pdf}{pdf}

\end{itemize}
More recent work in the type-theoretic literature includes:

\begin{itemize}%
\item [[Ugo Dal Lago]], \emph{Linear Dependent Types in a Subrecursive Setting}, in \emph{Bounded Linear Logic Workshop} Fontainebleau, 2013.


\item [[Ugo Dal Lago]], M. Gaboardi, \emph{Linear Dependent Types and Relative Completeness-, in}Logical Methods in Computer Science\_ Vol. 8(4:11), 2012.


\item [[Ugo Dal Lago]] and B. Petit, \emph{Linear dependent types in a call-by-value scenario}, in \emph{Science of Computer Programming 84}, 2014.


\item F.N. Forsberg, \emph{Restricted linear dependent types for resource allocation}, in \emph{Bounded Linear Logic Workshop}, Fontainebleau, 2013.


\item M. Gaboardi et al., \emph{Linear Dependent Types for Differential Privacy}, in POPL `13, 2013.



\end{itemize}
Proposals for a genuine [[syntax]] for dependent linear type theory are in

\begin{itemize}%
\item [[Matthijs Vákár]], \emph{Syntax and Semantics of Linear Dependent Types} (\href{http://arxiv.org/abs/1405.0033}{arXiv:1405.0033})


\item [[Matthijs Vákár]], \emph{Splitting the Atom of Dependent Types\ldots{} or Linear and Operational Dependent Type Theory}, November 2014 (\href{http://users.ox.ac.uk/~magd3996/research/10-11-2014-Oxford-Linear%20dependent%20types.pdf}{pdf slides})


\item [[Neelakantan Krishnaswami]], Pierre Pradic, [[Nick Benton]], \emph{Integrating Dependent and Linear Types}, POPL 15 (\href{http://www.cs.bham.ac.uk/~krishnan/dlnl-paper.pdf}{pdf})


\item [[Martin Lundfall]], \emph{A diagram model of linear dependent type theory}, (\href{https://arxiv.org/abs/1806.09593}{arXiv:1806.09593})



\end{itemize}
Semantics for dependent linear type theory and linear homotopy type theory are discussed in

\begin{itemize}%
\item [[Mike Shulman]], \emph{Framed bicategories and monoidal fibrations}, in Theory and Applications of Categories, Vol. 20, 2008, No. 18, pp 650-738. (\href{http://www.tac.mta.ca/tac/volumes/20/18/20-18abs.html}{TAC})


\item [[Kate Ponto]], [[Mike Shulman]], \emph{Duality and traces in indexed monoidal categories}, (\href{http://arxiv.org/abs/1211.1555}{arXiv:1211.1555}, \href{http://golem.ph.utexas.edu/category/2011/11/traces_in_indexed_monoidal_cat.html}{blog})


\item [[Mike Shulman]], \emph{Enriched indexed categories},(\href{http://arxiv.org/abs/1212.3914}{arXiv:1212.3914})


\item [[Urs Schreiber]], \emph{Quantization via Linear Homotopy Types}, (\href{http://arxiv.org/abs/1402.7041}{arXiv:1402.7041})



\end{itemize}
[[!redirects dependent linear type theories]]

[[!redirects linear dependent type theory]] [[!redirects linear dependent type theories]]

[[!redirects linear dependent homotopy type theory]] [[!redirects linear dependent homotopy type theories]]

[[!redirects dependent linear homotopy type theory]] [[!redirects dependent linear homotopy type theories]]

[[!redirects linear homotopy type theory]] [[!redirects linear homotopy type theories]]

[[!redirects linear homotopy-type theory]] [[!redirects linear homotopy-type theories]]

[[!redirects dependent linear type]] [[!redirects dependent linear types]]



\end{document}