tiny.tex

\documentclass[10pt]{article}
\usepackage{fullpage}

\thickmuskip=5mu plus 3mu minus 1mu
\medmuskip=4mu plus 2mu minus 3mu

% \usepackage{scohesion}

\usepackage{amssymb,amsthm}
\usepackage{thmtools}
\usepackage{amsmath}
\usepackage{stmaryrd}
\usepackage{wasysym}

\usepackage{mathpartir}
\usepackage{tikz-cd}

\usepackage{graphicx}
\usepackage{scalerel}
\usepackage{fontawesome}

\usepackage{xcolor}
\definecolor{darkgreen}{rgb}{0,0.45,0}

\usepackage[status=draft,inline,nomargin]{fixme}
\FXRegisterAuthor{mvr}{anmvr}{\color{blue}MVR}

\usepackage[style=alphabetic, maxbibnames=99, maxalphanames=99,
mincrossrefs=99]{biblatex}
\addbibresource{tiny.bib}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{example}[theorem]{Example}
\newtheorem{question}{Question}

\let\oldequiv\equiv%
\renewcommand{\equiv}{\simeq}
\newcommand{\defeq}{\oldequiv}
\newcommand{\ndefeq}{\not\defeq}

\newcommand{\rulen}[1]{\textsc{#1}}
\newcommand{\yields}{\vdash}
\newcommand{\qyields}{\Vdash}
\newcommand{\cbar}{\, | \,}
\newcommand{\judge}{\mathcal{J}}
\newcommand{\freshfor}{\mathbin{\#}}

\newcommand{\ctx}{\,\,\mathsf{ctx}}
\newcommand{\type}{\,\,\mathsf{type}}
\newcommand{\tele}{\,\,\mathsf{tele}}

% Ordinary HoTT notation
\newcommand{\Idsym}{\mathsf{Id}}
\newcommand{\Id}{\mathsf{Id}}
% \newcommand{\Id}[3]{\mathsf{Id}_{{#1}}(#2,#3)}
\newcommand*{\trunc}[2]{\mathopen{}\left\Vert #2\right\Vert_{#1}\mathclose{}}
\newcommand*{\strunc}[2]{\mathopen{}\left\Vert #2\right\Vert_{#1}^s\mathclose{}}
\newcommand*{\univ}{\mathcal{U}}
\newcommand*{\NN}{\mathbb{N}}
\newcommand*{\ZZ}{\mathbb{Z}}
% \newcommand*{\true}{\star}
\newcommand*{\id}{\mathsf{id}}
\newcommand*{\proj}{\mathsf{pr}}
\newcommand*{\pushpr}{\mathbin{\wasysquare}}
\newcommand*{\join}{\ast}
\newcommand*{\ap}{\mathsf{ap}}
\newcommand*{\transp}{\mathsf{tr}}
\newcommand*{\isContr}{\mathsf{isContr}}
\newcommand*{\isEquiv}{\mathsf{isEquiv}}
\newcommand*{\isSpace}{\mathsf{isSpace}}
\newcommand*{\isModal}{\mathsf{isModal}}
\newcommand*{\inl}{\mathsf{inl}}
\newcommand*{\inr}{\mathsf{inr}}
\newcommand*{\glue}{\mathsf{glue}}
\newcommand*{\code}{\mathsf{code}}
\newcommand*{\encode}{\mathsf{encode}}
\newcommand*{\decode}{\mathsf{decode}}
\newcommand*{\const}{\mathsf{const}}
\newcommand*{\fib}{\mathsf{fib}}
\newcommand*{\case}{\mathsf{case}}
\newcommand*{\refl}[1]{\mathsf{refl}_{#1}}
\newcommand*{\pathind}[3]{\mathsf{let} \; \refl{#2} = {#1} \,
  \mathsf{in} \, {#3}}
\newcommand*{\cupann}[2]{\mathbin{\tensor*[_{#1}]{\cup}{_{#2}}}}
\newcommand{\bang}{\mathord{!}}
\newcommand{\ind}[3]{\mathsf{let} \; {#2} = {#1} \, \mathsf{in} \, {#3}}

% \makeatletter
% \newcommand{\@thesum}[1]{(#1) \times}
% \newcommand{\sm}[1]{\@ifnextchar\bgroup{\@thesum{#1}\sm}{\@thesum{#1}}}
% \newcommand{\@theprd}[1]{(#1) \to}
% \newcommand{\prd}[1]{\@ifnextchar\bgroup{\@theprd{#1}\prd}{\@theprd{#1}}}
% \makeatother

\makeatletter \def\smsym{\sum}
\newcommand{\@thesum}[1]{\smsym_{(#1)}}
\newcommand{\sm}[1]{\@ifnextchar\bgroup{\@sm{#1}\sm}{\@sm{#1}}}
\newcommand{\@sm}[1]{\mathchoice{{\textstyle\@thesum{#1}}}{\@thesum{#1}}{\@thesum{#1}}{\@thesum{#1}}}
\def\prdsym{\prod}
\newcommand{\@theprd}[1]{\prdsym_{(#1)}}
\newcommand{\prd}[1]{\@ifnextchar\bgroup{\@prd{#1}\prd}{\@prd{#1}}}
\newcommand{\@prd}[1]{\mathchoice{{\textstyle\@theprd{#1}}}{\@theprd{#1}}{\@theprd{#1}}{\@theprd{#1}}}
\makeatother

\newcommand*{\lolli}{\multimap}

% \newcommand{\lock}{\text{\faLock}}
\newcommand{\lock}{\mathchoice {\scalebox{0.8}{\text{\faLock}}}
  {\scalebox{0.8}{\text{\faLock}}} {\scalebox{0.5}{\text{\faLock}}}
  {\scalebox{0.4}{\text{\faLock}}} }
\newcommand{\unlock}{\text{\faUnlock}}
\newcommand{\key}{\mathchoice
  {\scalebox{0.8}{\text{\faKey}}} {\scalebox{0.8}{\text{\faKey}}}
  {\scalebox{0.5}{\text{\faKey}}} {\scalebox{0.4}{\text{\faKey}}} }

\newcommand{\rbindsym}{\raisebox{-0.5pt}{\scalerel*{\reflectbox{\rotatebox[origin=c]{185}{$\lambda$}}}{\lambda}}}
% \newcommand{\rbindsym}{\raisebox{-0.55pt}{\scalerel*{\rotatebox[origin=c]{185}{$\lambda$}}{\lambda}}\hspace{-0.06em}}
\newcommand{\rbind}[1]{\rbindsym{} #1.}
% lol
% \newcommand{\rbind}[1]{. #1 \rbindsym{}}

\newcommand{\Tiny}{\mathbb{T}}
\newcommand{\lockn}[1]{\mathcal{#1}}
\newcommand{\locksin}[1]{\mathsf{locks}(#1)}
\newcommand{\varkeye}[2]{\key_{#1}^{#2}}
\newcommand{\varkey}[2]{\varkeye{\lockn{#1}}{#2}}
\newcommand{\admkeye}[2]{\overrightarrow{\key}_{#1}^{#2}}
\newcommand{\admkey}[2]{\admkeye{\lockn{#1}}{#2}}
\newcommand{\ctxlocke}[1]{\lock_{#1}}
\newcommand{\ctxlock}[1]{\ctxlocke{\lockn{#1}}}
% \newcommand{\ctxopen}[2]{\unlock_{\lockn{#1}}^{\,#2}}
\newcommand{\stubra}[1]{\llbracket #1 \rrbracket}
% \newcommand{\stubra}[1]{\lfloor #1 \rfloor}
\newcommand{\admbra}[1]{[ #1 ]}
\newcommand{\subkeyoe}[2]{#1/\key_{#2}}
\newcommand{\subkeyo}[2]{\subkeyoe{#1}{\lockn{#2}}}
\newcommand{\subkeye}[2]{\admbra{\subkeyoe{#1}{#2}}}
\newcommand{\subkey}[2]{\admbra{\subkeyo{#1}{#2}}}
\newcommand{\subkeyeann}[5]{\admbra{\key(#3; #1/#2; #4; #5)}}
\newcommand{\subkeyann}[5]{\subkeyeann{#1}{\lockn{#2}}{#3}{#4}{#5}}
\newcommand{\subkeyetele}[4]{\admbra{\key(#3; #1/#2; #4)}}
\newcommand{\subkeytele}[4]{\subkeyetele{#1}{\lockn{#2}}{#3}{#4}}
\newcommand{\substucke}[2]{\stubra{#1/\key_{#2}}}
\newcommand{\substuck}[2]{\substucke{#1}{\lockn{#2}}}
% \newcommand{\sublock}[2]{\admbra{\lock_{\lockn{#1}}/#2}}
\newcommand{\sublock}[2]{\admbra{\rbindsym{} #2. /\lock_{\lockn{#1}} }}
% \newcommand{\sublock}[2]{\admbra{ .#2 \rbindsym{} /\lock_{\lockn{#1}} }}

\newcommand{\unit}[3]{\mathsf{unit}_{#1, #2, \lockn{#3}}}
\newcommand{\counit}[3]{\mathsf{counit}_{#1, \lockn{#2}, #3}}

\newcommand{\rformsym}{\surd}
\newcommand{\rformslicesym}[1]{\surd_{\mkern-6mu/#1}}
\newcommand{\rforme}[2]{\ThisStyle{\raisebox{0.07em}{$\SavedStyle \rformsym_{\hspace{-0.25em}#1}$}} #2}
\newcommand{\rform}[2]{\rforme{\lockn{#1}}{#2}}
\newcommand{\rformu}[1]{\ThisStyle{\raisebox{0.07em}{$\SavedStyle \rformsym$}} #1}
% \newcommand{\rintroe}[2]{\mathsf{root}_{#1}(#2)}
\newcommand{\rintroe}[2]{\lock_{#1}. #2}
\newcommand{\rintro}[2]{\rintroe{\lockn{#1}}{#2}}
% \newcommand{\relim}[1]{\mathsf{unroot}(#1)}
% \newcommand{\rbindsym}{\rotatebox[origin=c]{180}{$\lambda$}}

\newcommand{\relim}[1]{\rbindsym #1}
\newcommand{\retro}[1]{\mathsf{retro}\,#1}

% \newcommand{\rdepform}[2]{{\between^{#1}}#2}
\newcommand{\rdepform}[2]{{#2}^{1/#1}}

\newcommand{\rget}[1]{{#1}_{\downharpoonleft}}

% Cubical stuff
\newcommand{\Set}{\mathsf{Set}}
\newcommand{\El}{\mathsf{El}}
\newcommand{\univfib}{\mathsf{U}}
\newcommand{\Int}{\mathbb{I}}
\DeclareMathOperator{\isFib}{\mathsf{isFib}}
\DeclareMathOperator{\Fib}{\mathsf{Fib}}
\DeclareMathOperator{\isNewFib}{\mathsf{isNewFib}}
\DeclareMathOperator{\NewFib}{\mathsf{NewFib}}
\newcommand{\Compstr}{\mathsf{C}}

\usepackage{hyperref}
\usepackage{cleveref}
\hypersetup{colorlinks,citecolor=darkgreen,linkcolor=darkgreen}

\title{Tiny Object}
\author{}
\date{}

\begin{document}
\maketitle

We describe a type theory that makes a fixed type $\Tiny$ a `tiny
object': there is a type former $\rformu$ that is the amazing right
adjoint to $(\Tiny \to -)$. Of necessity this is an external right
adjoint, and so the context structure of ordinary type theory will
have to be modified to support it.

We add $\rformu$ as a `Fitch style'
modality~\cite{clouston:fitch-style}, where the type former $\rformu$
is made right-adjoint to an operation on contexts. Such modalities are
particularly nice when they are a \emph{double} right adjoint, and
FitchTT~\cite{fitchtt} investigates adding modalities of this kind to
MLTT. We are in such a situation, of course, because
\[{(- \times \Tiny) \dashv (\Tiny \to -) \dashv \rformu -},\] and so
we could use~\cite{fitchtt} directly to produce a type theory.

But there is a special feature of $\rformu$ which impels us to create
a specialised theory for it. Specifically, the leftmost adjoint
$(- \times \Tiny)$ already exists as an operation on contexts: it is
simply context extension with $i : \Tiny$. We allow $\Tiny$ to be an
\emph{ordinary type}, rather than a pre-type or special piece of
syntax. This flexibility is essential for applications in synthetic
differential geometry, where, for example, the type of (first-order)
infinitesimals defined by
$D :\defeq \{ x : \mathbb{R} \mid x^2 = 0 \}$ is tiny. The only new
context former needed is something corresponding to $(\Tiny \to -)$,
which we write as context extension with a $lock$.

To make $(-,i:\Tiny) \dashv (-,\lock)$ on contexts, we need unit
$\Gamma \to (\Gamma,i : \Tiny, \lock)$ and counit
$(\Gamma,\lock,i : \Tiny) \to \Gamma$ substitutions. In~\cite{fitchtt}
these are added axiomatically, and the type theory is presented in a
variable-free CwF style where these explicit substitutions are pushed
around manually. The downside of the approach is that figuring out how
to use a variable could be challenging: we may have to devise by hand
an explicit substitution that extracts the variable from the context.
One of our aims is to give a fully explicit variable rule which
builds in the normal forms of these `stuck substitutions'.

The reason this gets interesting is that, because $\Tiny$ is an
ordinary type, we can substitute \emph{any term} $t : \Tiny$ for $i$
in the counit substitution. And so, the admissible counit rule is
parameterised by a genuine term $t : \Tiny$. The counit rule only gets
stuck on the ordinary variable rule, so every use of a variable in
this theory can have (possibly many) attached terms of $\Tiny$
corresponding to these stuck counits. Having $\Tiny$ as an ordinary
type distinguishes this type theory from
\cite{cavallo-harper:parametricity-for-ctt,cavallo:thesis} and
\cite[Section 5]{fitchtt}, where the $\Gamma,i:\Tiny$ context
extension is a special piece of syntax, and so only special `terms'
may be substituted for it.

In contrast to \cite[Section 2]{transpension}, we only add a right
adjoint for the non-dependent function space, rather than adding a
right adjoint to the dependent product
$\Pi_\Tiny : \mathcal{E}/\Tiny \to \mathcal{E}$. This makes the rules
for the $\rformu$ type much simpler, and (conjecturally) lets us
maintain admissibility of substitution, normalisation, etc. And, maybe
surprisingly, a right adjoint to the dependent function space is
derivable internally from our simply-typed version.

In~\cite{lops}, a tiny interval $\mathbb{I}$ is used to give an
internal construction of a universe that classifies fibrations. The
$\rformu$ type former is described by a collection of axioms, and the
fact that the adjunction is external is enforced by requiring the
inputs to these axioms to be `crisp', roughly, protected by a use of
the global sections/discrete inclusion modality $\flat$. Internally,
this manifests as an equivalence
$\flat((\Tiny \to A) \to B) \equiv \flat(A \to \rformu B)$, but we
will see that this is more restrictive than necessary. Once we have
the $\rformu$ type former built-in, we can prove an equivalence
$\rformu ((\Tiny \to A) \to B) \equiv (A \to \rformu B)$, where $A$
and $B$ do not have to be `global types'. (But the dependency of $B$
is still somewhat restricted.)

Our type theory tackles a challenge set by Lawvere, to produce a
formal system for working with tiny objects: ``This possibility does
not seem to have been contemplated by combinatory logic; the formalism
should be extended to enable treatment of so basic a
situation''~\cite[Section 3]{lawvere:adjoints}.

% \mvrnote{Which cube categories have tiny intervals?
% \cite{buchholtz-morehouse:cubes}}

\section{Contexts and Variables}

The $\rformu$ type former will be added by making it right-adjoint to
a judgemental version of ``$\Tiny \to \Gamma$'' which we write as
$\Gamma, \ctxlock{L}$, where, to refer to it later, the lock is
annotated with a `lock name' $\lockn{L}$. This first section will be
spent adding the necessary rules for $\Gamma, \ctxlock{L}$ to behave
like functions into $\Gamma$.

A simple way to achieve this is to assert axiomatic unit and counit
substitutions for the $(- \times \Tiny) \dashv (\Tiny \to -)$
adjunction, as in the following
\begin{mathpar}
  \inferrule*[left=tiny-form]{\Gamma \ctx}{\Gamma \yields \Tiny \type} \and
  \inferrule*[left=ctx-lock]{\Gamma \ctx}{\Gamma, \ctxlock{L} \ctx} \\
  \inferrule*[left=unit-sub]
  {\Gamma \ctx}
  {\Gamma \yields \unit{\Gamma}{i}{L} : \Gamma, i : \Tiny, \ctxlock{L}}
  \and
  \inferrule*[left=counit-sub]
  {\Gamma \ctx}
  {\Gamma, \ctxlock{L}, i : \Tiny \yields \counit{\Gamma}{L}{i} : \Gamma}
\end{mathpar}
together with equations that explain how these explicit substitutions
annihilate.

We think we can do better, however, and give normal forms for the
placement of these explicit substitutions. The examples in later
sections show that it is quite feasible to work in the resulting type
theory by hand.

Besides the context lock, we only need one additional base rule: a
modified version of the variable rule that builds in stuck instances
of the counit substitution. The rule is completely structural and
independent of the rules for types (besides the existence of $\Tiny$).
There are two new admissible rules, corresponding to precomposition
with the counit and unit substitutions.

\begin{itemize}
\item \textbf{The Tiny Type.} There is a closed type $\Tiny$.
  \begin{mathpar}
    \inferrule*[left=tiny-form]{\Gamma \ctx}{\Gamma \yields \Tiny \type}
  \end{mathpar}

\item \textbf{Context Lock.} There is a special context extension,
  \begin{mathpar}
    \inferrule*[left=ctx-lock]{\Gamma \ctx}{\Gamma, \ctxlock{L} \ctx}
    \and
  \end{mathpar}
  to be thought of as $\Tiny \to \Gamma$. We call $\lockn{L}$ a `lock
  name', all lock names in a context are unique.

\item \textbf{Counit.} Because a lock on a context is just a function
  into that context, we can use variables to the left of a lock if we
  can provide an argument to the function: this corresponds to
  precomposition with the counit substitution, with a substitution
  for $\Tiny$ and some contractions built-in.

  The simplest situation we can encounter is
  \begin{mathpar}
    \inferrule*[left=counit?,fraction={-{\,-\,}-}]
    {\Gamma \yields a : A \and \Gamma, \ctxlock{L}, \Gamma' \yields t : \Tiny \and \lock \notin \Gamma'}
    {\Gamma, \ctxlock{L}, \Gamma' \yields a\subkey{t}{L} : A\subkey{t}{L}}
  \end{mathpar}
  corresponding (non-dependently) to the composite
  \begin{align*}
    (\Tiny \to \Gamma) \times \Gamma'
    \xrightarrow{[\id, t]} (\Tiny \to \Gamma) \times \Gamma' \times
    \Tiny
    \xrightarrow{\proj} (\Tiny \to \Gamma) \times \Tiny
    \xrightarrow{\varepsilon} \Gamma
    \xrightarrow{a} A
  \end{align*}

  The new piece of term syntax is a stuck instance of this
  $\subkey{t}{L}$ rule, which we build into the variable rule
  below. To distinguish the admissible rule from the stuck rule, we
  will write the admissible rule as $\subkey{t}{L}$ and the actual
  stuck syntax as $\substuck{t}{L}$. Roughly, the admissible
  $\subkey{t}{L}$ will add a $\substuck{t}{L}$ to every
  \emph{free} variable usage in $a$, a bit like the underlining operation in
  the type theory for $\natural$.

  We need to generalise this rule in a couple of ways. First, we need
  to allow an additional telescope to be carried along, so that we may
  go under binders in the term $a : A$.

  Additionally, we may need to apply the counit to multiple locks
  simultaneously. To facilitate this, for a context
  $\Gamma, \Gamma' \ctx$, let $\locksin{\Gamma'}$ denote the (ordered)
  list of context locks
  $\ctxlocke{\lockn{L}_1}, \dots, \ctxlocke{\lockn{L}_n}$ that appear
  in the telescope $\Gamma'$.
  
  The generalised rule is then:
  \begin{mathpar}
    \inferrule*[left=counit-tele,fraction={-{\,-\,}-}]
    {\Gamma \yields \Gamma'' \tele \and \Gamma, \Gamma' \yields t_i : \Tiny
      \text{ for } \lockn{L}_i \in \locksin{\Gamma'} }
    {\Gamma, \Gamma' \yields \Gamma'' \admbra{\subkeyoe{t_1}{\lockn{L}_1}, \dots, \subkeyoe{t_n}{\lockn{L}_n}} \tele} \and
    \inferrule*[left=counit,fraction={-{\,-\,}-}]
    {\Gamma, \Gamma'' \yields a : A \and \Gamma, \Gamma' \yields t_i : \Tiny
      \text{ for } \lockn{L}_i \in \locksin{\Gamma'} }
    {\Gamma, \Gamma', \Gamma'' \admbra{\subkeyoe{t_1}{\lockn{L}_1}, \dots, \subkeyoe{t_n}{\lockn{L}_n}} \yields a \admbra{\subkeyoe{t_1}{\lockn{L}_1}, \dots, \subkeyoe{t_n}{\lockn{L}_n}} : A \admbra{\subkeyoe{t_1}{\lockn{L}_1}, \dots, \subkeyoe{t_n}{\lockn{L}_n}} }
  \end{mathpar}

  % Formally, the contexts and telescopes used should be annotated in
  % the syntax. When it is necessary to make clear which are used, we
  % will write $a \subkeyann{t}{L}{\Gamma}{\Gamma'}{\Gamma''}$ and
  % $\Gamma''\subkeytele{t}{L}{\Gamma}{\Gamma'}$.

\item \textbf{Variable Usage.} To use a variable $x : A$ that is
  behind some context locks, we must provide a term $t_i : \Tiny$
  for each lock between that variable and the front of the context.

  \begin{mathpar}
    \inferrule*[left=var]
    {\Gamma, x : A, \Gamma' \yields t_i : \Tiny
      \text{ for } \lockn{L}_i \in \locksin{\Gamma'} }
    {\Gamma, x : A, \Gamma' \yields x \stubra{\subkeyoe{t_1}{\lockn{L}_1}, \dots, \subkeyoe{t_n}{\lockn{L}_n}} :
      A \admbra{\subkeyoe{t_1}{\lockn{L}_1}, \dots, \subkeyoe{t_n}{\lockn{L}_n}}}
  \end{mathpar}

  The type of the variable usage has the admissible counit rule
  applied to it: typically these counits will not be stuck on the type
  $A$ unless $A$ is itself a variable.

\item \textbf{Substitution.} Ordinary substitution into a variable turns these
  `stuck' counits back into admissible ones, and continues into the attached terms of $\Tiny$.
  \begin{align*}
    % \Gamma, x : A, \Gamma'
    % &\yields x \substucke{t_1}{\lockn{L}_1} \dots
    %   \substucke{t_n}{\lockn{L}_n} : A\subkeye{t_1}{\lockn{L}_1} \dots \subkeye{t_n}{\lockn{L}_n} \\
    \Gamma, \Gamma'[a/x]
    &\yields x \stubra{\subkeyoe{t_1}{\lockn{L}_1}, \dots, \subkeyoe{t_n}{\lockn{L}_n}}[a/x] \\
    &:\defeq a\admbra{\subkeyoe{t_1[a/x]}{\lockn{L}_1}, \dots, \subkeyoe{t_n[a/x]}{\lockn{L}_n}}
  \end{align*}
  
\item \textbf{Calculating the Counit.} For now, assume that all the
  terms of $\Tiny$ that are involved are closed. To evaluate
  $b\subkey{t}{L}$ on a term $\Gamma \yields b : B$, induct on $b$
  until we reach an instance of the variable rule, say for the
  variable $x : A$.

  As always, there are cases depending on where in the context $x$
  lies. The typical case is when $x : A$ is in $\Gamma$, so the
  context has form
  \begin{align*}
    \Gamma_1, x : A, \Gamma_2, \Gamma'' &\ctx \\
    \locksin{\Gamma_2} &\defeq \lockn{J}_1, \dots,\lockn{J}_m \\
    \locksin{\Gamma''} &\defeq \lockn{K}_{1}, \dots, \lockn{K}_n
  \end{align*}
  and the variable usage looks like
  \begin{align*}
    \Gamma_1, x : A, \Gamma_2, \Gamma''
    &\yields x \stubra{\subkeyoe{j_1}{\lockn{J}_1}, \dots,
      \subkeyoe{j_{m}}{\lockn{J}_{m}},
      \subkeyoe{k_1}{\lockn{K}_{1}},
      \dots, \subkeyoe{k_n}{\lockn{K}_n}} \\
    &: A \admbra{\subkeyoe{j_1}{\lockn{J}_1}, \dots,
      \subkeyoe{j_{m}}{\lockn{J}_{m}},
      \subkeyoe{k_1}{\lockn{K}_{1}},
      \dots, \subkeyoe{k_n}{\lockn{K}_n}}
  \end{align*}
  Then we slot the new $\subkey{t}{L}$ into place, and leave it stuck:
  \begin{align*}
    \Gamma_1, x : A, \Gamma_2, \ctxlock{L}, \Gamma'' \yields
    (&x \stubra{\subkeyoe{j_1}{\lockn{J}_1}, \dots,
      \subkeyoe{j_{m}}{\lockn{J}_{m}},
      \subkeyoe{k_1}{\lockn{K}_{1}},
      \dots, \subkeyoe{k_n}{\lockn{K}_n}}) \subkey{t}{L} \\
    :\defeq {}
     &x \stubra{\subkeyoe{j_1}{\lockn{J}_1}, \dots,
       \subkeyoe{j_{m}}{\lockn{J}_{m}},
       \subkeyo{t}{L},
      \subkeyoe{k_1}{\lockn{K}_{1}},
       \dots, \subkeyoe{k_n}{\lockn{K}_n}}
  \end{align*}

  When working informally, this means counting how many
  $\ctxlocke{\lockn{K}_i}$ are created between the application of
  $\subkey{t}{L}$ and the variable (by the use of some of the typing
  rules), and placing $\subkeyo{t}{L}$ to the left of all the newly
  created $\ctxlocke{\lockn{K}_i}$.

  If instead $x : A$ is in $\Gamma''$, so
  $\Gamma, \Gamma_1'', x : A, \Gamma_2'' \ctx$, suppose the locks
  coming after $x$ are
  $\locksin{\Gamma_2''} \defeq \lockn{K}_{1}, \dots, \lockn{K}_n$ and
  the variable usage looks like
  \begin{align*}
    \Gamma, \Gamma_1'', x : A, \Gamma_2''
    &\yields x \stubra{\subkeyoe{k_1}{\lockn{K}_{1}}, \dots, \subkeyoe{k_n}{\lockn{K}_n}} \\
    &: A\admbra{\subkeyoe{k_1}{\lockn{K}_{1}}, \dots, \subkeyoe{k_n}{\lockn{K}_n}} \\
  \end{align*}
  Access to $x$ is not affected by the addition of the lock
  $\ctxlock{L}$ (which is placed to the left of it), so the variable
  usage is left unchanged.

  Things are trickier with general open terms of $\Tiny$. A couple of
  complications can arise: \mvrnote{These are a bit gnarly, so you
    should probably skip this list on first read}
  \begin{itemize}
  \item  When $t : \Tiny$ is not closed, so that
    $\Gamma_1, x : A, \Gamma_2, \ctxlock{L}, \Gamma' \yields t : \Tiny$,
    the variables used in the term $t$ itself are now locked behind the
    locks in $\Gamma''$ by the time we reach the variable $x$. We
    therefore need to (admissibly) apply
    \begin{align*}
      -\admbra{\subkeyoe{k_1}{\lockn{K}_{1}}, \dots, \subkeyoe{k_n}{\lockn{K}_n}}
    \end{align*}
    to the term $t$, so:
    \begin{align*}
      &x \stubra{\subkeyoe{j_1}{\lockn{J}_1}, \dots,
      \subkeyoe{j_{m}}{\lockn{J}_{m}},
      \subkeyoe{k_1}{\lockn{K}_{1}},
        \dots, \subkeyoe{k_n}{\lockn{K}_n}} \subkey{t}{L} \\
      :\defeq {}
      &x \stubra{\subkeyoe{j_1}{\lockn{J}_1}, \dots,
       \subkeyoe{j_{m}}{\lockn{J}_{m}},
       \subkeyo{t\admbra{\subkeyoe{k_1}{\lockn{K}_{1}}, \dots, \subkeyoe{k_n}{\lockn{K}_n}}}{L},
        \subkeyoe{k_1}{\lockn{K}_{1}},
        \dots, \subkeyoe{k_n}{\lockn{K}_n}}
    \end{align*}
  \item Instead, the terms $j_i$ and $k_i$ may not closed, and so the variables
    used in them might now lie behind the new lock $\ctxlock{L}$. The
    term $t$ is used to unlock them:
    \begin{alignat*}{2}
      &x  \stubra{&&\subkeyoe{j_1}{\lockn{J}_1}, \dots,
            \subkeyoe{j_{m}}{\lockn{J}_{m}},
            \subkeyoe{k_1}{\lockn{K}_{1}},
            \dots, \subkeyoe{k_n}{\lockn{K}_n}} \subkey{t}{L} \\
      :\defeq {}
      &x
        \stubra{&& \subkeyoe{j_1\subkey{t}{L}}{\lockn{J}_1},   \\
      &&& \dots, \\
      &&& \subkeyoe{j_{m}\subkey{t}{L}}{\lockn{J}_{m}}, \\
      &&& \subkeyo{t}{L}, \\
      &&& \subkeyoe{k_{1}\subkey{t}{L}}{\lockn{K}_{1}}, \\
      &&& \dots, \\
      &&& \subkeyoe{k_n\subkey{t}{L}}{\lockn{K}_n}
          }
    \end{alignat*}

  \item Finally, and slightly horrifyingly, the two complications can happen
    at the same time, yielding the final, general definition:
    \begin{alignat*}{2}
      &x  \stubra{&&\subkeyoe{j_1}{\lockn{J}_1}, \dots,
            \subkeyoe{j_{m}}{\lockn{J}_{m}},
            \subkeyoe{k_1}{\lockn{K}_{1}},
            \dots, \subkeyoe{k_n}{\lockn{K}_n}} \subkey{t}{L} \\
      :\defeq {}
      &x
        \stubra{&& \subkeyoe{j_1\subkey{t}{L}}{\lockn{J}_1},   \\
      &&& \dots, \\
      &&& \subkeyoe{j_{m}\subkey{t}{L}}{\lockn{J}_{m}}, \\
      &&& \subkeyo{t\admbra{\subkeyoe{k_1\subkey{t}{L}}{\lockn{K}_{1}}, \dots, \subkeyoe{k_n\subkey{t}{L}}{\lockn{K}_n}}}{L}, \\
      &&& \subkeyoe{k_{1}\subkey{t}{L}}{\lockn{K}_{1}}, \\
      &&& \dots, \\
      &&& \subkeyoe{k_n\subkey{t}{L}}{\lockn{K}_n}
          }
    \end{alignat*}
  \mvrnote{It's not so obvious to me that this terminates!}

\iffalse  
  \item The terms $k_i$ used on the other keys, however,
  may themselves use variables from $\Gamma$. These variables lie
  behind the new lock $\ctxlock{L}$, so we must proceed with applying
  the same \rulen{counit} to the $k_i$:
  \begin{align*}
    \Gamma, \ctxlock{L}, \Gamma', \Gamma_1'', x : A, \Gamma_2''
    &\yields x \substucke{k_1\subkey{t}{L}}{\lockn{K}_1} \dots \substucke{k_n\subkey{t}{L}}{\lockn{K}_n} \\
    &: A\subkeye{k_1\subkey{t}{L}}{\lockn{K}_1} \dots \subkeye{k_n\subkey{t}{L}}{\lockn{K}_n}
  \end{align*}
  \fi
  \end{itemize}

  Let's write out typing derivation in the situation where there are
  no other context locks around, making explicit the telescopes that
  are used.
  
  Given the variable
  \begin{mathpar}
    \inferrule*
    {\Gamma_1, x : A, \Gamma_2, \Gamma_1'', \ctxlock{K}, \Gamma_2'' \yields s : \Tiny}
    {\Gamma_1, x : A, \Gamma_2, \Gamma_1'', \ctxlock{K}, \Gamma_2'' \yields x\substuck{s}{K} : A}
  \end{mathpar}
  so that 
  \begin{mathpar}
    \inferrule*{
    \inferrule*
    {\Gamma_1, x : A, \Gamma_2, \Gamma_1'', \ctxlock{K}, \Gamma_2'' \yields s : \Tiny}
    {\Gamma_1, x : A, \Gamma_2, \Gamma_1'', \ctxlock{K}, \Gamma_2'' \yields x\substuck{s}{K} : A} \and
    \Gamma_1, x : A, \Gamma_2, \ctxlock{L}, \Gamma' \yields t : \Tiny}
    {\Gamma_1, x : A, \Gamma_2, \Gamma', \Gamma_1''\subkey{t}{L}, \ctxlock{K}, \Gamma_2''\subkey{t}{L} \yields x\substuck{s}{K}\subkey{t}{L} : A}
  \end{mathpar}

  Our definition sets this equal to
  $x\substuck{(t\subkey{s\subkey{t}{L}}{K})}{L}\substuck{s}{K}$, where
  \begin{align*}
    t\subkey{s\subkey{t}{L}}{K} \defeq t\subkeyann{s\subkeyann{t}{L}{\Gamma_1, x : A, \Gamma_2}{\Gamma'}{\Gamma''_1, \ctxlock{K}, \Gamma''_2}}{K}{\Gamma_1, x : A, \Gamma_2, \ctxlock{L}, \Gamma', \Gamma_1''\subkey{t}{L}}{\Gamma_2'' \subkey{t}{L}}{\cdot}
  \end{align*}
  has typing derivation
  \begin{mathpar}
    \inferrule*
    {\inferrule*
      {\Gamma_1, x : A, \Gamma_2, \ctxlock{L}, \Gamma' \yields t : \Tiny}
      {\Gamma_1, x : A, \Gamma_2, \ctxlock{L}, \Gamma', \Gamma_1''\subkey{t}{L} \yields t : \Tiny}      
    \and
      \inferrule*
      {\Gamma_1, x : A, \Gamma_2, \Gamma_1'', \ctxlock{K}, \Gamma_2'' \yields s : \Tiny \and
        \Gamma_1, x : A, \Gamma_2, \ctxlock{L}, \Gamma' \yields t : \Tiny
      }
      {\Gamma_1, x : A, \Gamma_2, \ctxlock{L}, \Gamma', \Gamma_1''\subkey{t}{L}, \ctxlock{K}, \Gamma_2''\subkey{t}{L} \yields s\subkey{t}{L} : \Tiny}
    }
    {\Gamma_1, x : A, \Gamma_2, \ctxlock{L}, \Gamma', \Gamma_1''\subkey{t}{L}, \ctxlock{K}, \Gamma_2'' \subkey{t}{L} \yields t\subkey{s\subkey{t}{L}}{K} : \Tiny}
  \end{mathpar}

\item \textbf{Unit.} To complete the implementation of the adjunction,
  we have an admissible rule representing the unit map. The following
  rule is precomposition with the substitution
  $\Gamma \to (\Gamma,i : \Tiny, \ctxlock{L})$, suitably generalised
  with a telescope $\Gamma'$:
  \begin{mathpar}
    \inferrule*[left=unit,fraction={-{\,-\,}-}]
    {\Gamma, i : \Tiny, \ctxlock{L}, \Gamma' \yields a : A}
    {\Gamma, \Gamma'\sublock{L}{i} \yields a\sublock{L}{i} : A\sublock{L}{i}} \\
    \inferrule*[left=unit-tele,fraction={-{\,-\,}-}]
    {\Gamma, i : \Tiny, \ctxlock{L} \yields \Gamma' \tele}
    {\Gamma \yields \Gamma'\sublock{L}{i} \tele}    
  \end{mathpar}
  Like the $\subkey{t}{L}$ operation, we use substitution-like syntax
  for the unit map because it commutes past everything until it
  reaches a variable. The silly $\rbind{i}$ notation is chosen to
  match the syntax for the type former later, sorry!

  The lock and key then `click together', yielding an ordinary
  substitution. In the simplest case, when $t : \Tiny$ is closed and
  $x$ has a single matching stuck \rulen{counit}.
  \begin{align*}
    x \substuck{t}{L}\sublock{L}{i}
    :\defeq x[t/i]
  \end{align*}
  So if $x \defeq i$ the result is $t$, and otherwise the substitution
  yields $x$ again.

  If $x$ has several stuck counits, the operation needs to continue
  into the associated terms. To simplify things a little, rather than
  yielding an actual substitution we can immediately divide into cases
  on whether the underlying variable is the one being `searched for'
  by the \rulen{unit} rule.
  \begin{align*}
    &i \stubra{\subkeyoe{j_1}{\lockn{J}_1}, \dots,
       \subkeyoe{j_{m}}{\lockn{J}_{m}},
       \subkeyo{t}{L},
      \subkeyoe{k_1}{\lockn{K}_{1}},
       \dots, \subkeyoe{k_n}{\lockn{K}_n}}\sublock{L}{i} \\
    :\defeq {}
    &t\sublock{L}{i} \\
    &x \stubra{\subkeyoe{j_1}{\lockn{J}_1}, \dots,
       \subkeyoe{j_{m}}{\lockn{J}_{m}},
       \subkeyo{t}{L},
      \subkeyoe{k_1}{\lockn{K}_{1}},
       \dots, \subkeyoe{k_n}{\lockn{K}_n}} \\
    :\defeq {}
    &x\stubra{\subkeyoe{j_1\sublock{L}{i}}{\lockn{J}_1}, \dots,
       \subkeyoe{j_{m}\sublock{L}{i}}{\lockn{J}_{m}},
      \subkeyoe{k_1\sublock{L}{i}}{\lockn{K}_{1}},
       \dots, \subkeyoe{k_n\sublock{L}{i}}{\lockn{K}_n}}
  \end{align*}
  % \begin{align*}
  %   &x \stubra{\subkeye{s_1}{\lockn{K}_1}, \dots,
  %   \subkeye{s_{i}}{\lockn{K}_{i}}, \subkey{t}{L}, \subkeye{s_{i+1}}{\lockn{K}_{i+1}},
  %   \dots, \subkeye{s_n}{\lockn{K}_n}}\sublock{L}{i} \\
  %   :\defeq {}
  %   &x[t\sublock{L}{i}/i]\admbra{\subkeye{s_1\sublock{L}{i}}{\lockn{K}_1}, \dots,
  %   \subkeye{s_{i}\sublock{L}{i}}{\lockn{K}_{i}}, \subkeye{s_{i+1}\sublock{L}{i}}{\lockn{K}_{i+1}},
  %   \dots, \subkeye{s_n\sublock{L}{i}}{\lockn{K}_n}}
  % \end{align*}

  % \begin{align*}
  %   (\varkey{L'}{t'} \varkeye{\lockn{K}_n}{s_n} \dots \varkeye{\lockn{K}_1}{s_1} x)[\sublock{L}{i}] &:\defeq \admkey{L'}{t'[\sublock{L}{i}]}(\varkeye{\lockn{K}_n}{s_n} \dots \varkeye{\lockn{K}_1}{s_1} x)[\sublock{L}{i}] \\
  %   (\varkey{L}{t} \varkeye{\lockn{K}_n}{s_n} \dots \varkeye{\lockn{K}_1}{s_1} x)[\sublock{L}{i}] &:\defeq (\varkeye{\lockn{K}_n}{s_n} \dots \varkeye{\lockn{K}_1}{s_1} x)[t[\sublock{L}{i}]/i] \\
  %   x[\sublock{L}{i}] &:\defeq x
  %   % (\admkey{L}{t} c) [a/x] &:\defeq \admkey{L}{t[a/x]} c[a/x] \\
  %   % (\varkey{L}{t} c)[\sublock{L}{i}] &:\defeq c[t[\sublock{L}{i}]/i] %\\
  %   % (\admkey{K}{t} c)[\sublock{L}{i}] &:\defeq
  %   % \admkey{K}{t[\sublock{L}{i}]} c[\sublock{L}{i}] &&\lockn{L}
  %   % \not\defeq \lockn{K}
  % \end{align*}

  In any application of the \rulen{unit} rule, the lock $\lockn{L}$
  and the variable $i$ no longer appear in the resulting term
  $a\sublock{L}{i}$.
\end{itemize}

% \begin{remark}
%   To be careful, we should have proper calculus of telescopes
%   $\Gamma \yields \Gamma' \tele$ that $-\subkey{t}{L}$
%   and $-\sublock{L}{i}$ are defined on.
% \end{remark}

% \begin{remark}
%   We do not have weakening by additional locks for arbitrary terms,
%   but we do have a kind of lock weakening for closed terms:
%   \begin{mathpar}
%     \inferrule*[left=closed-lock-wk,fraction={-{\,-\,}-}]
%     {\Gamma \yields \judge}
%     {\ctxlock{L}, \Gamma \yields \judge}
%   \end{mathpar}
% \end{remark}

These rules are peculiar, but if we insist on pushing the
admissible rules to the leaves I believe something like this is forced
on us by the setting we are trying to capture.

\subsection{Examples of Admissible Rules}

Some examples of applying keys to terms:
\begin{alignat*}{2}
  &x : \NN,  y : \NN
  &&\yields x + y : \NN \\
  &x : \NN,  y : \NN, \ctxlock{L}, i : \Tiny
  &&\yields (x + y)\subkey{i}{L} : \NN\subkey{i}{L} \\
  &&&\defeq x\substuck{i}{L} + y\substuck{i}{L} : \NN \\
  ~\\
  &x : \NN
  &&\yields (\lambda y. x + y) : \NN \to \NN  \\
  &x : \NN,\ctxlock{L}, i : \Tiny
  &&\yields (\lambda y. x + y)\subkey{i}{L} : (\NN \to \NN)\subkey{i}{L}  \\
  &&&\defeq (\lambda y. x\substuck{i}{L} + y) : \NN \to \NN  \\
  ~\\
  &A : \univ, B : A \to \univ, f : \prd{x : A} B(x)
  &&\yields f : \prd{x : A} B(x) \\
  &A : \univ, B : A \to \univ, f : \prd{x : A} B(x), \ctxlock{L}, i : \Tiny
  &&\yields f\subkey{i}{L} : \left(\prd{x : A} B(x)\right)\subkey{i}{L} \\
  &&&\defeq f\substuck{i}{L} : \prd{x : A\subkey{i}{L}} (B(x))\subkey{i}{L} \\
  &&&\defeq f\substuck{i}{L} : \prd{x : A\substuck{i}{L}} (B\substuck{i}{L})(x)
\end{alignat*}
In this last example, $B\substuck{i}{L}$ has type
$A\substuck{i}{L} \to \univ$, so applying it to $x$ is well-formed.

Applying \rulen{counit} in various locations.
\begin{alignat*}{2}
  &x : \NN,\ctxlock{K}, k : \Tiny
  &&\yields a\substuck{k}{K} : \NN \\
  &x : \NN,\ctxlock{K}, k : \Tiny, \ctxlock{L}, i : \Tiny
  &&\yields a\substuck{k}{K} \subkey{i}{L} \\
  &&&\defeq a\stubra{\subkeyo{k\subkey{i}{L}}{K}, \subkeyo{i}{L}}  \\
  &&&\defeq a\stubra{\subkeyo{k\substuck{i}{L}}{K}, \subkeyo{i}{L}} : \NN  \\
  ~\\
  &x : \NN, \ctxlock{K}, k : \Tiny
  &&\yields a\substuck{k}{K} : \NN \\
  &x : \NN, \ctxlock{K}, \ctxlock{L}, i : \Tiny, k : \Tiny
  &&\yields a\substuck{k}{K} \subkey{i}{L} \\
  &&&\defeq a\stubra{\subkeyo{k\subkey{i}{L}}{K}, \subkeyo{i}{L}}  \\
  &&&\defeq a\stubra{\subkeyo{k}{K}, \subkeyo{i}{L}} : \NN \\
  ~\\
  &x : \NN, \ctxlock{K}, k : \Tiny
  &&\yields a\substuck{k}{K} : \NN \\
  &x : \NN, \ctxlock{L}, i : \Tiny, \ctxlock{K}, k : \Tiny
  &&\yields a\substuck{k}{K} \subkey{i}{L} \\
  &&&\defeq a\stubra{\subkeyo{i\subkey{k\subkey{i}{L}}{K}}{L}, \subkeyo{k}{K}} \\
  &&&\defeq a\stubra{\subkeyo{i\subkey{k}{K}}{L}, \subkeyo{k}{K}} \\
  &&&\defeq a\stubra{\subkeyo{i\substuck{k}{K}}{L}, \subkeyo{k}{K}}
\end{alignat*}

Applying \rulen{unit} in various locations:
\begin{alignat*}{2}
  &t : \Tiny,\ctxlock{L}, i : \Tiny
  &&\yields t\substuck{i}{L} : \Tiny \\
  &i : \Tiny
  &&\yields (t\substuck{i}{L})\sublock{L}{t} \\
  &&&\defeq t[i/t] \\
  &&&\defeq i : \Tiny \\
  ~\\
  &x : A, i : \Tiny, \ctxlock{L}, j : \Tiny
  &&\yields x\substuck{i\substuck{j}{L}}{L} : A \\
  &x : A, j : \Tiny
  &&\yields \left( x\substuck{i\substuck{j}{L}}{L} \right)\sublock{L}{i} \\
  &&&\defeq x[i\substuck{j}{L}\sublock{L}{i}/i] \\
  &&&\defeq x[i[j\sublock{L}{i}/i]/i] \\
  &&&\defeq x[i[j/i]/i] \\
  &&&\defeq x[j/i] : A
\end{alignat*}
Or even
\begin{alignat*}{2}
  &i : \Tiny, \ctxlock{L}, j : \Tiny
  &&\yields i\substuck{i\substuck{j}{L}}{L} : \Tiny \\
  &j : \Tiny
  &&\yields \left( i\substuck{i\substuck{j}{L}}{L} \right)\sublock{L}{i} \\
  &&&\defeq i\substuck{j}{L}\sublock{L}{i} \\
  &&&\defeq j\sublock{L}{i} \\
  &&&\defeq j : \Tiny
\end{alignat*}
Nothing stops us from iterating this forever:
\begin{alignat*}{2}
  &i : \Tiny, \ctxlock{L}, j : \Tiny
  &&\yields
     i\substuck{i\substuck{i\substuck{j}{L}}{L}}{L} : \Tiny
\end{alignat*}
Semantically, the context corresponds to $i : \Tiny \to \Tiny$ and
$j : \Tiny$, and the term is a version of the iterated application
$i(i(\dots i(j)))$. The lock substitution $\sublock{L}{i}$ then
replaces $i$ with the identity, and so the entire term reduces to $j$.

\iffalse
\begin{remark}
  It feels a bit as though these keys are just delayed substitutions,
  so let's try and make something interesting happen. Suppose we have
  global elements $1, 2, 3, 4 : \Tiny$, and consider the function
  \begin{align*}
    f &: (\Tiny \times \Tiny) \to \rform{L} \rform{K} (\Tiny \times \Tiny) \\
    f(x, y, \ctxlock{L}, \ctxlock{K}) &:\defeq (x\substuck{1}{L}\substuck{2}{K},y\substuck{3}{L}\substuck{4}{K})
  \end{align*}
  This can be evaluated in the following two different ways:
  \begin{align*}
    f(i, j, \rbind{i}, \rbind{j})
    & \defeq (x\substuck{1}{L}\substuck{2}{K}, y\substuck{3}{L}\substuck{4}{K})[i/x][j/y][\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}] \\
    & \defeq (i\substuck{1}{L}\substuck{2}{K}, j\substuck{3}{L}\substuck{4}{K})[\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}] \\
    & \defeq (i\substuck{1}{L}\substuck{2}{K}[\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}], j\substuck{3}{L}\substuck{4}{K}[\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}]) \\
    & \defeq (1, 4)
  \end{align*}
  and
  \begin{align*}
    f(j, i, \rbind{i}, \rbind{j})
    & \defeq (x\substuck{1}{L}\substuck{2}{K}, y\substuck{3}{L}\substuck{4}{K})[i/x][j/y][\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}] \\
    & \defeq (j\substuck{1}{L}\substuck{2}{K}, i\substuck{3}{L}\substuck{4}{K})[\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}] \\
    & \defeq (j\substuck{1}{L}\substuck{2}{K}[\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}], i\substuck{3}{L}\substuck{4}{K}[\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}]) \\
    & \defeq (2, 3)
  \end{align*}

  So the \emph{user} of a $\rformsym$ gets to choose which variable gets
  substituted for, but doesn't get to choose the value that eventually
  gets plugged in. And the values for the other $\key$s get completely
  lost!
\end{remark}
\fi

\begin{remark}
  It feels a bit as though these keys are just delayed substitutions,
  so let's try and make something interesting happen. Suppose we have
  global elements $1, 2, 3, 4 : \Tiny$, and consider a term
  \begin{align*}
    x : \Tiny, y : \Tiny, \ctxlock{L}, \ctxlock{K}
    &\yields
      (x\stubra{\subkeyo{1}{L},\subkeyo{2}{K}},y\stubra{\subkeyo{3}{L},\subkeyo{4}{K}})
      : \Tiny \times \Tiny
  \end{align*}
  Applying two different substitutions allows us to select which of
  the stuck keys to apply:
  \begin{align*}
    & (x\stubra{\subkeyo{1}{L},\subkeyo{2}{K}}, y\stubra{\subkeyo{3}{L},\subkeyo{4}{K}})[i/x][j/y][\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}] \\
    & \defeq (i\stubra{\subkeyo{1}{L},\subkeyo{2}{K}}, j\stubra{\subkeyo{3}{L},\subkeyo{4}{K}})[\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}] \\
    & \defeq (i\stubra{\subkeyo{1}{L},\subkeyo{2}{K}}[\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}], j\stubra{\subkeyo{3}{L},\subkeyo{4}{K}}[\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}]) \\
    & \defeq (1, 4)
  \end{align*}
  and
  \begin{align*}
    & (x\stubra{\subkeyo{1}{L},\subkeyo{2}{K}}, y\stubra{\subkeyo{3}{L},\subkeyo{4}{K}})[j/x][i/y][\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}] \\
    & \defeq (j\stubra{\subkeyo{1}{L},\subkeyo{2}{K}}, i\stubra{\subkeyo{3}{L},\subkeyo{4}{K}})[\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}] \\
    & \defeq (j\stubra{\subkeyo{1}{L},\subkeyo{2}{K}}[\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}], i\stubra{\subkeyo{3}{L},\subkeyo{4}{K}}[\rbind{i}/\ctxlock{L}][\rbind{j}/\ctxlock{K}]) \\
    & \defeq (2, 3)
  \end{align*}
  Once we have the type former, we will be able to cause these
  different substitutions to occur. So the \emph{user} of a term
  containing stuck keys gets to choose which of the stuck keys is
  eventually used, but doesn't get to choose the actual term that gets
  plugged in. And the stored terms for the other keys are
  completely lost!
\end{remark}

\subsection{Total Substitutions}

\newcommand{\wksub}[1]{\mathsf{w}(#1)}
\newcommand{\conjinv}[3]{\mathsf{inv}(#1, \lockn{#2}, #3)}
\newcommand{\varfunc}[1]{,\uparrow_{#1}}
\newcommand{\lockfunc}[1]{,\uparrow_{\lockn{#1}}}

Suppose that besides the ordinary substitution rules 
\begin{mathpar}
\inferrule*{~}{\Gamma \yields \cdot : \cdot} \and
\inferrule*{\Gamma \yields \theta : \Delta \and \Gamma \yields a : A[\theta]}{\Gamma \yields (\theta, a/x) : \Delta, x : A} \and
\inferrule*{\Gamma \yields \theta : \Delta}{\Gamma, x : A \yields \wksub{\theta} : \Delta} \and
\inferrule*{\Gamma \yields \theta : \Delta \and \Delta \yields \theta' : \Xi}{\Gamma \yields (\theta' \circ \theta) : \Xi} \\
\inferrule*[fraction={-{\,-\,}-}]{\Gamma \yields \theta : \Delta}{\Gamma, x : A[\theta] \yields (\theta \varfunc{x}) : \Delta, x : A}
\end{mathpar}
we also have
\begin{mathpar}
\inferrule*{\Gamma, i : \Tiny \yields \theta : \Delta}{\Gamma \yields (\theta, i./\lockn{L}) : \Delta,\ctxlock{L}} \and
\inferrule*{~}{\Gamma, \ctxlock{L}, i : \Tiny \yields \counit{\Gamma}{L}{i} : \Gamma}
\end{mathpar}
From these, we can get functoriality, the unit substitution, and the inverse to the former rule
\begin{mathpar}
\inferrule*[fraction={-{\,-\,}-}]{\Gamma \yields \theta : \Delta}{\Gamma,\ctxlock{L} \yields \theta \lockfunc{L} : \Delta,\ctxlock{L}} \and
\inferrule*[fraction={-{\,-\,}-}]{~}{\Gamma \yields \unit{\Gamma}{i}{L} : \Gamma, i : \Tiny, \ctxlock{L}} \and
\inferrule*[fraction={-{\,-\,}-}]{\Gamma \yields \theta : \Delta,\ctxlock{L}}{\Gamma, i : \Tiny \yields \conjinv{\theta}{L}{i} : \Delta}
\end{mathpar}
defined by
\begin{align*}
\theta \lockfunc{L} &:\defeq (\theta \circ \counit{\Gamma}{L}{i}), i./\lockn{L} \\
\unit{\Gamma}{i}{L} &:\defeq (\id_\Gamma \varfunc{i}),  i./\lockn{L} \\
\conjinv{\theta}{L}{i} &:\defeq \counit{\Delta}{L}{i} \circ (\theta \varfunc{i})
\end{align*}

The equations we need to assert are:
\begin{align*}
  (\theta, i./\lockn{L}) \circ \theta' &\defeq (\theta \circ (\theta'\varfunc{i})), i./\lockn{L} \\
  \wksub{\theta, i./\lockn{L}} &\defeq (\theta \circ (\wksub{\id_\Gamma} \varfunc{i})), i./\lockn{L} \\
                                   % &\defeq (\theta, i./\lockn{L}) \circ \wksub{\id_\Gamma} \\
  \theta \circ \counit{\Gamma}{L}{i} &\defeq \counit{\Delta}{L}{i} \circ (\theta \lockfunc{L} \varfunc{i}) \\
  \counit{(\Gamma, j : \Tiny)}{L}{i} \circ (\unit{\Gamma}{i}{L} \varfunc{i}) &\defeq (\wksub{\id_\Gamma}, i/j)
\end{align*}
The last equation is one of the triangle identities. This other one:
\begin{align*}
  (\counit{\Gamma}{K}{i} \lockfunc{L}) \circ \unit{\Gamma, \ctxlock{K}}{i}{L} &\defeq (\id_\Gamma \circ \counit{\Gamma}{K}{i}), i./\lockn{L}
\end{align*}
follows without being asserted separately, by expanding the definition of $-\lockfunc{L}$ and using the first equation.

% Let's expand the left side of the last one:
% \begin{align*}
%   (\counit{\Gamma}{K}{i} \lockfunc{L}) \circ \unit{\Gamma, \ctxlock{K}}{i}{L}
%   &\defeq ((\counit{\Gamma}{K}{i} \circ \counit{(\Gamma,\ctxlock{K},i)}{L}{j}), j./\lockn{L}) \circ \unit{\Gamma, \ctxlock{K}}{i}{L} \\
%   &\defeq (\counit{\Gamma}{K}{i} \circ \counit{(\Gamma,\ctxlock{K},i)}{L}{j} \circ (\unit{\Gamma, \ctxlock{K}}{i}{L} \varfunc{j})), j./\lockn{L} \\
% \end{align*}

\section{Type}

The type former is now made right-adjoint to $\ctxlock{L}$ in the
`obvious' way, following the pattern of \cite{fitchtt}. My choice of
syntax for the term constructors may be where I lose the crowd, but I
will try to justify it in a minute.

% \begin{mathpar}
%   \inferrule*[left=$\rformsym$-form]
%   {\Gamma, \ctxlock{L} \yields A : \univ}
%   {\Gamma \yields \rform{L} A : \univ} \and
%   \inferrule*[left=$\rformsym$-intro]
%   {\Gamma, \ctxlock{L} \yields a : A}
%   {\Gamma \yields \rintro{L} a : \rform{L} A} \and
%   \inferrule*[left=$\rformsym$-elim]
%   {\Gamma, i : \Tiny \yields r : \rform{L} A}
%   {\Gamma \yields \relim{i.r} : A\sublock{L}{i}} \\
%   \relim{i.\rintro{L} a} \defeq a\sublock{L}{i} \and
%   r \defeq \rintro{L}{\relim{i. r\subkey{i}{L}}}
% \end{mathpar}
\begin{mathpar}
  \inferrule*[left=$\rformsym$-form]
  {\Gamma, \ctxlock{L} \yields A : \univ}
  {\Gamma \yields \rform{L} A : \univ} \and
  \inferrule*[left=$\rformsym$-intro]
  {\Gamma, \ctxlock{L} \yields a : A}
  {\Gamma \yields \rintro{L} a : \rform{L} A} \and
  \inferrule*[left=$\rformsym$-elim]
  {\Gamma, i : \Tiny \yields r : \rform{L} A}
  {\Gamma \yields r(\rbind{i}) : A\sublock{L}{i}} \\
  (\rintro{L}{a})(\rbind{i}) \defeq a\sublock{L}{i} \and
  r \defeq \rintro{L}{(r\subkey{i}{L}(\rbind{i}))}
\end{mathpar}

In words:
\begin{itemize}
\item \rulen{$\rformsym$-form} and \rulen{$\rformsym$-intro}: For any
  `$\ctxlock{L}$-locked' term $a : A$, we can amazingly bind the lock
  $\ctxlock{L}$ and form a term $\rintro{L} a : \rform{L} A$. The syntax
  is intended to be reminiscent of an ordinary $\lambda$-binding.

  Reading upwards, going under $\rform{L} - $ or $\rintro{L} -$ means
  that all extant variables get locked by $\ctxlock{L}$, so every
  future use of those variables in $a$ must have an attached
  $-\substuck{t}{L}$ to be well formed.

  If $A$ is a closed type, we will just write $\rformu A$ rather than
  binding an unused lock name.
  
\item \rulen{$\rformsym$-elim}: If using an assumption $i : \Tiny$ we can
  produce a term $r : \rform{L} A$, then we can amazingly apply $r$ to
  the fresh $i$ to form $r(\rbind{i}) : A$. We are free to completely
  ignore the new assumption $i$ in $r$ if we wish, just as a constant
  function may ignore its argument.

  The syntax is a bit insane: to keep the analogy with ordinary
  function application, the variable $i$ is bound in the parentheses
  on the right, but then is \emph{in scope in the body of the function
    to the left}\footnote{If we took Lawvere
  seriously~\cite{lawvere:adjointness-foundations} and wrote function
  application as $xf$, then we would not have this problem!}.
  
\item \rulen{$\rformsym$-beta}: Amazingly binding a lock $\rintro{L} a$
  and then amazingly applying it to $\rbind{i}$ reduces to
  $a\sublock{L}{i}$, in perfect analogy with
  $(\lambda x. b)(a) \defeq b[a/x]$.
  
\item \rulen{$\rformsym$-eta}: Any element $r : \rform{L} A$ is equal to
  one where you immediately bind a lock and apply $r$ to it, in
  analogy with $f \defeq (\lambda x. f(x))$.
\end{itemize}

\subsection{Basic Examples}

First, some maps that are easily definable from the rules. The functor
$\Tiny \to -$ is a monad, and its right adjoint $\rformu{}$
is therefore a comonad.

\begin{definition}
  If $A$ is (for now) a closed type, define a counit map
  $\varepsilon_A : \rformu{A} \to A$ by
  \begin{align*}
    \varepsilon_A &: \rformu{A} \to A \\
    \varepsilon_A(r) &:\defeq r(\rbind{i})
  \end{align*}
  To get a term of $A$, we need a term of $\rformu{A}$ that we can
  amazingly evaluate on an additional assumption $i : \Tiny$. But we
  already have the variable $r : \rformu{A}$, so we have no
  need to use the additional assumption.
\end{definition}

\begin{definition}
  For $f : A \to B$ a closed function, define $\rformu f$ by
  \begin{align*}
    \rformu f &: \rform{L} A \to \rform{K} B \\
    (\rformu f)(r) &:\defeq \rintro{K}{f(r\substuck{i}{K}(\rbind{i}))}
    % \rformu f(r) &:\defeq \rintro{L}{f(\relim{i.r\substuck{i}{L}})}
  \end{align*}
\end{definition}

This should be compared with the definition of function composition,
as the shape of the definition is the same:
\begin{align*}
  f \circ - &: (C \to A) \to (C \to B) \\
  (f \circ -)(r) &:\defeq \lambda c. f(r(c))
\end{align*}

In words, we start with $r : \rform{L} A$. To produce a term of
$\rform{K} B$ we have to produce a `$\lockn{K}$-locked' term of $B$.
There is a function $f : A \to B$ available, so we just have to get a
$\lockn{K}$-locked term of $A$. We cannot amazingly evaluate
$r : \rform{L} A$ on its own because it has become trapped behind
$\ctxlock{K}$. But we \emph{can} amazingly evaluate $r\substuck{i}{K}$
given an additional assumption $i : \Tiny$. This gets us a
$\lockn{K}$-locked term of $A$ which we can apply $f$ to, giving the
$\lockn{K}$-locked term of $B$ that we wanted. This time, the access
to the additional term $i : \Tiny$ was crucial: it is exactly what we
needed to get access $r$ via $r\substuck{i}{K} : \rform{L}{A}$.

If $f$ is not closed then this is not well-typed, because $f$ as a
variable also became locked behind $\ctxlock{L}$. But if \emph{all}
the inputs to the above construction are provided under $\rformu$,
then we can have access to a function $A \to B$ where we need it. In
full generality:
\begin{definition}
  For $A,B : \rformu \univ$ and
  $f : \rform{L}\left((\relim{i.A\substuck{i}{L}}) \to
    (\relim{i.B\substuck{i}{L}})\right)$, define $\rformu f$ by
  \begin{align*}
    \rformu f &: \rform{L}\left(\relim{i.A\substuck{i}{L}}\right) \to \rform{L}\left( \relim{i.B\substuck{i}{L}}\right) \\
    \rformu f(r) &:\defeq \rintro{L}{(\relim{j. f\substuck{j}{L}})(\relim{i.r\substuck{i}{L}})}
  \end{align*}
\end{definition}

This simple example is already very noisy, so to cut down on the
symbols we will introduce a couple of pieces of syntactic sugar.

\subsection{Sugar}

Like ordinary \rulen{$\to$-intro}, and as with any negative type
former, the \rulen{$\rformsym$-intro} rule is right-invertible and so we
will define terms of it via copattern matching~\cite{???}. For
example, we will write
\begin{align*}
  r(\ctxlock{L}, \ctxlock{K}) :\defeq \judge
  \quad \text{to mean} \quad
  r :\defeq \rintro{L}{\rintro{K}{\judge}}
\end{align*}
This integrates nicely with ordinary copattern-style definitions of
functions: we write
\begin{align*}
  f(x,y,\ctxlock{L},z) :\defeq \judge
  \quad \text{to mean} \quad
  f :\defeq \lambda x. \lambda y. \rintro{L}{\lambda z. \judge}
\end{align*}
This syntax makes it easy to see at a glance which locks affect each
variable in the term $\judge$: the $x$ and $y$ here are to the left of
$\ctxlock{L}$ in the list of arguments and so are locked by
$\ctxlock{L}$, whereas $z$ is not locked by anything.

Similarly, we might evaluate some combination of $\to$ and $\rformsym$
by applying it to a tuple of arguments, as in $f(a, b, \rbind{i}, c)$.
The `argument' to a lock is a new bound variable $i$ as in
\rulen{$\rformsym$-elim}, but remember that this variable is now in
scope \emph{to the left} of that argument in the tuple. These compute
in the `obvious' way, with a $\beta$-reduction for each entry in the
list of arguments. If $f$ is defined via the pattern match above, we
find
\begin{align*}
  f(x,y,\ctxlock{L},z)
  :&\defeq \judge \\
  f(a(i), b(i), \rbind{i}, c)
   &\defeq f(a(i))(b(i))(\rbind{i})(c) \\
   &\defeq \left( \lambda x. \lambda y. \rintro{L}{\lambda z. \judge} \right)(a(i))(b(i))(\rbind{i})(c) \\
   &\defeq \left( \lambda x. \lambda y. \rintro{L}{\lambda z. \judge} \right)(a(i))(b(i))(\rbind{i})(c) \\
   &\defeq  \left( \rintro{L}{\lambda z. \judge[a(i)/x][b(i)/y]} \right)(\rbind{i})(c) \\
   &\defeq  \left( \lambda z. \judge[a(i)/x][b(i)/y]\sublock{L}{i} \right)(c) \\
  &\defeq \judge[a(i)/x][b(i)/y]\sublock{L}{i}[c/z]
\end{align*}
We have arranged the syntax of our admissible rules so that function
definition and use click together: comparing
$f(a(i), b(i), \rbind{i}, c)$ and $f(x,y,\ctxlock{L},z)$, the first
arguments become substitutions $[a(i)/x][b(i)/y]$ and the $\rbind{i}$
`argument' becomes a `substitution' $\sublock{L}{i}$.

Any ordinary function is tautologically equal to the `definition'
\begin{align*}
  f(x) :\defeq f(x)
\end{align*}
by $\eta$-expansion. For $\rformsym$, this $\eta$-expansion introduces an
instance of the counit. That is, any term $r : \rform{L}{A}$ is equal to the `definition'
\begin{align*}
  r(\ctxlock{L}) :\defeq r\substuck{i}{L}(\rbind{i})
\end{align*}

For the second piece of syntactic sugar, we will often need to extract
terms of $A$ from assumptions $r : \rformu{A}$ using the counit map
$\varepsilon_A$ defined above. When such assumptions are behind many
context locks, the \rulen{$\rformsym$-elim} rule provides a term
$i : \Tiny$ that can be used to unlock all these context locks at
once, giving us access to $A$ regardless of where $r$ lies in the
context.
\begin{definition}
  If a variable $x : \rform{L} A$ is behind several locks
  $\ctxlocke{\lockn{K}_1} \dots \ctxlocke{\lockn{K}_n}$, then let
  \begin{align*}
    \rget{x} :\defeq (x \stubra{\subkeyoe{i}{\lockn{K}_1},
    \dots, \subkeyoe{i}{\lockn{K}_n}})(\rbind{i}) : A \admbra{\subkeyoe{i}{\lockn{K}_1},
    \dots, \subkeyoe{i}{\lockn{K}_n}}\sublock{L}{i}
  \end{align*}
  in particular, if $x : \rform{L} A$ is behind no locks in the
  context then $\rget{x} :\defeq \varepsilon_A(x)$.
\end{definition}
This notation $\rget{x}$ is intended to evoke the elimination rule
$x_\sharp$ used in cohesive HoTT (and similar). It cannot be
internalised as a function, it is just an admissible piece of syntax.

Using these shorthands, the definition of functoriality is much less
noisy: For $A,B : \rformu \univ$ and
$f : \rform{L}\left(\rget{A} \to \rget{B}\right)$ we have
\begin{align*}
  &\rformu f : \rform{L}\rget{A} \to \rform{L}\rget{B} \\
  &\rformu f(r, \ctxlock{L}) :\defeq \rget{f}(\rget{r})
\end{align*}

\subsection{Adjointness}\label{sec:adjointness}

Now let's look at how $\rformu$ relates to $(\Tiny \to -)$
\begin{definition}
  If $A, B : \univ$ are (for now) closed types, there are maps
  \begin{align*}
    \eta_A &: A \to \rformu(\Tiny \to A) \\
    \varepsilon_B &: (\Tiny \to \rformu B) \to B
  \end{align*}
  given by
  \begin{align*}
    \eta_A(a, \ctxlock{L}, t) &:\defeq a \substuck{t}{L} \\
    \varepsilon_B(f) &:\defeq f(i, \rbind{i})
  \end{align*}
  Allowing the maximum amount of dependency, for \emph{any} $A : \univ$, there is a map
  \begin{align*}
    \eta_A &: A \to \rform{L}(\prd{t : \Tiny} A \substuck{t}{L})
  \end{align*}
  and for \emph{any} $B : \Tiny \to \rformu \univ$ a map
  \begin{align*}
    \varepsilon_B &: \left(\prd{t:\Tiny} \rform{K} B \substuck{j}{K}(t\substuck{j}{K}, \rbind{j})\right) \to B(j, \rbind{j})
  \end{align*}
  with the same definitions as in the closed case.
\end{definition}

\iffalse
Let us typecheck $\varepsilon_B(f) :\defeq f(i, \rbind{i})$ against
that latter expression. The term $f(i)$ has type
$\rform{K} \relim{j.(B \substuck{j}{K})(i \substuck{j}{K})}$, and so
$f(i, \rbind{i})$ has type
\begin{align*}
  &\left(\relim{j.(B \substuck{j}{K})(i
    \substuck{j}{K})}\right)\sublock{K}{i} \\
  &\defeq \relim{j.(B \substuck{j}{K}\sublock{K}{i})(i \substuck{j}{K}\sublock{K}{i})} \\
  &\defeq \relim{j.(B[j/i])(i[j/i])} \\
  &\defeq \relim{j.B(j)}
\end{align*}
which is what we wanted.
or
\begin{align*}
  &\left((B \substuck{j}{K})(i \substuck{j}{K}, \rbind{j})\right)\sublock{K}{i} \\
  &(B \substuck{j}{K}\sublock{K}{i})(i \substuck{j}{K}\sublock{K}{i}, \rbind{j}) \\
  &(B [j/i])(i [j/i], \rbind{j}) \\
  &B(j, \rbind{j})
\end{align*}
\fi

Besides $\varepsilon_B$ not being definable for arbitrary $B$, we have
also seen that $\rformu -$ is not internally functorial. So to what
extent do we actually get the adjointness $(\Tiny \to -) \dashv \rformu -$?
\begin{proposition}
  If $A$ and $B$ are closed types then there is an equivalence
  \begin{align*}
    \Phi : \rformu ((\Tiny \to A) \to B) \to (A \to \rformu B)
  \end{align*}
  given by
  % \begin{alignat*}{2}
  %   g &\mapsto \lambda a. \rintro{L}{\rget{g}(\lambda j.\varkey{L}{j} a)} &&: \rformu((\Tiny \to A) \to B) \to (A \to \rformu B) \\
  %   f &\mapsto \rintro{K}{\lambda h. \relim{i.(\varkey{K}{i} f)(h(i))}} &&: (A \to \rformu B) \to \rformu ((\Tiny \to A) \to B)
  % \end{alignat*}

  % \begin{alignat*}{2}
  %   \hat g(a, \ctxlock{L}) &:\defeq \rget{g}(\lambda j.\varkey{L}{j} a) \\
  %   \hat f(\ctxlock{K}, h) &:\defeq \relim{i.(\varkey{K}{i} f)(h(i))}
  % \end{alignat*}
  \begin{alignat*}{2}
    \Phi(g, a, \ctxlock{L})
    &:\defeq g\substuck{i}{L}(\rbind{i}, \lambda j. a \substuck{j}{L}) \\
    \Phi^{-1}(f, \ctxlock{K}, h)
    &:\defeq f\substuck{k}{K}(h(k), \rbind{k})
  \end{alignat*}
\end{proposition}
\begin{proof}
  Starting with $\Phi^{-1}(\Phi(g))$ fully $\eta$-expanded, we can
  crunch through the composite:
  % \begin{align*}
  %   (\Phi^{-1} (\Phi g))(\ctxlock{K}, h)
  %   &\defeq ((\Phi g) \subkey{k}{K})(h(k), \rbindsym k.) \\
  %   &\defeq (\Phi (g\substuck{k}{K}))(h(k), \rbindsym k.) \\
  %   &\defeq \left( (g\substuck{k}{K}\subkey{i}{L})(\rbind{i}, \lambda j. a \substuck{j}{L}) \right)[h(k)/a]\sublock{L}{k} \\
  %   &\defeq \left( (g\substuck{k\substuck{i}{L}}{K}\substuck{i}{L})(\rbind{i}, \lambda j. a \substuck{j}{L}) \right)[h(k)/a]\sublock{L}{k} \\
  %   &\defeq \left( (g\substuck{k\substuck{i}{L}}{K}\substuck{i}{L})(\rbind{i}, \lambda j. h(k) \substuck{j}{L}) \right)\sublock{L}{k} \\
  %   &\defeq
  %     (g\substuck{k\substuck{i}{L}}{K}\substuck{i}{L}\sublock{L}{k}))(\rbindsym
  %     i., \lambda j. h(k) \substuck{j}{L}\sublock{L}{k})  \\
  %   &\defeq (g\substuck{k\substuck{i}{L}\sublock{L}{k}}{K})(\rbindsym
  %     i., \lambda j. h(k) [j/k]) \\
  %   &\defeq (g\substuck{k[i/k]}{K})(\rbind{i}, \lambda j. h(k)
  %     [j/k]) \\
  %   &\defeq (g\substuck{i}{L})(\rbind{i}, \lambda j. h(j)) \\
  %   &\defeq (g\substuck{i}{L})(\rbind{i}, h)
  % \end{align*}
  \begin{align*}
    &\Phi^{-1}(\Phi(g\substuck{k}{K}), \rbind{k}, h) \\
    &\defeq \Phi(g\substuck{k}{K}, h(k), \rbind{k})
    && \text{(Definition of $\Phi^{-1}$)} \\
    &\defeq \left( (g\stubra{\subkeyo{k}{K},\subkeyo{i}{L}})(\rbind{i}, \lambda j. a \substuck{j}{L}) \right)[h(k)/a]\sublock{L}{k}
    && \text{(Definition of $\Phi$)} \\
    &\defeq \left( (g\stubra{\subkeyo{k}{K},\subkeyo{i}{L}})(\rbind{i}, \lambda j. (h(k)) \substuck{j}{L}) \right)\sublock{L}{k}
    && \text{(Computing $[h(k)/a]$)} \\
    &\defeq (g\stubra{\subkeyo{k}{K},\subkeyo{i}{L}}\sublock{L}{k})(\rbind{i}, \lambda j. (h(k)) \substuck{j}{L}\sublock{L}{k})
    && \text{(Commuting $\sublock{L}{k}$ with application)} \\
    &\defeq (g\substuck{k}{K}[i/k])(\rbind{i}, \lambda j. (h(k)) [j/k])
    && \text{(Computing $\substuck{-}{L}\sublock{L}{k}$)} \\
    &\defeq (g\substuck{i}{K})(\rbind{i}, \lambda j. h(j))
    && \text{(Computing $[j/k]$)} \\
    &\defeq (g\substuck{i}{K})(\rbind{i}, h)
    && \text{($\eta$ for functions)} \\
    &\defeq g
    && \text{($\eta$ for $\rformsym$)}
  \end{align*}

  The other way:
  \begin{align*}
    &\Phi (\Phi^{-1}(f\substuck{i}{L}, a, \rbind{i})) \\
    &\defeq \Phi^{-1}(f\substuck{i}{L}, \rbind{i}, \lambda j. a \substuck{j}{L})
    && \text{(Definition of $\Phi$)} \\
    &\defeq (f\substuck{i}{L}\substuck{k}{K})(h(k), \rbind{k})\sublock{K}{i}[\lambda j. a \substuck{j}{L}/h]
    && \text{(Definition of $\Phi^{-1}$)} \\
    &\defeq (f\substuck{i}{L}\substuck{k}{K}\sublock{K}{i})(h(k), \rbind{k})[\lambda j. a \substuck{j}{L}/h]
    && \text{(Commuting $\sublock{K}{i}$)} \\
    &\defeq (f\substuck{i}{L}[k/i])(h(k), \rbind{k})[\lambda j. a \substuck{j}{L}/h]
    && \text{(Computing $\substuck{k}{K}\sublock{K}{i}$)} \\
    &\defeq (f\substuck{k}{L})(h(k), \rbind{k})[\lambda j. a \substuck{j}{L}/h]
    && \text{(Computing $[k/i]$)} \\
    &\defeq (f\substuck{k}{L})((\lambda j. a \substuck{j}{L})(k), \rbind{k})
    && \text{(Computing $[\lambda j. a \substuck{j}{L}/h]$)} \\
    &\defeq (f\substuck{k}{L})(a \substuck{k}{L}, \rbind{k})
    && \text{($\beta$ for functions)} \\
    &\defeq f
    && \text{($\eta$ for $\rformsym$)}
  \end{align*}

  \iffalse
  Crunching through both directions:
  \begin{align*}
    &\rintro{K}{\lambda h. \relim{i.(\admkey{K}{i} \left(\lambda a. \rintro{L}{\rget{g}(\lambda j.\varkey{L}{j} a)}\right))(h(i))}} \\
    &\defeq \rintro{K}{\lambda h. \relim{i.(\admkey{K}{i} \left(\lambda a. \rintro{L}{(\relim{l.\varkey{L}{l} g})(\lambda j.\varkey{L}{j} a)}\right))(h(i))}} && \text{(Expanding $\rget g$)} \\
    &\defeq \rintro{K}{\lambda h. \relim{i.\left(\lambda a. \rintro{L}{(\relim{l.\varkey{L}{l} \varkey{K}{i} g})(\lambda j.\varkey{L}{j} a)}\right)(h(i))}} && \text{(Computing $\admkey{K}{i}$)} \\
    &\defeq \rintro{K}{\lambda h. \relim{i.\rintro{L}{(\relim{l.\varkey{L}{l} \varkey{K}{i} g})(\lambda j.\admkey{L}{j} h(i))}}} && \text{($\beta$ for $\to$ on $a$)} \\
    &\defeq \rintro{K}{\lambda h. \relim{i.\rintro{L}{(\relim{l.\varkey{L}{l} \varkey{K}{i} g})(\lambda j.(\varkey{L}{j} h)(\varkey{L}{j} i))}}} && \text{(Computing $\admkey{L}{j}$)} \\
    &\defeq \rintro{K}{\lambda h. (\relim{l.\varkey{L}{l} \varkey{K}{i} g})(\lambda j.(\varkey{L}{j} h)(\varkey{L}{j} i))[\sublock{L}{i}]} && \text{($\beta$ for $\rformu$)} \\
    &\defeq \rintro{K}{\lambda h. (\relim{l.\varkey{K}{l} g})(\lambda j.h( j))} && \text{(Computing $\sublock{L}{i}$)} \\
    &\defeq \rintro{K}{\lambda h. (\relim{l.\varkey{K}{l} g})(h)} && \text{($\beta$ for $\to$ on $j$)} \\
    &\defeq \rintro{K}{\relim{l.\varkey{K}{l} g}} && \text{($\beta$ for $\to$ on $h$)} \\
    &\defeq g && \text{($\eta$ for $\rformu$)} \\
  \end{align*}
  and
  \begin{align*}
    &\lambda a. \rintro{L}{(\relim{l.\admkey{L}{l} \left(\rintro{K}{\lambda h. \relim{i.(\varkey{K}{i} f)(h(i))}}\right)})(\lambda j.\varkey{L}{j} a)} \\
    &\defeq \lambda a. \rintro{L}{(\relim{l. \rintro{K}{\lambda h. \relim{i.(\varkey{K}{i} \varkey{L}{l} f)(h(i))}}})(\lambda j.\varkey{L}{j} a)} && \text{(Computing $\admkey{L}{l}$)} \\
    &\defeq \lambda a. \rintro{L}{(\lambda h. \relim{i.(\varkey{K}{i} \varkey{L}{l} f)(h(i))}[\sublock{K}{l}])(\lambda j.\varkey{L}{j} a)} && \text{($\beta$ for $\rformu$)} \\
    &\defeq \lambda a. \rintro{L}{(\lambda h. \relim{i.( \varkey{L}{i} f)(h(i))})(\lambda j.\varkey{L}{j} a)} && \text{(Computing $\sublock{K}{l}$)} \\
    &\defeq \lambda a. \rintro{L}{\relim{i.(\varkey{L}{i} f)((\lambda j.\varkey{L}{j} a)(i))}} && \text{($\beta$ for $\to$ on $h$)} \\
    &\defeq \lambda a. \rintro{L}{\relim{i.(\varkey{L}{i} f)(\varkey{L}{i} a))}} && \text{($\beta$ for $\to$ on $j$)} \\
    &\defeq \lambda a. \rintro{L}{\relim{i.\admkey{L}{i}(f(a))}} && \text{(`Uncomputing' $\admkey{L}{i}$)} \\
    &\defeq \lambda a. f(a) && \text{($\eta$ for $\rformu$)} \\
    &\defeq f && \text{($\eta$ for $\to$)}
  \end{align*}
  \fi
\end{proof}

\begin{remark}
  Internal equivalences of this kind for an arbitrary adjoint modality
  have been defined in MTT, where the modality is instead a positive
  type former, see~\cite[Proposition 3.4]{transpension}
  and~\cite[Section 10.4]{mtt}. The fact that this internal
  formulation circumvents the `no-go' theorem of \cite{lops} was also
  noted in \cite[Section 10.1]{transpension}.
\end{remark}

Happily, we can allow $A$ and $B$ to be dependent types:
\begin{proposition}\label{prop:adj}
  For any $A : \univ$ and $B : \rformu \univ$, there is an equivalence
  \begin{align*}
    \rform{L} ((\prd{t:\Tiny} A\substuck{t}{L}) \to \rget{B}) \to (A \to \rform{L} \rget{B})
  \end{align*}
  with maps defined the same way as above.
\end{proposition}
And in fact, we can also let $B$ depend on $A$. In maximum generality,
\begin{proposition}\label{prop:dep-adj}
  For any $A : \univ$ and $B : A \to \rformu \univ$, there is an
  equivalence
  % \begin{align*}
  %   \left(\prd{a:A} \rform{L} \rget{B(a)}\right) \equiv \rform{L} \left(\prd{f:\prd{t:\Tiny} A\substuck{t}{L}} \relim{i.(B\substuck{i}{L})(f(i))}\right)
  % \end{align*}
  \begin{align*}
    \rform{L} \left(\prd{f:\prd{t:\Tiny} A\substuck{t}{L}} B\substuck{i}{L}(f(i), \rbind{i})\right) \to \prd{a:A} \rform{L} \rget{B(a)}
  \end{align*}
  with maps defined the same way as above. \mvrnote{I admit that the
    notation here is so heavy that it's hard to see the original
    adjunction underneath it...}
\end{proposition}

% But we are actually running into the weak variable rule issue
% already. We want the type of the second one to be
% $\rformu((\Tiny \to A) \to B) \to \rform{K}(A \to \rform{L} B)$, but
% because of the two contexts locks $\ctxlock{\lockn{K}}$ and
% $\ctxlock{\lockn{L}}$, we actually can't access $g$ where we need
% to.

% \begin{lemma}
%If $A$ is closed, the triangle identities hold:
%\begin{align*}
%(\varepsilon_{\Tiny \to A}) \circ (\Tiny \to {\eta_A}) &\defeq \id_{\Tiny \to A} \\
%(\rformu \varepsilon_A) \circ (\eta_{\rformu A}) &\defeq \id_{\rformu A}
%\end{align*}
%\end{lemma}
%We can use functoriality on $\varepsilon_A$ here, because it is a closed function as long as $A$ is a closed type. I think the above could probably be made to work with a non-closed $A : \rformu \univ$, but it would take some fiddling to line things up.
%\begin{proof}
%Let us expand each function on its own, $\alpha$-renaming things so they don't clash.
%\begin{align*}
%(\Tiny \to {\eta_A})(g) &\defeq \lambda s. \rintro{L}{\lambda t. \varkey{L}{t} (g(s))} \\
%(\varepsilon_{\Tiny \to A})(f) &\defeq \relim{i.f(i)}\\
%(\eta_{\rformu A})(x) &\defeq \rintro{L}{\lambda t. \varkey{L}{t} x}\\
%(\rformu \varepsilon_A)(w) &\defeq \rintro{K}{\relim{j.\relim{i.\varkey{K}{i} w}(j)}}
%\end{align*}
%And now composing them and reducing:
%\begin{align*}
%&(\varepsilon_{\Tiny \to A}) \circ (\Tiny \to {\eta_A})(g) \\
%&\defeq \relim{i.\left[\lambda s. \rintro{L}{\lambda t. \varkey{L}{t} (g(s))} \right](i)} \\
%&\defeq \relim{i.\rintro{L}{\lambda t. \varkey{L}{t} (g(i))}} \\
%&\defeq \left(\lambda t. \varkey{L}{t} (g(i))\right)[\sublock{L}{i}] \\
%&\defeq \lambda t. (g(i))[t/i] \\
%&\defeq \lambda t. g(t) \\
%&\defeq g
%\end{align*}
%and
%\begin{align*}
%&(\rformu \varepsilon_A) \circ (\eta_{\rformu A})(x) \\
%&\defeq \rintro{K}{\relim{j.\relim{i.\admkey{K}{i} \left[\rintro{L}{\lambda t. \varkey{L}{t} x}\right]}(j)}} \\
%&\defeq \rintro{K}{\relim{j.\relim{i.\rintro{L}{\lambda t. \varkey{L}{t} \varkey{K}{i} x}}(j)}} \\
%&\defeq \rintro{K}{\relim{j.(\lambda t. \varkey{L}{t} \varkey{K}{i} x)[\sublock{L}{i}](j)}} \\
%&\defeq \rintro{K}{\relim{j.(\lambda t. \varkey{K}{t} x)(j)}} \\
%&\defeq \rintro{K}{\relim{j. \varkey{K}{j} x}} \\
%&\defeq x
%\end{align*}
% \end{proof}
\iffalse
\subsection{Comonad}
$\rformu$ is supposed to be a comonad, because it is right adjoint to
the monad $(\Tiny \to -)$. We could get the comonad structure from the
above adjunction, but the maps are easy to define directly:

\begin{proposition}
  $\rform{}$ is a comonad, where for any $A : \rformu \univ$,
  \begin{alignat*}{2}
    \varepsilon_A &:\defeq (\lambda r. \relim{\_.r}) &&: \rform{L} \rget{A} \to \rget{A} \\
    \delta_A &:\defeq (\lambda s. \rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}s}}}) &&: \rform{L} \rget{A} \to \rform{J} \rform{K} \rget{A}
  \end{alignat*}

  \begin{align*}
    \varepsilon_A(r)
    &:\defeq \relim{\_.r} \\
    \delta_A(s, \ctxlock{J}, \ctxlock{K})
    &:\defeq \relim{i.s\substuck{i}{J}\substuck{i}{K}}
  \end{align*}
  Or even
  \begin{align*}
    \varepsilon_A(r) &:\defeq \rget{r} \\
    \delta_A(s, \ctxlock{J}, \ctxlock{K}) &:\defeq \rget{s}
  \end{align*}
  Or even
  \begin{align*}
    \varepsilon_A(r) &:\defeq r(\rbind{\_}) \\
    \delta_A(s, \ctxlock{J}, \ctxlock{K}) &:\defeq (s\substuck{i}{J}\substuck{i}{K})(\rbind{i})
  \end{align*}
\end{proposition}
\begin{proof}
  Checking these by hand is a pain. A hypothetical proof assistant
  would be convinced by $\refl{}$, because all the identities involved
  are definitional.
  \begin{align*}
    \rformu \varepsilon_A \circ \delta_A
    &: \rform{L} \rget{A} \to \rform{L} \rget{A} \\
    (\rformu \varepsilon_A \circ \delta_A)(r, \rbind{i})
    &:\defeq (\rformu \varepsilon_A \circ \delta_A)(r, \rbind{i}) \\
    &\defeq (\rformu \varepsilon_A)(\delta_A(r, \rbind{i})) \\
    &\defeq (\rformu \varepsilon_A)(\rintro{K}{\delta_A(r\substuck{k}{K}, \rbind{i}, \rbind{k})}) \\
    &\defeq (\rformu \varepsilon_A)(\rintro{K}{(s\substuck{i}{J}\substuck{i}{K})(\rbind{i})}) \\
  \end{align*}

  \begin{align*}
    \rformu \varepsilon_A \circ \delta_A
    &:\defeq \rformu (\lambda r. \relim{\_.r}) \circ (\lambda s. \rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}s}}}) \\
    &:\defeq \lambda r. \rintro{L}{(\lambda r. \relim{\_.r})(\relim{i.\varkey{L}{i}r})} \circ (\lambda s. \rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}s}}}) \\
    &\defeq \lambda r. \rintro{L}{\relim{\_.\relim{i.\varkey{L}{i}r}}} \circ (\lambda s. \rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}s}}}) \\
    &\defeq \lambda r. \rintro{L}{\relim{\_.\relim{i.\admkey{L}{i}\rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}r}}}}}} \\
    &\defeq \lambda r. \rintro{L}{\relim{\_.\relim{i.\rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}\varkey{L}{i}r}}}}}} \\
    &\defeq \lambda r. \rintro{L}{\relim{\_.\rintro{K}{\relim{l.\varkey{K}{l}\varkey{L}{l}r}}}} \\
    &\defeq \lambda r. \rintro{L}{\relim{l.\varkey{L}{l}r}} \\
    &\defeq \lambda r. r \\
    ~\\
    \varepsilon_{\rform{J} A} \circ \delta_A &:\defeq (\lambda r. \relim{\_.r}) \circ (\lambda s. \rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}s}}}) \\
    &\defeq \lambda r. \relim{\_.\rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}r}}}} \\
    &\defeq \lambda r. \rintro{K}{\relim{l.\varkey{K}{l}r}} \\
    &\defeq \lambda r. r \\
  \end{align*}
  \begin{align*}
    \rformu \delta_A \circ \delta_A
    &:\defeq \rformu (\lambda s'. \rintro{J'}{\rintro{K'}{\relim{l'.\varkey{K'}{l'}\varkey{J'}{l'}s'}}})  \circ (\lambda s. \rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}s}}}) \\
    &:\defeq (\lambda r. \rintro{M}{\rintro{J'}{\rintro{K'}{\relim{l'.\admkey{K'}{l'}\admkey{J'}{l'}\relim{i.\varkey{M}{i}{r}}}}}})  \circ (\lambda s. \rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}s}}}) \\
    &\defeq (\lambda r. \rintro{M}{\rintro{J'}{\rintro{K'}{\relim{l'.\relim{i.\varkey{K'}{l'}\varkey{J'}{l'}\varkey{M}{i}{r}}}}}})  \circ (\lambda s. \rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}s}}}) \\
    &\defeq \lambda r. \rintro{M}{\rintro{J'}{\rintro{K'}{\relim{l'.\relim{i.\admkey{K'}{l'}\admkey{J'}{l'}\admkey{M}{i}{\rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}r}}}}}}}}} \\
    &\defeq \lambda r. \rintro{M}{\rintro{J'}{\rintro{K'}{\relim{l'.\relim{i.{\rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}\varkey{K'}{l'}\varkey{J'}{l'}\varkey{M}{i}r}}}}}}}}} \\
    &\defeq \lambda r. \rintro{M}{\rintro{J'}{\rintro{K'}{\relim{l'.\rintro{K}{\relim{l.\varkey{K}{l}\varkey{K'}{l'}\varkey{J'}{l'}\varkey{M}{l}s}}}}}} \\
    &\defeq \lambda r. \rintro{M}{\rintro{J'}{\rintro{K'}{\relim{l.\varkey{K'}{l}\varkey{J'}{l}\varkey{M}{l}r}}}} \\
    ~\\
    \delta_{\rformu A} \circ \delta_A
    &:\defeq (\lambda s'. \rintro{J'}{\rintro{K'}{\relim{l'.\varkey{K'}{l'}\varkey{J'}{l'}s'}}}) \circ (\lambda s. \rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}s}}}) \\
    &\defeq \lambda s'. \rintro{J'}{\rintro{K'}{\relim{l'.\admkey{K'}{l'}\admkey{J'}{l'}\rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}s'}}}}}} \\
    &\defeq \lambda s'. \rintro{J'}{\rintro{K'}{\relim{l'.\rintro{J}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{J}{l}\varkey{K'}{l'}\varkey{J'}{l'}s'}}}}}} \\
    &\defeq \lambda s'. \rintro{J'}{\rintro{K'}{\rintro{K}{\relim{l.\varkey{K}{l}\varkey{K'}{l}\varkey{J'}{l}s'}}}}
  \end{align*}
  which up to $\alpha$-equivalence is the same as the previous.
\end{proof}
$\rformu$ is not typically idempotent, unless $\Tiny$ is a proposition
so that $\Tiny \to \Tiny \times \Tiny$ is an equivalence.
\fi

\subsection{Left Exactness}

We can show that, as a right adjoint, $\rform{}$ preserves $1$ and pullbacks.
\begin{proposition}[$\rformsym$ preserves 1]
  $\rformu{1} \equiv 1$
\end{proposition}
\begin{proof}
  Any term $r : \rformu{1}$ will $\eta$-expand as
  $r \defeq \rintro{L}{r\substuck{i}{L}(\rbind{i})} \defeq
  \rintro{L}{\star}$ and so $\rformu{1}$ is contractible.
\end{proof}

\begin{proposition}[$\rformsym$ preserves $\Sigma$]\label{prop:root-preserve-sum}
  If $A : \univ$ and $B : A \to \univ$ are closed, then
  \begin{align*}
    \rformu \left( \sm{x : A} B(x) \right) \equiv \sm{x : \rformu A} \rformu B(\rget{x})
  \end{align*}
  Generally, if $A : \rformu \univ$ and
  $B : \rformu (\rget{A} \to \univ)$ there is an equivalence
  \begin{align*}
    \rformu \left( \sm{x : \rget{A}}\rget{B}(x) \right) \equiv \sm{x : \rformu \rget{A}} \rformu (\rget{B}(\rget{x}))
  \end{align*}
\end{proposition}
\begin{proof}
  Define maps either way by
  \begin{align*}
    r &\mapsto (\rintro{L}{\proj_1 \rget{r}}, \rintro{K}{\proj_2\rget{r}}) \\
    (s,t) &\mapsto \rintro{L}(\rget{s}, \rget{t})
  \end{align*}
\end{proof}

\begin{proposition}
  For any $A : \rformu{\univ}$ and $r, s : \rformu{\rget{A}}$, there
  is an equivalence
  \begin{align*}
    (r = s) \equiv \rformu \left( \rget{r} = \rget{s} \right)
    % \rform{L} \left( \prd{t : \Tiny} \varkey{L}{t} a(t) =
    %   \varkey{L}{t} a'(t) \right) \equiv \left(\rintro{L}{\lambda
    %   t. \varkey{L}{t} a(t)} =_{\rformu \prd{t : \Tiny}
    %   \varkey{L}{t} A(t)} \rintro{L}{\lambda t. \varkey{L}{t}
    %   a'(t)}\right)
  \end{align*}
\end{proposition}
\begin{proof}
  By the fundamental theorem of $\Idsym$-types, we just have to check
  that for fixed $r : \rformu{\rget{A}}$, the type
  \begin{align*}
    \sm{s : \rformu{\rget{A}}} \rformu \left( \rget{r} = \rget{s} \right)
  \end{align*}
  is contractible. By Proposition~\ref{prop:root-preserve-sum}, this
  type is equivalent to
  \begin{align*}
    \rformu{\left(\sm{x : \rget{A}} \rget{r} = x \right)}
  \end{align*}
  and the interior is a contractible pair.
\end{proof}
This might look more familiar with the left side $\eta$-expanded:
\begin{corollary}[$\rformsym$ preserves $=$]
  $(\rintro{L}{\rget{r}} = \rintro{L}{\rget{s}}) \equiv \rform{L}
  \left( \rget{r} = \rget{s} \right)$
\end{corollary}
% \begin{corollary}[$\rformu$ preserves $=$]
%   If $A : \univ$ and $a,a' : A$ are closed then
%   \begin{align*}
%\left(\rintro{}{a} =_{\rformu A} \rintro{}{a'}\right) \equiv \rformu \left( a =_A a' \right)
%\end{align*}
%and more generally, if $A : \Tiny \to \univ$ and
% $a,a' : \prd{t : \Tiny} A(t)$ then
% \begin{align*}
%\left(\rintro{L}{\lambda t. \varkey{L}{t} a(t)} =_{\rformu \prd{t : \Tiny} \varkey{L}{t} A(t)} \rintro{L}{\lambda t. \varkey{L}{t} a'(t)}\right) \equiv \rform{L} \left( \prd{t : \Tiny} \varkey{L}{t} a(t) = \varkey{L}{t} a'(t) \right)
%\end{align*}
% \end{corollary}
% This is reminiscent of the same fact as for $\sharp$, but things are
% a bit weird because $\sharp$ is a monad and $\rformu$ is a comonad.
% \begin{proof}
%   \begin{align*}
%&\left(\rintro{L}{\lambda t. \varkey{L}{t} a(t)} =_{\rformu \prd{t : \Tiny} \varkey{L}{t} A(t)} \rintro{L}{\lambda t. \varkey{L}{t} a'(t)}\right) \\
%&\equiv \rform{K}{\left(\relim{k.\admkey{K}{k}\rintro{L}{\lambda t. \varkey{L}{t} a(t)}} =_{\prd{t : \Tiny} \varkey{L}{t} A(t)} \relim{k.\admkey{K}{k}\rintro{L}{\lambda t. \varkey{L}{t} a'(t)}}\right)} \\
%&\defeq \rform{K}{\left(\lambda t. \varkey{K}{t} a(t) =_{\prd{t : \Tiny} \varkey{L}{t} A(t)} \lambda t. \varkey{K}{t} a'(t) \right)}
%\end{align*}
%Going for the encode-decode strategy, let $\code $ be defined by
%\begin{align*}
%\code &: \rform{L}{(\prd{t : \Tiny} \varkey{L}{t}A(t))} \to \rform{L}{(\prd{t : \Tiny} \varkey{L}{t}A(t))} \to \univ \\
%\code(u,v) &:\defeq \rform{L} \left(\prd{t : \Tiny} \rget{u}(t) = \rget{v}(t)\right)
%\end{align*}
%so that
%\begin{align*}
%\code(\rintro{L}{\lambda t. \varkey{L}{t} a(t)}, \rintro{L}{\lambda t. \varkey{L}{t} a'(t)})
%&\defeq \rform{L} \left( \prd{t : \Tiny} \varkey{L}{t} a(t) = \varkey{L}{t} a'(t) \right)
%\end{align*}
%\begin{align*}
%\encode : \prd{u,v :\rform{L}{(\prd{t : \Tiny} \varkey{L}{t}A(t))}} (u = v) \to \code(u,v)
%\end{align*}
%\begin{align*}
%\decode : \prd{u,v : \rform{L}{(\prd{t : \Tiny} \varkey{L}{t}A(t))}} \code(u,v) \to (u = v)
%\end{align*}
% \end{proof}

\section{Transpension}\label{sec:transpension}

An equivalent characterisation of a tiny object in a 1-topos, due to
Freyd~\cite[Proposition 1.2]{yetter:tiny}, is an object $\Tiny$ such
that the dependent product functor
\begin{align*}
  \Pi_\Tiny : \mathcal{E}/\Tiny \to \mathcal{E}
\end{align*}
has a right adjoint $\nabla_\Tiny$. This operation was given the name \emph{transpension} in~\cite{dependable-atomicity, transpension}.

If $\Tiny$ is tiny in the ordinary
sense, then in a 1-topos this adjoint $\nabla_\Tiny$ can be defined by the
pullback
\[
  \begin{tikzcd}
    \Sigma_\Tiny \nabla_\Tiny B \ar[r] \ar[d] \arrow[dr, phantom, "\lrcorner", very near start] & \rformu B_\bot \ar[d, "\rformu \mathrm{supp}"] \\
    \Tiny \ar[r, "{(\chi_{\id_\Tiny})^\vee}" swap] & \rformu \Omega
  \end{tikzcd}
\]
where $B_\bot$ is the partial map classifier for $B$ and
$\mathrm{supp} : B_\bot \to \Omega$ is the canonical subobject
$B \rightarrowtail B_\bot$. By definition $\mathrm{supp}$ is the
dependent product of the terminal map $B \to 1$ along
$\mathrm{true} : 1 \to \Omega$.

This construction doesn't do the right thing in HoTT, but something
similar works: for $B : \rformu \univ$, define a type family
$\rdepform{-}{B} : \Tiny \to \univ$ by the pullback
\[
  \begin{tikzcd}
    \sm{t : \Tiny} \rdepform{t}{B} \ar[r] \ar[d] \arrow[dr, phantom, "\lrcorner", very near start] & \rformu \left(\sm{X : \univ} X \to \rget{B} \right) \ar[d, "\rformu \proj_1"] \\
    \Tiny \ar[r, "{(-=\id_\Tiny)^\vee}" swap] & \rformu \univ
  \end{tikzcd}
\]
where the map along the bottom is the transpose of
$(\lambda f. f = \id_\Tiny) : (\Tiny \to \Tiny) \to \univ$.

We can simplify this description a fair amount. Because $\rformu$ commutes with $\Sigma$, the map on the right is
equivalent to the projection
\begin{align*}
  \proj_1 : \sm{X : \rformu \univ} \rform{K}{(\rget{X} \to \rget{B})} \to \rformu \univ
\end{align*}
The fibre of the pullback over a fixed $t : \Tiny$ is then easy to
calculate: it is the fibre of that $\proj_1$ over the value of the bottom map at $t$, namely $\rintro{K}{\prd{s : \Tiny} t\substuck{s}{K} = s}$. We can calculate it by plugging that type in for $X$ and simplifying:
\begin{align*}
  &\rform{L}{(\rget{X} \to \rget{B})}[(\rintro{K}{\prd{s : \Tiny} t\substuck{s}{K} = s})/X] \\
  &\defeq \rform{L}{(X\substuck{l}{L}(\rbind{l}) \to \rget{B})}[\rintro{K}{\prd{s : \Tiny} t\substuck{s}{K} = s}/X] \\
  &\defeq \rform{L}{\left(\left( \rintro{K}{\prd{s : \Tiny} t\substuck{s}{K} = s} \right)\subkey{l}{L}(\rbind{l}) \to \rget{B} \right)} \\
  &\defeq \rform{L}{\left(\left( \rintro{K}{\prd{s : \Tiny} t\stubra{\subkeyo{l\substuck{s}{K}}{L}, \subkeyo{s}{K}} = s}\right)(\rbind{l}) \to \rget{B} \right)} \\
  &\defeq \rform{L}{\left( (\prd{s : \Tiny} t\stubra{\subkeyo{l\substuck{s}{K}}{L}, \subkeyo{s}{K}} = s)\sublock{K}{l} \to \rget{B} \right)} \\
  &\defeq \rform{L}{\left( (\prd{s : \Tiny} t\stubra{\subkeyo{l\substuck{s}{K}}{L}, \subkeyo{s}{K}}\sublock{K}{l} = s) \to \rget{B} \right)} \\
  &\defeq \rform{L}{\left( (\prd{s : \Tiny} t\substuck{l[s/l]}{L} = s) \to \rget{B} \right)} \\  
  &\defeq \rform{L}{\left( (\prd{s : \Tiny} t\substuck{s}{L} = s) \to \rget{B} \right)}
\end{align*}
and so we take this as our definition.
\begin{definition}
  For $B : \rformu \univ$, define the \emph{transpension} $B^{1/-} : \Tiny \to \univ$ to be
  \begin{align*}
    \rdepform{t}{B} :\defeq \rform{L}{\left( (\prd{s : \Tiny} t\substuck{s}{L} = s) \to \rget{B} \right)}
  \end{align*}
\end{definition}
\mvrnote{This looks really close to something we can apply dependent adjointness to directly, but I don't think there's a way to rewrite $t\substuck{s}{L} = s$ in the form $?\subkey{s}{L}$}

The whole point of this construction was to be a right adjoint to the dependent product with $\Tiny$, and indeed it is:
\begin{proposition}
  For $A : \Tiny \to \univ$ and $B : \rformu \univ$
  \begin{align*}
    \rform{L} \left( \left(\prd{s : \Tiny} A\substuck{s}{L}(s)\right) \to \rget{B} \right) \equiv \left(\prd{t : \Tiny} A(t) \to \rdepform{t}{B} \right)
  \end{align*}
\end{proposition}
\begin{proof}
  To apply dependent adjointness (Proposition~\ref{prop:dep-adj}) we
  need to massage the interior of the $\rform{L}$ a little. Let $P$
  denote the type family
  \begin{align*}
    &P : \left(\sm{t : \Tiny} A(t)\right) \to \rformu{\univ} \\
    &P(t, a, \ctxlock{K}) :\defeq (\prd{s:\Tiny} t\substuck{s}{K} t = s) \to \rget{B}
  \end{align*}
  Then
  \begin{align*}
    &\rform{L} \left(\left(\prd{s:\Tiny} (A\substuck{s}{L})(s)\right) \to \rget{B} \right) \\
    &\equiv \rform{L} \left(\left(\prd{s:\Tiny}\sm{t : \Tiny} {a : A\substuck{s}{L}(t)} (t = s) \right)\to \rget{B} \right) && \text{(Contractible pair)} \\
    &\equiv \rform{L} \left(\prd{f:\prd{t':\Tiny} \sm{t : \Tiny} A\substuck{t'}{L}(t)} \left(\prd{s:\Tiny} \proj_1(f(i)) = s\right) \to \rget{B} \right)  && \text{(Univ. property of $\Sigma$)} \\
    &\defeq \rform{L} \left(\prd{f:\prd{t':\Tiny} \sm{t : \Tiny} A\substuck{t'}{L}(t)} P\substuck{i}{L}(f(i), \rbind{i})\right) && \text{(Definition of $P$)} \\
    &\equiv \prd{(t,a) : \sm{t : \Tiny} A(t)} \rform{L}{(P\substuck{i}{L})(t\substuck{i}{L},a\substuck{i}{L}, \rbind{i})} && \text{(Proposition~\ref{prop:dep-adj})} \\
    &\defeq \prd{(t,a) : \sm{t : \Tiny} A(t)} \rform{L}{\left((\prd{s : \Tiny} t \substuck{s}{L} = s) \to \rget{B}\right)} && \text{(Definition of $P$)} \\
    &\defeq \prd{(t,a) : \sm{t : \Tiny} A(t)} \rdepform{t}{B} && \text{(Definition of $B^{1/t}$)} \\
    &\equiv\prd{t : \Tiny} A(t) \to \rdepform{t}{B} && \text{(Currying)}
  \end{align*}

  \iffalse
  To apply dependent adjointness (Proposition~\ref{prop:dep-adj}) we
  need to massage the interior of the $\rform{L}$ a little. Define
  \begin{align*}
    &P : \left(\sm{t : \Tiny} A(t)\right) \to \rformu{\univ} \\
    &P(t,a) :\defeq \rintro{K}{(\prd{s:\Tiny} \varkey{K}{s} t = s) \to \rget{B}}
  \end{align*}
  so that
  \begin{align*}
    &\relim{i.(\admkey{L}{i}P)(\admkey{L}{i}(t,a))} \\
    &\defeq \relim{i.(\admkey{L}{i}(\lambda (t,a). \rintro{K}{(\prd{s:\Tiny} \varkey{K}{s} t = s) \to \rget{B}}))(\admkey{L}{i}(t,a))} \\
    &\defeq \relim{i.(\lambda (t,a). \rintro{K}{(\prd{s:\Tiny} \varkey{K}{s} t = s) \to \rget{(\varkey{L}{i}B)}})(\varkey{L}{i} t, \varkey{L}{i}a)} \\
    &\defeq \relim{i.\rintro{K}{(\prd{s:\Tiny} \varkey{K}{s} \varkey{L}{i} t = s) \to \rget{(\varkey{L}{i}B)}}} \\
    &\defeq (\prd{s:\Tiny} \varkey{L}{s} t = s) \to \rget{B}
  \end{align*}
  is exactly the interior of $\rform{L}$ in the definition of
  $\rdepform{t}{B}$.

  Then
  \begin{align*}
    &\prd{t : \Tiny} A(t) \to \rdepform{t}{B} \\
    &\equiv \prd{(t,a) : \sm{t : \Tiny} A(t)} \rdepform{t}{B} && \text{(Currying)} \\
    &\defeq \prd{(t,a) : \sm{t : \Tiny} A(t)} \rform{L}{\left((\prd{s : \Tiny} \varkey{L}{s} t = s) \to \rget{B}\right)} && \text{(Definition)} \\
    &\defeq \prd{(t,a) : \sm{t : \Tiny} A(t)} \rform{L}{\relim{i.(\admkey{L}{i}P)(\admkey{L}{i}(t,a))}} && \text{(Above calculation)} \\
    &\equiv \rform{L} \left(\prd{f:\prd{t':\Tiny} \sm{t : \Tiny} (\varkey{L}{t'}A)(t)} \relim{i.(\varkey{L}{i}P)(f(i))}\right) && \text{(Proposition~\ref{prop:dep-adj})} \\
    &\defeq \rform{L} \left(\prd{f:\prd{t':\Tiny} \sm{t : \Tiny} (\varkey{L}{t'}A)(t)} \left(\prd{s:\Tiny} \proj_1(f(i)) = s\right) \to \rget{B} \right)&& \text{(Definition of $P$)} \\
    &\equiv \rform{L} \left(\left(\prd{s:\Tiny}\sm{t : \Tiny} {a : (\varkey{L}{s}A)(t)} (t = s) \right)\to \rget{B} \right) && \text{(Univ. property of $\Sigma$)} \\
    &\equiv \rform{L} \left(\left(\prd{s:\Tiny} (\varkey{L}{s}A)(s)\right) \to \rget{B} \right) && \text{(Contractible pair)}
  \end{align*}
  is what we wanted to show.
  \fi
\end{proof}

\begin{corollary}
  $\left(\prd{t : \Tiny} \rdepform{t}{B} \right) \equiv \rformu
  \rget{B}$
\end{corollary}
\begin{proof}
  Plug in $A \defeq \const_1$ in the above.
\end{proof}


% \begin{lemma}
%   If $0 : \Tiny$ then
%   $((\Tiny \to A) \to B) \equiv (A \to \rform{?} B)$
% \end{lemma}
% \begin{proof}
%   Suppose $f : ((\Tiny \to A) \to B)$, can start with
%   $\lambda a. \rintro{L}{?}$, but now we are stuck. We want to use
%   $f$ but it is locked, and we don't have a $t : \Tiny$ to let us
%   use it.
%
%   So let's just say $f$ is a closed term. Then we are unstuck:
%   \begin{align*}
%\mathsf{form}(f) :\defeq \lambda a. \rintro{L}{ (\varkey{L}{0} f)(\lambda t. \varkey{L}{t} a)} : (A \to \rform{?} B)
%\end{align*}
%
%If $g : (A \to \rform{?} B)$, then can define
%\begin{align*}
%\mathsf{function}(g) :\defeq \lambda h. \relim{i. g(h(i))} : ((\Tiny \to A) \to B)
%\end{align*}
%without needing $g$ to be closed.
%
%Now to try round trips. For this we do need $g$ to be closed or
% composing doesn't make sense.
% \begin{align*}
%&\mathsf{form}(\mathsf{function}(g))  \\
%&\defeq \lambda a. \rintro{L}{ (\varkey{L}{0} (\mathsf{function}(g)))(\lambda t. \varkey{L}{t} a)} \\
%&\defeq \lambda a. \rintro{L}{ (\mathsf{function}(\varkey{L}{0} g))(\lambda t. \varkey{L}{t} a)} \\
%&\defeq \lambda a. \rintro{L}{ (\lambda h. \relim{i. (\varkey{L}{0} g)(h(i))})(\lambda t. \varkey{L}{t} a)} \\
%&\defeq \lambda a. \rintro{L}{ \relim{i. (\varkey{L}{0} g)((\lambda t. \varkey{L}{t} a)(i)))}} \\
%&\defeq \lambda a. \rintro{L}{ \relim{i. (\varkey{L}{0} g)(\varkey{L}{i} a)}}
%\end{align*}
%And the other:
%\begin{align*}
%&\lambda h. \relim{i. (\lambda a. \rintro{L}{ f(\lambda t. \varkey{L}{t} a)})(h(i))} \\
%&\defeq \lambda h. \relim{i. \rintro{L}{ f(\lambda t. \varkey{L}{t} (h(i)))}}\\
%&\defeq \lambda h. \relim{i. \rintro{L}{ f(\lambda t. \varkey{L}{t} h(\varkey{L}{t} i))}}\\
%&\defeq \lambda h. f(\lambda t. \varkey{L}{t} h(\varkey{L}{t} i))[\sublock{L}{i}]\\
%&\defeq \lambda h. f(\lambda t. h(t))\\
%&\defeq \lambda h. f(h) \\
%&\defeq f
%\end{align*}
% \end{proof}

% If we try to make rules for this directly and build in the required
% substitutions, we get something horrible like
% \begin{mathpar}
%   \inferrule*[left=$\rformsym$-intro]{\Gamma, \ctxlock{L} \yields B
%   \type \and \Gamma \yields t : \Tiny}{\Gamma \yields
%   \rdepform{t}{B} \type} \and \inferrule*[left=$\rformsym$-intro]{\Gamma
%   \yields t' : \Tiny \and \Gamma, \ctxlock{L} \yields t : \Tiny \and
%   \Gamma, \ctxlock{L} \yields a : A(t) \and \Gamma, \ctxlock{L}, f :
%   \prd{t : \Tiny} A \yields b : B}{\Gamma \yields
%   \rintro{L}{f.b,t,a} : \rdepform{t}{B}} \and
%   \inferrule*[left=$\rformsym$-elim]{\Gamma, i : \Tiny \yields r :
%   \rdepform{i}{B}}{\Gamma \yields \relim{i.r} : B}
% \end{mathpar}
% where we need \emph{two} terms of $\Tiny$ in the intro rule, one to
% use in the function $f$, and the second to get past the resulting
% lock in the conclusion.

A surprising fact is that the pullback of $\Tiny$ to any slice
$\mathcal{E}/X$ is itself also tiny~\cite[Theorem 1.4]{yetter:tiny},
but crucially, the right adjoint $\rformsym$ is not preserved by
pullback.

Instead, the right adjoint $\rformslicesym{X}$ on an object
$D \to X$ can be calculated by the pullback
\[
  \begin{tikzcd}
    \Sigma_X \rformslicesym{X} D \ar[r] \ar[d] & \rformu (\Sigma_{\Tiny \to X} \Pi_c D) \ar[d, "\rformu \Pi_c D"] \\
    X \ar[r, "\eta" swap] & \rformu (\Tiny \to X)
  \end{tikzcd}
\]
where $c : X \to (\Tiny \to X)$ is the transpose of the projection
$X \times \Tiny \to X$, and the $\rformsym$ on the right is the global
adjoint to $(\Tiny \to -)$. This can also be described internally, but I have not come across a use for it.

\iffalse
Let us describe this internally. Suppose $X$ is a closed
type. Switching perspective from the slice over $X$ to type families
over $X$, we first calculate the dependent product of a type family
$D : X \to \univ$ along the map $c : X \to (\Tiny \to X)$. This is

\begin{align*}
  \sm{f : \Tiny \to X} (\prd{x' : X} (c(x') = f) \to D(x'))
\end{align*}
with the first projection down to $\Tiny \to X$. We now need to apply
$\rformsym$. Similar to transpension, because
$\rformsym$ commutes with pullbacks this is
\begin{align*}
  \sm{f : \rform{L}{\Tiny \to X}} \rform{L}{\left(\prd{x' : X} (c(x') = (f\substuck{i}{L})(\rbind{i})) \to D(x')\right)}
\end{align*}
To pull back along $\eta$ and calculate the fibre over $x : X$, we can
simply substitute:

\begin{align*}
  &\rform{L}{\left(\prd{x' : X} (c(x') = (\eta(x)\substuck{i}{L})(\rbind{i})) \to D(x')\right)} \\
  \equiv &\rform{L}{\left(\prd{x' : X} (c(x') = (\eta(x\substuck{i}{L}))(\rbind{i})) \to D(x')\right)} \\
  \equiv &\rform{L}{\left(\prd{x' : X} (c(x') = (\rintro{K}{\lambda k. x\substuck{i}{L}\substuck{k}{K}}))(\rbind{i})) \to D(x')\right)} \\
  \equiv &\rform{L}{\left(\prd{x' : X} (c(x') = (\lambda k. x\substuck{i}{L}\substuck{k}{K}\subkey{i}{K}) \to D(x')\right)} \\
  \equiv &\rform{L}{\left(\prd{x' : X} (c(x') = (\lambda k. x\substuck{k}{L}) \to D(x')\right)} \\
  \equiv &\rform{L}{\left(\prd{x' : X} \left( \prd{k : \Tiny} (x' = x\substuck{k}{L})\right) \to D(x')\right)} \\
\end{align*}
\fi

\iffalse
\section{$\Tiny$-discreteness}
\begin{definition}
  A type $A : \univ$ is \emph{$\Tiny$-discrete} if the weakening map
  $A \to (\Tiny \to A)$ is an equivalence.
\end{definition}

\mvrnote{In \cite{yetter:tiny} it is proven that $\Tiny$-discrete
  objects form a reflective and coreflective subcategory, at least in
  the 1-topos case. Does it work here? We can use a nullification HIT
  to build the reflection, but I can't get that to be equivalent to
  the coequaliser definition in Yetter}
\fi

\section{Tininess Closure Properties}

\newcommand{\trform}[2]{\sqrt[#1]{}#2}

An external definition for now:
\begin{definition}
  A type $S$ is \emph{tiny} if for any closed type $X$ there is a type $\trform{S}{X}$ and a map
  \begin{align*}
    (S \to \trform{S}{X}) \to X
  \end{align*}
  that induces a bijection on homspaces or whatever
\end{definition}

Or something more circular?
\begin{definition}
  A type $S$ is \emph{tiny} if there is a map $\trform{S}{-} : \trform{S}{\univ} \to \univ$ so that for any $X : \univ$ there is a map
  \begin{align*}
    \eta_X : X \to \trform{S}{S \to X}
  \end{align*}
  such that the precomposition map
  \begin{align*}
    \trform{S}{X}
  \end{align*}
\end{definition}

For example:
\begin{proposition}
  If $S$ and $T$ are tiny then $S \times T$ is tiny.
\end{proposition}


\section{Internal Models of Cubical Type Theory}

Finally, a little commentary on cubical type theory. Let us repeat the
construction of \cite[Theorem 5.2]{lops}, and see whether anything
becomes more explicit.

The ambient type theory is intensional, predicative MLTT with function extensionality and UIP: we therefore denote the
ambient universe $\Set$ rather than $\univ$, and aim to construct a
new universe $\univfib$ that classifies fibrations. We also have an
interval type $\Int$, which is assumed to be tiny.

The main piece of input data is a \emph{notion of composition
  structure}, which is a function $\Compstr : (\Int \to \Set) \to \Set$ that
parameterises the notion of fibration. There are some derived structures:
\begin{align*}
  \isFib &: \prd{\Gamma : \Set}{A : \Gamma \to \Set} \Set \\
  \isFib(\Gamma)(A) &:\defeq \prd{p : \Int \to \Gamma} \Compstr(A \circ p) \\
  \Fib &: \Set \to \Set \\
  \Fib(\Gamma) &:\defeq \sm{A : \Gamma \to \Set} \isFib(\Gamma)(A)
\end{align*}

The original construction is done in crisp type theory, with an
interval asserted to be tiny by axiomatically adding a ``crisp
adjunction''
\begin{align*}
  \flat((\Int \to A) \to B) \equiv \flat(A \to \rformu{B})
\end{align*}
The types in our construction will be a little different: the
$\rformu$ former itself is used to guard the adjunction, as we saw in
Section~\ref{sec:adjointness}.

The construction proceeds the same way as in \cite{lops}. The
universe classifying fibrations is constructed by the pullback
\[
  \begin{tikzcd}
    \univfib \ar[r] \ar[d] \arrow[dr, phantom, "\lrcorner", very near start] & \rformu \sm{A : \Set} A \ar[d, "\rformu \proj_1"] \\
    \Set \ar[r, "\Compstr^\vee" swap] & \rformu \Set
  \end{tikzcd}
\]
By definition,
\begin{align*}
  \Compstr^\vee(X) :\defeq \rintro{L}{\Compstr(\lambda j. X\substuck{j}{L})}
\end{align*}

For the second time in this note, we calculate a pullback directly by
commuting $\rformsym$ with $\Sigma$ and substituting. The convenient definition of $\univfib$ is then
\begin{align*}
  \univfib
  &:\defeq \sm{X : \Set} \rformu{\rget{A}} [\Compstr^\vee(X)/A] \\
  % &\defeq \sm{X : \Set} \rformu{(A\substuck{i}{L})(\rbind{i})} [\Compstr^\vee(X)/A] \\
  % &\defeq \sm{X : \Set} \rform{K}{(\Compstr^\vee(\substuck{i}{K}))(\rbind{i})} \\
  &\defeq \sm{X : \Set} \rform{L}{\Compstr(\lambda j. X\substuck{j}{L})}
\end{align*}

The projection maps in the original pullback square are given by
\begin{align*}
  &\pi_1 : \univfib \to \Set \\
  &\pi_1(X, r) :\defeq X \\
  &\pi_2 : \univfib \to \rformu \sm{A : \Set} A \\
  &\pi_2(X, r, \ctxlock{L}) :\defeq (\Compstr(\lambda j. X\substuck{j}{L}), \rget{r})
\end{align*}

The map $\pi_2$ can be transposed back to
\begin{align*}
  \pi_2{}_\vee
  &: (\Int \to \univfib) \to \sm{A : \Set} A \\
  \pi_2{}_\vee(p)
  &:\defeq \pi_2(p(k), \rbind{k}) \\
  &\defeq \pi_2(\proj_1 p(k), \proj_2 p(k), \rbind{k}) \\
  &\defeq (\Compstr(\lambda j. (\proj_1 p(k))\subkey{j}{L}), \rget{(\proj_2 p(k))})\sublock{L}{k} \\
  &\defeq (\Compstr(\lambda j. \proj_1 p(j)), (\proj_2 p(i))(\rbind{i}))
\end{align*}
And so we have a explicit definition of $\El$ for $\univfib$:
\begin{align*}
  \El &: \Fib \univfib \\
  \El &:\defeq (\pi_1, \lambda p. (\proj_2 p(i))(\rbind{i}))
\end{align*}

We can also define a map
\begin{align*}
  \code : \prd{\Gamma : \rformu \Set}{\Phi : \rformu (\Fib \Gamma)} \Gamma \to \univfib
\end{align*}
as in the paper.

But looking at this construction, things are much simpler if we
slightly change the definition of $\Fib$. Surrounding the body of $\isFib$ with a $\rformsym$, define
\begin{align*}
  \isNewFib(\Gamma)(A) :\defeq \rform{L}{\left(\prd{p : \prd{i : \Int} \Gamma\substuck{i}{L}} \Compstr(\lambda i. (A\substuck{i}{L})(p(i)))\right)}
\end{align*}
The counit for $\rformsym$ gives a function
$\isNewFib(\Gamma)(A) \to \isFib(\Gamma)(A)$, which induces a map
$\NewFib(\Gamma) \to \Fib(\Gamma)$.

Unchanged, the type $\univfib$ defined above classifies \emph{non-crisp}
fibrations, in that there is an equivalence between non-crisp
functions $\Gamma \to \univfib$ and $\NewFib(\Gamma)$.

This is clear once we simplify further... The definition of
$\isNewFib$ is precisely of the shape to apply dependent
adjointness, and
\begin{align*}
  \isNewFib(\Gamma)(A) \equiv \prd{g : \Gamma} \rform{L}{\Compstr(\lambda i. A\substuck{i}{L}(g))})
\end{align*}
so
\begin{align*}
  \NewFib(\Gamma) &:\defeq \sm{A : \Gamma \to \Set} \isNewFib(\Gamma)(A) \\
                  &\equiv \sm{A : \Gamma \to \Set} \prd{g : \Gamma} \rform{L}{\Compstr(\lambda i. A\substuck{i}{L}(g))} \\
                  &\equiv \Gamma \to \sm{A : \Set} \rform{L}{\Compstr(\lambda i. A\substuck{i}{L})} 
\end{align*}
and the codomain is exactly the definition of $\univfib$. We get an
element of $\NewFib \univfib$ tautologically, running the identity
$\univfib \to \univfib$ backwards through that equivalence.

\iffalse
\subsection{CCHM}
\label{sec:cchm}

\newcommand{\cof}{\mathsf{cof}}
\newcommand{\Cof}{\mathsf{Cof}}
\newcommand{\CCHMcomp}{\mathsf{CCHM}}
\newcommand{\Fill}{\mathsf{Fill}}
\newcommand{\extrel}{{\nnearrow}}

Now recall the \emph{CCHM composition structure}. For the definition
we need a couple of additions to the theory:
\begin{align*}
  0, 1 : \Int \\
  \cof : \Set \to \Set \\
\end{align*}

The extension relation is defined by
\begin{align*}
f \extrel x :\defeq (u : \varphi) \to (f(u) = x)
\end{align*}

\begin{definition}
  \begin{align*}
    \CCHMcomp &: (\Int \to \Set) \to \Set \\
    \CCHMcomp(P) &:\defeq (\varphi : \Cof)(p : (i : \Int) \to \varphi \to P(i)) \to
                   \left( \sm{a_0 : P(0)} p(0) \extrel a_0 \right) \to
                   \left( \sm{a_0 : P(1)} p(1) \extrel a_1 \right)
  \end{align*}
\end{definition}

The derived notion of filling can be defined
\begin{align*}
  \Fill(A) &: (\Int \to \Set) \to \Set \\
  \Fill(A) &:\defeq (\varphi : \Cof)(f : (i : \Int) \to \varphi \to A(i))
             (a : \sm{a' : A(0)} f(0) \extrel a') \to
             \sm{g : (i : \Int) \to P(i)} f \extrel g \times g(0) = a
\end{align*}

But we might want something different.



\begin{lemma}
  Given $A : \Set$ and $\isFib(A)$, \mvrnote{from comp to fill}
\end{lemma}

\begin{proposition}
  If $A_1 : \univfib$ and $A_2 : A_1 \to \univfib$, there is a
  fibration structure $\isFib\left( \sm{x : A_1} A_2(x) \right)$.
\end{proposition}
\begin{proof}

\end{proof}

\section{Tiny Objects in Synthetic Differential Geometry}

\iffalse
\section{Path Types}
  \newcommand{\coe}{\mathsf{coe}} \newcommand{\coh}{\mathsf{coh}}
  \newcommand{\OTO}{\mathsf{IsOTO}} \newcommand{\oto}{\mathsf{oto}}

  I am strongly reminded of~\cite[Section
  2.3]{altenkirch-kaposi:without-interval}, whose $\Gamma^=$ looks an
  awful lot like our $\Gamma, \lock$ supposing two points
  $0, 1 : \Tiny$, and whose `logical relation at a type' looks an
  awful lot like a pair of maps
  \begin{align*}
    (-)^{*T} &: \prd{A:\univ} \rform{L}\left(\varkey{L}{0}A \to \varkey{L}{1}A \to \univ\right) \\
    (-)^{*t} &: \prd{\{A:\univ\}} {a : A}  \rform{L}\left((\rget{A})^{*T}(\varkey{L}{0}a,\varkey{L}{1}a)\right)
  \end{align*}
  (where $A : \univ$ is implicit in the second map) or combining them
  into one map
  \begin{align*}
    (-)^* &: \prd{\{A:\univ\}} {a : A} \rform{L}\left(\rget{(\univ^*(A))}(\varkey{L}{0}a,\varkey{L}{1}a)\right)
  \end{align*}
  relying on the definition
  \begin{align*}
    \univ^* :\defeq \rintro{L}{\lambda A. \lambda B. A \to B \to \univ}
  \end{align*}

  \subsection{IsEquiv}

  Following~\cite[Section 2.8]{altenkirch-kaposi:without-interval},
  what we really want is for paths in $\univ$ to be equivalences. We
  instead want something like
  \begin{align*}
    (-)^* &: \prd{\{A:\univ\}} {a : A} \rform{L}\left(\proj_1 \rget{(\univ^*(A))}(\varkey{L}{0}a,\varkey{L}{1}a)\right) \\
    \univ^* &:\defeq \rintro{L}{\lambda A.\lambda B. \sm{R: A \to B \to \univ} \prd{a : A} \isContr(\sm{b : B} R(a,b)) \times \prd{b : B} \isContr(\sm{a : A} R(a,b))}
  \end{align*}
  The actual $\univ^*$ that they use is, for all $A,B : \univ$, the
  iterated $\Sigma$ of
  \begin{align*}
    R &: A \to B \to \univ \\
    \coe^0 &: A \to B \\
    \coh^0 &: \prd{x:A} R(x, \coe^0 x) \\
    \coe^1 &: B \to A \\
    \coh^1 &: \prd{y : B} R(\coe^1 y, y) \\
      &\dots
  \end{align*}
  (plus a couple more fields)

  The hard one in that paper is $\Pi$-types, so let's skip to trying
  to define $(A \to B)^*$ for $A,B : \univ$. Under a lock
  $\ctxlock{L}$ we have to produce
  \begin{align*}
    (A \to B)^* &: (\varkey{L}{0}A \to \varkey{L}{0}B)\to (\varkey{L}{1}A \to \varkey{L}{1}B) \to \univ \\
    \coe^0 &: (\varkey{L}{0}A \to \varkey{L}{0}B)\to (\varkey{L}{1}A \to \varkey{L}{1}B) \\
    \coh^0 &: \prd{f : \varkey{L}{0}A \to \varkey{L}{0}B} R(f, \coe^0 f) \\
    \coe^1 &: (\varkey{L}{1}A \to \varkey{L}{1}B) \to (\varkey{L}{0}A \to \varkey{L}{0}B)  \\
    \coh^1 &: \prd{g : \varkey{L}{1}A \to \varkey{L}{1}B } R(\coe^1 g, g)
  \end{align*}
  The relation is defined is defined by pointwise relatedness:
  \begin{align*}
    (A \to B)^*(f_0, f_1) :\defeq \prd{x_0 : \varkey{L}{0}A}{x_1 : \varkey{L}{1}A}{r : \rget{(A^*)}(x_0, x_1)} \rget{(B^*)}(f_0(x_0), f_1(x_1))
  \end{align*}
  The $\coe$ can be defined easily
  \begin{align*}
    \coe^0(f_0,a_1) :\defeq \rget{(\coe^0_B)}(f_0(\rget{(\coe^1_A)}(a_1)))
  \end{align*}
  and now $\coh$ is the interesting one, but here we get stuck.

  We can sort of define filling the `top' of a box for any $A : \univ$
  \begin{align*}
    \mathsf{top}_A &: \rform{L} \left(\prd{x_0 : \varkey{L}{0}A}{x_1 : \varkey{L}{1}A} \rform{K} \left( (\relim{i. \varkey{K}{0} \varkey{L}{i} A^*})(\varkey{K}{0}x_0, \varkey{K}{0} x_1) \to (\relim{i. \varkey{K}{1} \varkey{L}{i} A^*})(\varkey{K}{1}x_0, \varkey{K}{1} x_1) \right) \right) \\
    \mathsf{top}_A &:\defeq \rintro{L}{\lambda x_0. \lambda x_1. \rintro{K}{\relim{k.\coe^0_{(\relim{i. \varkey{K}{k}\varkey{L}{i} A^*})(\varkey{K}{k}x_0,\varkey{K}{k}x_1)}}}}
  \end{align*}
  But this isn't enough, we need to allow arbitrary relations for
  $x_0$ and $x_1$, not just `refl'. And here we truly are stuck,
  because we don't have a substitution roughly like
  $x_0, x_1, R(x_0, x_1) \yields x, \ctxlock{L}$.

  Would need a backwards map
  \begin{align*}
    ? &: \prd{A:\univ} \rform{L}\left(\sm{x_0 : \varkey{L}{0}A}{x_1 : \varkey{L}{1}A} \rget{A^*}(x_0, x_1) \to \prd{t:\Tiny} \varkey{L}{t}A \right)
  \end{align*}
  that computes, is such a thing reasonable? This is feeling not good.

  \subsection{OTO}

  Mike had a different suggestion in his MURI talk for how the
  relation on $\univ$ should work. I am going to try and write this
  using a $\rformu$. For a relation $R : A \to B \to \univ$,
  coinductively $\OTO(R)$ has destructors
  \begin{align*}
    \OTO(R) &\to \left(\prd{a : A} \sm{b : B} R(a,b)\right) \times \left(\prd{b : B} \sm{a : A} R(a,b)\right) \\
    % \OTO(R) &\to \rform{L} \prd{a_0 : \varkey{L}{0}A}{b_0 : \varkey{L}{0}B}{r_0 : (\varkey{L}{0}R)(a_0,b_0))}{a_1 : \varkey{L}{1}A}{b_1 : \varkey{L}{1}B}{r_1 : (\varkey{L}{1}R)(a_1,b_1))} \\
    % &\quad\quad\quad \OTO\left(\lambda a_2. \lambda b_2. (\proj_1
    %   \rget{R^*}(a_0, a_1, a_2)(b_0,b_1,b_2))(r_0,r_1)\right)
\OTO(R) &\to \prd{a : A}{b : B}{r : R(a,b)} \rform{L} \OTO\left(\relim{i.(\varkey{L}{i}R)^*}\right)
\end{align*}
This relies on the definition of $\univ^*$ and $(A \to B)^*$ being the ones below.

Let's name things in a similar way to the cubical paper, and call $R$ and the non-recursive fields of $\OTO(R)$
\begin{align*}
\coe &: A \to B \\
\coh &: \prd{x:A} \Id(x, \coe x) \\
\coe^{-1} &: B \to A \\
\coh^{-1} &: \prd{y : B} \Id(\coe^{-1} y, y)
\end{align*}
and, the recursive one, say
\begin{align*}
\partial R(\ctxlock{L}, a_0, b_0, r_0, a_1, b_1, r_1) : \OTO\left(\lambda a_2. \lambda b_2. (\proj_1 \rget{R^*}(a_0, a_1, a_2)(b_0,b_1,b_2))(r_0,r_1)\right)
\end{align*}
And let's also give a name to the first component of $\univ^*$:
\begin{align*}
\Id &: \prd{A : \univ} \rform{L}\left(\varkey{L}{0}A \to \varkey{L}{1}A \to \univ \right)
\end{align*}
so that for an ordinary term $a : A$,
\begin{align*}
a^* : \rform{L} \Id_A(\ctxlock{L}, \varkey{L}{0}a, \varkey{L}{1}a)
\end{align*}

Now the actual definitions:  (using the pattern-matching notation)
\begin{align*}
\Id_\univ(\ctxlock{L},A,B) &:\defeq \sm{R : A \to B \to \univ} \OTO(R) \\
\coe_\univ(\ctxlock{L}) &: \univ \to \univ \\
\coe_\univ(\ctxlock{L}) &:\defeq \id_\univ \\
\coh_\univ(\ctxlock{L}) &: \prd{A : \univ} \sm{R : A \to A \to \univ} \OTO(R) \\
\coh_\univ(\ctxlock{L}, A) &:\defeq (\rget{\Id_A}, \coe_A, \dots) \\
%\partial_\univ(\ctxlock{L},\ctxlock{K}, A_0, B_0, r_0, A_1, B_1, r_1) &:
\end{align*}
Now let's think about the recursive field. We at least need
\begin{align*}
\partial\coe_\univ(\ctxlock{L},\ctxlock{K}, A_0, B_0, r_0, A_1, B_1, r_1, a_2, b_2) &: ?
\end{align*}
where
\begin{align*}
A_0, B_0, A_1, B_1 &: \univ \\
r_0 &: \Id_\univ(A_0, B_0) \\
r_1 &: \Id_\univ(A_1, B_1) \\
a_2 &: \Id_\univ(A_0, A_1) \\
b_2 &: \Id_\univ(B_0, B_1)
\end{align*}


\begin{align*}
\Id_{\prd{x:A}B(x)}(\ctxlock{L}) &: \prd{x:\varkey{L}{0}A} \varkey{L}{0} B(x) \to \prd{x:\varkey{L}{1}A} \varkey{L}{1} B(x) \to \univ \\
\Id_{\prd{x:A}B(x)}(\ctxlock{L}, f_0, f_1) &:\defeq \prd{p : \prd{i:\Tiny} \varkey{L}{i} A} \Id_{B?}(\ctxlock{L}, f_0(p(0)), f_1(p(1))) \\
\coe_{\prd{x:A}B(x)}(\ctxlock{L}) &: \prd{x:\varkey{L}{0}A} \varkey{L}{0} B(x) \to \prd{x:\varkey{L}{1}A} \varkey{L}{1} B(x) \\
\coe_{\prd{x:A}B(x)}(\ctxlock{L},f_0,a_1) &:\defeq \coe_{B?}(f_0(\coe_A^{-1}(a_1))) \\
\coh_{\prd{x:A}B(x)}(\ctxlock{L}) &: \prd{f : \prd{x:\varkey{L}{0}A} \varkey{L}{0} B(x)} \Id_{\prd{x:A}B(x)}(\ctxlock{L}, f, \coe_{\prd{x:A}B(x)}(\ctxlock{L}, f)) \\
\coh_{\prd{x:A}B(x)}(\ctxlock{L}, f, p) &:\defeq ? \\
(\lambda x. b)^*(\ctxlock{L}) &: \prd{p : \prd{i:\Tiny} \varkey{L}{i} A} \Id_{B?}(\ctxlock{L}, (\varkey{L}{0}b)[p(0)/x], (\varkey{L}{1}b)[p(1)/x]) \\
(\lambda x. b)^*(\ctxlock{L},p) &:\defeq \relim{i.((\varkey{L}{i}b)[p(i)/x])^*} \\
(f(a))^*(\ctxlock{L}) &:\defeq f^*(\ctxlock{L},\lambda i. \varkey{L}{i} a)
\end{align*}


\begin{align*}
(\code(\Sigma_A B) : \univ)^*(\ctxlock{L}) &:\defeq ? \\
\end{align*}

OLD: This relies on the definition of $(A \to B)^*$ being pointwise relatedness, so that $\rget{R^*}$ has type
\begin{align*}
\rget{R^*} &: \prd{a_0 : \varkey{L}{0}A}{a_1 : \varkey{L}{1}A}{a_2 : \rget{A^*}(a_0,a_1)}{b_0 : \varkey{L}{0}B}{b_1 : \varkey{L}{1}B}{b_2 : \rget{B^*}(b_0,b_1)}  \\
&\qquad (\univ^*)((\varkey{L}{0} R)(a_0,b_0), (\varkey{L}{1} R)(a_1,b_1))
\end{align*}
and we have also already chosen
\begin{align*}
(\univ^*)((\varkey{L}{0} R)(a_0,b_0), (\varkey{L}{1} R)(a_1,b_1)) :\defeq
\sm{S : (\varkey{L}{0} R)(a_0,b_0) \to (\varkey{L}{1} R)(a_1,b_1) \to \univ} \dots
\end{align*}
and so we have to project out that first part so that we can evaluate it at $(r_0,r_1)$.

Actually now $\rget{R^*}$ has type
\begin{align*}
\rget{R^*} &: \prd{a : \prd{i:\Tiny} \varkey{L}{i} A}{b : \prd{i:\Tiny} \varkey{L}{i} B}  \\
&\qquad \proj_1 \Id_{\univ}((\varkey{L}{0} R)(a(0),b(0)), (\varkey{L}{1} R)(a(1),b(1)))
\end{align*}

\mvrnote{Well, now I'm stuck again. The only idea I have left is to build in endpoints into the context $\ctxlock{L}$ somehow, maybe following the altenkirch/kamposi idea. (and change the type rules).}

% \mvrnote{I had to change the definition of $\Id_{\prd{x:A}B(x)}(\ctxlock{L}, f_0, f_1) $ because I was getting stuck when defining $(\lambda x. b)^*$. The old way, where you use a relation between $a0$ and $a1$, there does not appear to be any way to construct the $\Id$ in $B$. There is nothing you can substitute for $x$ in $b$, because you only have the endpoints}


%\subsection{Directed}
%It might be easier to try a directed thing first.

%Unfolding definitions it has type
%\begin{align*}
%\coh^0 : \prd{f_0 : \varkey{L}{0}A \to \varkey{L}{0}B} \prd{x_0 : \varkey{L}{0}A}{x_1 : \varkey{L}{1}A}{r : \rget{(R_A)}(x_0, x_1)} \rget{(R_B)}(f_0(x_0), \rget{(\coe^0_B)}(f_0(\rget{(\coe^1_A)}(x_1))))
%\end{align*}
%\begin{align*}
%\coh^0(f_0,x_0,x_1,r) :\defeq ?? \rget{(\coh^0_B)}(f_0(\rget{(\coe^1_A)}(x_1)))
%\end{align*}
%Suppose we have $A : \univ$ and $B : A \to \univ$. (Just letting $x : A \yields B : \univ$ as a term will confuse me).
%\begin{align*}
%R &: \left(\prd{x : \varkey{L}{0}A}(\varkey{L}{0}B)(x)\right)\to \left(\prd{x : \varkey{L}{1}A}(\varkey{L}{1}B)(x)\right) \to \univ \\
%\coe^0 &: \left(\prd{x : \varkey{L}{0}A}(\varkey{L}{0}B)(x)\right) \to \left(\prd{x : \varkey{L}{1}A}(\varkey{L}{1}B)(x)\right) \\
%\coh^0 &: \prd{f : \prd{x : \varkey{L}{0}A}(\varkey{L}{0}B)(x)} f \sim \coe^0 f \\
%\coe^1 &: \left(\prd{x : \varkey{L}{1}A}(\varkey{L}{1}B)(x)\right) \to \left(\prd{x : \varkey{L}{0}A}(\varkey{L}{0}B)(x)\right) \\
%\coh^1 &: \prd{g : \prd{x : \varkey{L}{1}A}(\varkey{L}{1}B)(x)} \coe^1 g \sim g
%\end{align*}

%Then define $\Idsym_A(a,a') :\defeq \relim{\_.A^{*T}}(a,a')$ and $\refl{a} :\defeq \relim{\_.a^{*t}}$. Their stuck $\mathsf{R} : \Gamma \to \Gamma^=$ are admissible for us: it is just the transpose of weakening, which corresponds to ignoring the new variable in $\relim{i.a}$.

%\section{Extension Types?}
%\newcommand{\syn}{\mathsf{syn}}
%\newcommand{\Op}{\fullmoon}
%In Jon's Synthetic Tait Computability stuff, the $\syn$ proposition is tiny. The extension types also frequently use $\syn$ as the proposition where the term is fixed. Is this a coincidence? Can we make $\Op - :\defeq (\syn \to -)$ `compute' the same way $\Idsym$-types are supposed to commute?
%
%Suppose we do something similar to the above and have maps
%\begin{align*}
%(-)^{\Op T} &: \prd{A:\univ} \rform{L}\left(\sm{R : \univ} (\syn \to A \equiv R)\right) \\
%(-)^{\Op t} &: \prd{A:\univ} A \to \rform{L}\left(\proj_1 \rget{(A^{\Op T})}\right)
%\end{align*}
%where $\relim{\_.\proj_1 A^{\Op T}} : \univ$ is supposed to be what $A$ reduces to when $\syn$ holds. Again this can be given as one map
%\begin{align*}
%(-)^{\Op} &: \prd{A:\univ} A \to \rform{L}\left(\proj_1 \rget{\univ^{\Op}(A)}\right)
%\end{align*}
%if we define $\univ^{\Op}(A) :\defeq \sm{R : \univ} (\syn \to A \equiv R)$.
%
%\mvrnote{Is this going anywhere?}

%Type former for extension types might have shape
%\begin{align*}
%Ext : \prd{A : \syn \to \univ} \prd{s : \syn} A(s) \to \univ
%\end{align*}
%so $Ext(A)(a)$ is the type of terms that are exactly $a$ when $\syn$ holds.
%
%But that type rearranges to
%\begin{align*}
%\prd{A : \syn \to \univ} \prd{s : \syn} A(s) \to \univ
%&\equiv \left(\syn \to \sm{A : \univ} A\right) \to \univ \\
%&\equiv \left(\sm{A : \univ} A\right) \to \rformu \univ \\
%&\equiv \prd{A : \univ} (A \to \rformu \univ)
%\end{align*}
%This is equivalent to $\prd{A : \univ} \rformu ((\syn \to A) \to \univ)$ if that helps.

%Is this now suitable as a destructor for the universe? Just using $\prd{A : \univ} (\syn \to A) \to \univ$ is another candidate, but maybe it is important that $A$ is also restricted to $\syn$?

%\section{No Labels?}
%Can we somehow fold the $i: \Tiny$ variable into the lock label?
%
%\begin{mathpar}
%\inferrule*[left=ctx-lock]{\Gamma \ctx}{\Gamma, \ctxlocke{i} \ctx} \\
%\inferrule*[left=counit,fraction={-{\,-\,}-}]{\Gamma, \ctxlocke{i}, \Gamma' \yields t : \Tiny \and \Gamma \yields a : A}{\Gamma, \ctxlocke{i}, \Gamma' \yields \varkeye{i}{t} a : \varkeye{i}{t} A} \and
%\inferrule*[left=unit,fraction={-{\,-\,}-}]{\Gamma, i : \Tiny, \ctxlocke{i} \yields a : A}{\Gamma \yields a[\sublock{}{i}] : A[\sublock{}{i}]}
%\end{mathpar}
%\begin{mathpar}
%%\inferrule*[left=var-option-1]{n \defeq |{\mathsf{locks}(\Gamma')}| \\\\
%%\Gamma, x : A, \Gamma' \yields t_i : \Tiny \text{ for } i \in [1,n]
%%}{\Gamma, x : A, \Gamma' \yields \varkeye{t_n} \dots \varkeye{t_1} x : \varkeye{t_n} \dots \varkeye{t_1} A} \and
%\inferrule*[left=var]{
%\Gamma, x : A, \Gamma'_{>i_i} \yields t_i : \Tiny \text{ for } i_i \in \mathsf{locks}(\Gamma')
%}{\Gamma, x : A, \Gamma' \yields \varkeye{i_n}{t_n} \dots \varkeye{i_1}{t_1} x : \varkeye{i_n}{t_n} \dots \varkeye{i_1}{t_1} A} \and
%\end{mathpar}
%\begin{mathpar}
%\inferrule*[left=$\rformsym$-intro]{\Gamma, \ctxlocke{i} \yields A \type}{\Gamma \yields \rforme{i} A \type} \and
%\inferrule*[left=$\rformsym$-intro]{\Gamma, \ctxlocke{i} \yields a : A}{\Gamma \yields \rintroe{i} a : \rforme{i} A} \and
%\inferrule*[left=$\rformsym$-elim]{\Gamma, i : \Tiny \yields r : \rforme{i} A}{\Gamma \yields \relim{i.r} : A[\sublock{}{i}]} \\
%\relim{i.\rintroe{i} a} \defeq a[\sublock{}{i}] \and r \defeq \rintroe{i}{\relim{j. \varkeye{j}{i} r}} \text{ for } r : \rforme{i} A
%\end{mathpar}
%This is probably bad: $\rintroe{i} a$ is a term that looks like it binds a fresh variable $i$, but that is not actually a variable you can use anywhere other than in the subscript of $\key$.

%\section{Contraction}
%In some settings, like BCH cubes~\cite{bch:cubes}, there is a semicartesian monoidal product $\otimes$, and the interval $\mathbb{I}$ is tiny not for $\to$, but $\lolli$. Interestingly, the existing \rulen{$\rformu$-elim} rule would be derivable, because of first precomposing with the map $\Gamma \otimes I \to \Gamma \times I$. We also do not need to worry about the unit, because it is only ever used with a context literally of the form $(\Gamma \otimes i : \Tiny), \ctxlock{L}$.
%
%And so the only place an affineness restriction can come into play is in the counit/variable rule, where we build in a term of $\Tiny$.
%\mvrnote{come back to this?}

%There are a couple of alternative ideas for how variables could work, but each has implications for the admissible rules.
%\begin{itemize}
%\item \textbf{Keep Some Context.}
%
%
%\item \textbf{Keep Full Context.} A more powerful option would be to keep the same context for each $t_i$.
%\begin{mathpar}
%\inferrule*[left=var?]{
%\Gamma, x : A, \Gamma' \yields t_i : \Tiny \text{ for } \lockn{L}_i \in \mathsf{locks}(\Gamma')
%}{\Gamma, x : A, \Gamma' \yields \varkeye{\lockn{L}_n}{t_n} \dots \varkeye{\lockn{L}_1}{t_1} x : \admkeye{\lockn{L}_n}{t_n} \dots \admkeye{\lockn{L}_1}{t_1} A} \and
%\end{mathpar}
%This is building in some kind of contraction for $\Tiny$. The downside is that calculating $\admkey{L}{t} a$ is weirder: we would need to remember the $\ctxlock{K}$ that we go under in the term $a$, and then adjust $\admkey{L}{t}$ so that $t$ is still a valid term. With this variable rule, we define:
%\begin{align*}
%\admkeye{\lockn{L}}{t}  \left(\varkeye{\lockn{K}_n}{s_n} \dots \varkeye{\lockn{K}_{i+1}}{s_{i+1}} \varkeye{\lockn{K}_i}{s_i} \dots \varkeye{\lockn{K}_1}{s_1} x\right) &:\defeq \varkeye{\lockn{K}_n}{s_n} \dots \varkeye{\lockn{K}_{i+1}}{s_{i+1}} \varkeye{\lockn{L}}{t'}  \varkeye{\lockn{K}_i}{\admkeye{\lockn{L}}{t'} s_i} \dots \varkeye{\lockn{K}_1}{\admkeye{\lockn{L}}{t'} s_1} x \\
%& \quad \text{where } t' :\defeq \admkeye{\lockn{K}_n}{s_n} \dots \admkeye{\lockn{K}_{i+1}}{s_{i+1}} t
%\end{align*}
%and then the map $\rformu A \to \rformu \rformu A$ is definable. Maybe it makes sense to order the keys the other way around in this style.
%
%So let's try that:
%\begin{mathpar}
%\inferrule*[left=var?]{
%\Gamma, x : A, \Gamma' \yields t_i : \Tiny \text{ for } \lockn{L}_i \in \mathsf{locks}(\Gamma')
%}{\Gamma, x : A, \Gamma' \yields \varkeye{\lockn{L}_1}{t_1} \dots \varkeye{\lockn{L}_n}{t_n} x : \admkeye{\lockn{L}_1}{t_1} \dots \admkeye{\lockn{L}_n}{t_n} A} \and
%\end{mathpar}
%and
%\begin{align*}
%\admkeye{\lockn{L}}{t} \left(\varkeye{\lockn{K}_1}{s_1} \dots \varkeye{\lockn{K}_i}{s_i}\varkeye{\lockn{K}_{i+1}}{s_{i+1}} \dots \varkeye{\lockn{K}_n}{s_n} x\right) &:\defeq \varkeye{\lockn{K}_1}{\admkeye{\lockn{L}}{t'} s_1} \dots \varkeye{\lockn{K}_i}{\admkeye{\lockn{L}}{t'} s_i} \varkeye{\lockn{L}}{t'} \varkeye{\lockn{K}_{i+1}}{s_{i+1}} \dots \varkeye{\lockn{K}_n}{s_n} a \\
%& \quad \text{where } t' :\defeq \admkeye{\lockn{K}_{i+1}}{s_{i+1}} \dots \admkeye{\lockn{K}_n}{s_n} t
%\end{align*}
%And the lock
%\begin{align*}
%(\varkey{L}{t} \varkeye{\lockn{K}_n}{s_n} \dots \varkeye{\lockn{K}_1}{s_1} x)[\sublock{L}{i}] &:\defeq (\varkeye{\lockn{K}_n}{s_n} \dots \varkeye{\lockn{K}_1}{s_1} x)[t[\sublock{L}{i}]/i] \\
%(\varkey{L'}{t'} \varkeye{\lockn{K}_n}{s_n} \dots \varkeye{\lockn{K}_1}{s_1} x)[\sublock{L}{i}] &:\defeq \admkey{L'}{t'[\sublock{L}{i}]}(\varkeye{\lockn{K}_n}{s_n} \dots \varkeye{\lockn{K}_1}{s_1} x)[\sublock{L}{i}] \\
%x[\sublock{L}{i}] &:\defeq x
%%(\admkey{L}{t} c) [a/x] &:\defeq \admkey{L}{t[a/x]} c[a/x] \\
%%(\varkey{L}{t} c)[\sublock{L}{i}] &:\defeq c[t[\sublock{L}{i}]/i] %\\
%%(\admkey{K}{t} c)[\sublock{L}{i}] &:\defeq \admkey{K}{t[\sublock{L}{i}]} c[\sublock{L}{i}] &&\lockn{L} \not\defeq \lockn{K}
%\end{align*}
%
%\item \textbf{Fully General Counit.} If you build a substitution for $i : \Tiny$ into
%\begin{mathpar}
%\inferrule*[left=counit?,fraction={-{\,-\,}-}]{\Gamma,\Gamma' \yields a : A}{\Gamma, \ctxlock{L}, i : \Tiny, \admkey{L}{t}\Gamma' \yields \admkey{L}{t} a : \admkey{L}{i} A}
%\end{mathpar}
%then the fully general counit should be
%\begin{mathpar}
%\inferrule*[left=counit?,fraction={-{\,-\,}-}]{\Gamma,\Gamma' \yields a : A \and \Gamma, \ctxlock{L}, \admkey{L}{t}\Gamma' \yields t : \Tiny}{\Gamma, \ctxlock{L}, \admkey{L}{t}\Gamma' \yields \admkey{L}{t} a : \admkey{L}{t} A}
%\end{mathpar}
%which looks a bit psycho, with $t$ appearing in its own context.
%
%What if instead, we use some kind of context clearing operation.
%\begin{mathpar}
%\inferrule*[left=counit?,fraction={-{\,-\,}-}]{\Gamma,\Gamma' \yields a : A \and \Gamma, \ctxlock{L}, \Gamma'\setminus \Gamma \yields t : \Tiny}{\Gamma, \ctxlock{L}, \admkey{L}{t}\Gamma' \yields \admkey{L}{t} a : \admkey{L}{t} A}
%\end{mathpar}
%
%The variable rule should match this: for a single lock,
%\begin{mathpar}
%\inferrule*[left=var?,fraction={-{\,-\,}-}]{\Gamma_1,x : A,\Gamma_2, \ctxlock{L}, \admkey{L}{t}\Gamma' \yields t : \Tiny}{\Gamma_1,x : A,\Gamma_2, \ctxlock{L}, \admkey{L}{t}\Gamma' \yields \varkey{L}{t} x : \admkey{L}{t} A}
%\end{mathpar}
%and there would be some complicated n-ary version. This would also solve the contraction problem, but the form of the conclusion doesn't look stable under substitution absent some crazy trick.
%\end{itemize}
%
%
%\section{Pushouts}
%Because $(\Tiny \to -)$ is now a left adjoint, it should preserve e.g. pushouts. Let $(f,g) : A \leftarrow S \to B$ and consider the pushout $A +_S B$. First, supposing the inputs are closed, Prop~\ref{prop:closed-adj},
%\begin{align*}
%&\rform{L} (\Tiny \to A +_S B) \to C)\\
%&\equiv (A +_S B \to \rform{L} C) \\
%&\equiv \sm{h : A \to \rform{L} C}{k : B \to \rform{L} C} \prd{s : S} h(f(s)) = k(g(s)) \\
%&\equiv \sm{h : \rform{L} (\Tiny \to A) \to C}{k : \rform{L} (\Tiny \to B) \to C} \prd{s : S} \rintro{L}{\rget{h}(\lambda j.(\varkey{L}{j} f)(\varkey{L}{j} s))} =\rintro{L}{\rget{k}(\lambda j.(\varkey{L}{j} g)(\varkey{L}{j} s))} \\
%&\equiv \sm{h : \rform{L} (\Tiny \to A) \to C}{k : \rform{L} (\Tiny \to B) \to C} \prd{s : S} \rform{L}{\left(\rget{h}(\lambda j.(\varkey{L}{j} f)(\varkey{L}{j} s)) = \rget{k}(\lambda j.(\varkey{L}{j} g)(\varkey{L}{j} s))\right)} \\
%&\equiv \sm{h : \rform{L} (\Tiny \to A) \to C}{k : \rform{L} (\Tiny \to B) \to C} \rform{L}{\left(\prd{p : \Tiny \to S} \rget{h}(\lambda j.(\varkey{L}{j} f)(p(j))) = \rget{k}(\lambda j.(\varkey{L}{j} g)(p(j)))\right)} ? \\
%&\equiv \rform{L} \left( \sm{h :(\Tiny \to A) \to C}{k : (\Tiny \to B) \to C} \prd{p : \Tiny \to S} h(\lambda j.(\varkey{L}{j} f)(p(j))) = k(\lambda j.(\varkey{L}{j} g)(p(j)))\right) \\
%&\equiv \rform{L} \left((\Tiny \to A) +_{\Tiny \to S} (\Tiny \to B) \to C\right)
%\end{align*}
%which is what we hoped.
%\begin{align*}
%&\rform{L} ((\prd{t:\Tiny} \varkey{L}{t} (A +_S B)) \to \rget{C})\\
%&\equiv (A +_S B \to \rform{L} \rget{C}) \\
%&\equiv \sm{h : A \to \rform{L} \rget{C}}{k : B \to \rform{L} \rget{C}} \prd{s : S} h(f(s)) = k(g(s)) \\
%&\equiv \sm{h : \rform{L} ((\prd{t:\Tiny} \varkey{L}{t} A) \to \rget{C})
%}{k : \rform{L} ((\prd{t:\Tiny} \varkey{L}{t} B) \to \rget{C})
%} \prd{s : S} h(f(s)) = k(g(s)) \\
%\end{align*}
\fi

\section{The Bug}

The variable rule is not closed under substitution, if the superscripts on the keys get complicated:
\begin{alignat*}{2}
x : A, \ctxlock{L}, B : \univ, \ctxlock{K}, f : \varkey{K}{0} B \to \Tiny, b &:  \varkey{K}{0} B, t : \Tiny &&\yields \varkey{K}{t} \varkey{L}{t} x : A \\
x : A, \ctxlock{L}, B : \univ, \ctxlock{K}, f : \varkey{K}{0} B \to \Tiny, b &:  \varkey{K}{0} B &&\yields \varkey{K}{f(b)} \varkey{L}{f(b)} x : A
\end{alignat*}
but the second term is not well formed, because the $f$ and $b$ get cleared after the first key and so can't be used in the second. So we either need some kind of affineness restriction, or we need to go `fully cartesian' instead of this half-way option.

Here's an idea: We build in as much cartesian-ness as possible,
\begin{mathpar}
\inferrule*[left=var]{
\Gamma, x : A, \Gamma' \yields t_i : \Tiny \text{ for } \lockn{L}_i \in \mathsf{locks}(\Gamma')
}{\Gamma, x : A, \Gamma' \yields \varkeye{\lockn{L}_n}{t_n} \dots \varkeye{\lockn{L}_1}{t_1} x : \admkeye{\lockn{L}_n}{t_n} \dots \admkeye{\lockn{L}_1}{t_1} A}
\end{mathpar}
\begin{mathpar}
\inferrule*[left=counit,fraction={-{\,-\,}-}]{\Gamma, \Gamma'' \yields a : A \and \Gamma, \ctxlock{L}, \Gamma' \yields t : \Tiny}{\Gamma, \ctxlock{L}, \Gamma', \admkey{L}{t}\Gamma'' \yields \admkey{L}{t} a : \admkey{L}{t} A}
\end{mathpar}

This is annoying, because when $\admkey{L}{t}$ reaches a variable, it has to recur into all the superscripts of the existing keys, rather than stopping as the outermost key.

Maybe we can use some sugar to make it manageable:
\begin{mathpar}
\inferrule*[left=counit,fraction={-{\,-\,}-}]{\Gamma, \ctxlock{L}^{t}, \Gamma' \yields a : A \and \Gamma, \ctxlock{L}, \Gamma' \yields t : \Tiny}{\Gamma, \ctxlock{L}, \admkey{L}{t}\Gamma' \yields \admkey{L}{t} a : \admkey{L}{t} A}
\end{mathpar}
\begin{mathpar}
\inferrule*[left=var]{~ \ctxlock{L}^\varnothing \notin \Gamma'}{\Gamma, x : A, \Gamma' \yields x : A}
\end{mathpar}
and then we try to build the former into the latter. But then how do we handle a lock being opened more than once?

\begin{mathpar}
\inferrule*[left=counit?,fraction={-{\,-\,}-}]{\Gamma \yields a : A \and \Gamma, \ctxlock{L}, \Gamma' \yields t : \Tiny \and \lock \notin \Gamma'}{\Gamma, \ctxlock{L}, \Gamma' \yields \admkey{L}{t} a : \admkey{L}{t} A}
\end{mathpar}
but we will need a generalised version of this, for going under binders in $a : A$. The actual counit rule is then
\begin{mathpar}
\inferrule*[left=counit,fraction={-{\,-\,}-}]{\Gamma, \Gamma'' \yields a : A \and \Gamma, \ctxlock{L}, \Gamma' \yields t : \Tiny}{\Gamma, \ctxlock{L}, \Gamma', \admkey{L}{t}\Gamma'' \yields \admkey{L}{t} a : \admkey{L}{t} A}
\end{mathpar}


Notation idea: write keys like
\begin{align*}
  \key(t/\lockn{L}, s/\lockn{K}) x
\end{align*}
and write the unit substitution as
\begin{align*}
  \judge[i/\lockn{L}]
\end{align*}
so you get
\begin{align*}
  \left(\key(t/\lockn{L}, s/\lockn{K}) i\right)[i/\lockn{L}]
  &\defeq   i[t/i] \defeq t
\end{align*}
or in that case maybe it should be postfix
\begin{align*}
  \left(i \key[t/\lockn{L}, s/\lockn{K}] \right)[i/\lockn{L}]
  \defeq i [t/i]
\end{align*}

%\section{Combined With Cohesion??}
%Heaven help us

\fi

\printbibliography

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: