\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate]{lipics-v2021}
\usepackage{mathabx}
\usepackage{stackengine} % for \ab and similar

%This is a template for producing LIPIcs articles.
%See lipics-v2021-authors-guidelines.pdf for further information.
%for A4 paper format use option "a4paper", for US-letter use option "letterpaper"
%for british hyphenation rules use option "UKenglish", for american hyphenation rules use option "USenglish"
%for section-numbered lemmas etc., use "numberwithinsect"
%for enabling cleveref support, use "cleveref"
%for enabling autoref support, use "autoref"
%for anonymousing the authors (e.g. for double-blind review), add "anonymous"
%for enabling thm-restate support, use "thm-restate"
%for enabling a two-column layout for the author/affilation part (only applicable for > 6 authors), use "authorcolumns"
%for producing a PDF according the PDF/A standard, add "pdfa"

%\pdfoutput=1 %uncomment to ensure pdflatex processing (mandatatory e.g. to submit to arXiv)
%\hideLIPIcs  %uncomment to remove references to LIPIcs series (logo, DOI, ...), e.g. when preparing a pre-final version to be uploaded to arXiv or another public repository

%\graphicspath{{./graphics/}}%helpful if your graphic files are in another directory

\bibliographystyle{plainurl}% the mandatory bibstyle

\title{Internal strict propositions using point-free equations}

%\titlerunning{Dummy short title}

% \author{Jane {Open Access}}{Dummy University Computing Laboratory, [optional: Address], Country \and My second affiliation, Country \and \url{http://www.myhomepage.edu} }{johnqpublic@dummyuni.org}{https://orcid.org/0000-0002-1825-0097}{(Optional) author-specific funding acknowledgements}

\author{István Donkó}{Eötvös Loránd University, Budapest, Hungary}{isti115@inf.elte.hu}{}{Supported by the ÚNKP-21-3 New National Excellence Program of the Ministry for Innovation and Technology from the source of the National Research, Development and Innovation Fund.}
\author{Ambrus Kaposi}{Eötvös Loránd University, Budapest, Hungary}{akaposi@inf.elte.hu}{http://orcid.org/0000-0001-9897-8936}{Supported by the Bolyai Fellowship of the Hungarian Academy of Sciences, Project no. BO/00659/19/3, and by the ``Application Domain Specific Highly Reliable IT Solutions'' project which has been implemented with the support provided from the National Research, Development and Innovation Fund of Hungary, financed under the Thematic Excellence Programme TKP2020-NKA-06 (National Challenges Subprogramme) funding scheme}

\authorrunning{I. Donkó and A. Kaposi}

\Copyright{István Donkó and Ambrus Kaposi}

\ccsdesc[500]{Theory of computation~Logic~Type theory}

\keywords{Martin-Löf's type theory, intensional type theory, function extensionality, setoid model, homotopy type theory}

%\category{} %optional, e.g. invited paper

\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
%\relatedversiondetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93]{Classification (e.g. Full Version, Extended Version, Previous Version}{URL to related version} %linktext and cite are optional

%\supplement{}%optional, e.g. related research data, source code, ... hosted on a repository like zenodo, figshare, GitHub, ...
\supplementdetails[cite=formalis, subcategory={Formalisation}]{Software}{https://bitbucket.org/akaposi/prop} %linktext, cite, and subcategory are optional

%\funding{(Optional) general funding statement \dots}%optional, to capture a funding statement, which applies to all authors. Please enter author specific funding statements as fifth argument of the \author macro.

\acknowledgements{Thanks to Christian Sattler for discussions on the topics of this paper. Many thanks to the anonymous reviewers for their comments and suggestions.}%optional

%\nolinenumbers %uncomment to disable line numbering



%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\EventEditors{Henning Basold, Jesper Cockx, and Silvia Ghilezan}
\EventNoEds{3}
\EventLongTitle{27th International Conference on Types for Proofs and Programs (TYPES 2021)}
\EventShortTitle{TYPES 2021}
\EventAcronym{TYPES}
\EventYear{2021}
\EventDate{June 14--18, 2021}
\EventLocation{Leiden, The Netherlands (Virtual Conference)}
\EventLogo{}
\SeriesVolume{239}
\ArticleNo{8}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newtheorem{construction}[theorem]{Construction}

\input{abbrevs.tex}

\begin{document}

\maketitle

\begin{abstract}
The setoid model of Martin-Löf's type theory bootstraps extensional
features of type theory from intensional type theory equipped with a
universe of definitionally proof irrelevant (strict)
propositions. Extensional features include a Prop-valued identity type
with a strong transport rule and function extensionality. We show that
a setoid model supporting these features can be defined in intensional
type theory without any of these features. The key component is a
point-free notion of propositions. Our construction suggests that
strict algebraic structures can be defined along the same lines in
intensional type theory.
\end{abstract}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Introduction}

The setoid model of type theory pioneered by Hofmann
\cite{DBLP:books/daglib/0088162} supports the following extensional
features that are missing from intensional type theory: function
extensionality, propositional extensionality (univalence for
propositions \cite{setoid}) and quotient inductive-inductive types
\cite{kaposi-qiit-setoid}. If the setoid model is defined in an
intensional metatheory and all equations of the model (such as the
$\beta$ rule) hold definitionally, then it constitutes a \emph{model
construction} (also called syntactic translation): any model of
intensional type theory can be turned into its ``setoidified'' variant
which supports the extensional features, thus bootstrapping the
extensional features from intensional type theory. Hofmann's original
model only justified some of the equations definitionally. Altenkirch
showed that if the metatheory supports a sort $\TyP$ of definitionally
proof irrelevant propositions in addition to the sort $\Ty$ of types,
then there is a version of the setoid model where all equations are
definitional \cite{DBLP:conf/lics/Altenkirch99}. After he presented
this model construction at the Symposium on Logic in Computer Science
in 1999 \cite{DBLP:conf/lics/Altenkirch99}, Per Martin-Löf asked
whether it is possible to remove the extra requirement of $\TyP$. As
far as we know, the question is still open.

In this setoid model a closed type is a setoid: a type together with an
equivalence relation; a term is a function between the types which
respects the relations. If the equivalence relation is proof relevant
($\Ty$-valued), then terms have to additionally include components
about respecting the reflexivity, symmetry and transitivity proofs,
then when proving equalities of terms (such as the $\beta$ law), one
has to show that the corresponding new components are equal, which
forces the introduction of new components, and so on. This problem is
usually referred to as coherence problem, see \cite[Section
  5.3]{DBLP:books/daglib/0088162} for a discussion in the context of
the setoid model, or \cite{DBLP:conf/lics/KrausR20} for a recent
exposition of the general phenomenon. Altenkirch's solution
\cite{DBLP:conf/lics/Altenkirch99} was to make the relation
$\TyP$-valued instead of $\Ty$-valued: in this case, terms
automatically respect reflexivity proofs as there is only one proof of
reflexivity, up to definitional equality. We could avoid requiring
$\TyP$ by using the internally definable universe of homotopy
propositions $\hProp$ \cite{HoTTbook}. If the relation is
$\hProp$-valued, terms respect reflexivity proofs up to the internal
identity type. However to show that the relation for $\Pi$ types is in
$\hProp$, we need that $\hProp$ is closed under $\Pi$. To prove this,
we need function extensionality, which defeats the purpose of the
model bootstrapping function extensionality.

In this paper we show that in intensional type theory there is an
alternative notion of proposition that is closed under $\Pi$. A type
$A$ is an $\hProp$ if any two elements of $A$ are equal. We can also
express this equation in a point-free way: the two functions ``first''
and ``second'' both having type $A\ra A\ra A$ are equal. We call this
property $\isPfProp$ for point-free propositions.
\[
\isHProp\,A \equiv (a\,a' : A) \ra \Id_A\,a\,a' \hspace{6em} \isPfProp\,A \equiv \Id_{(A\ra A\ra A)}\,(\lambda a\,a'.a)\,(\lambda a\,a'.a')
\]
In the presence of function extensionality, $\isHProp\,A$ and
$\isPfProp\,A$ are equivalent. However, in intensional type theory
without function extensionality, the latter is stronger. $\isPfProp$
classifies definitionally proof irrelevant types in the empty context:
from canonicity it follows that if $\isPfProp\,A$ for a closed type
$A$, then all elements of $A$ are definitionally equal. For a type
family $A : D\ra\Type$ over a closed type we use a dependent variant
of $\isPfProp$:
\[
\isPfPropd\,A \equiv \Id_{((d:D)\ra A\,d\ra A\,d\ra A\,d)}\,(\lambda d\,a\,a'.a)\,(\lambda d\,a\,a'.a')
\]
In intensional type theory, unlike $\hProp$, $\isPfPropd$ is closed
under $\Pi$ types. This essentially relies on the $\eta$ rule for
$\Pi$ types. Using $\eta$ for $\Sigma$ and $\top$, we can prove that
$\isPfPropd$ is closed under these type formers too. $\isPfProp$
only includes $\bot$ if it has a weak $\eta$ rule saying that any two
elements of $\bot$ are definitionally equal. This is usually not the
case in intensional type theory where $\bot$ is defined as an
inductive type.

With the help of point-free propositions, we give a partial positive
answer to Martin-Löf's question: in intensional type theory without a
sort of propositions, we define the setoid model with $\bot$, $\top$,
$\Pi$, $\Sigma$, types, a sort $\TyP$ closed under $\top$, $\Pi$,
$\Sigma$ and a $\TyP$-valued identity type with function
extensionality. Our answer is partial because $\bot$ is not in $\TyP$,
and the model does not support inductive types, or a universe of
propositions. We also define an external version of this model as a
model construction taking as input a model of intensional type theory,
and outputting a model with extensionality principles. This latter
construction only uses external point-free propositions which are the
same as subobjects in category theory, but we still haven't
encountered it in the literature.

Recently, there is a renewed interest in models of type theory with a
sort $\TyP$. Agda was extended with a universe of strict propositions
\cite{DBLP:journals/pacmpl/GilbertCST19}, this was used to formalise
fully featured variants of the setoid model
\cite{setoid,DBLP:conf/fossacs/AltenkirchBKSS21,kaposi-qiit-setoid},
strict presheaf models were built using $\TyP$
\cite{DBLP:conf/lics/Pedrot20}, and the metatheory of type theories
with $\TyP$ was studied
\cite{DBLP:journals/lmcs/AbelC20,DBLP:journals/corr/abs-2103-04287}.
One difference between $\TyP$ and $\pfProp$ is that (as every sort)
the former is static: it only includes types which are built into
it. The latter is dynamic: any type is included for which all elements
are definitionally equal. Another difference is that proof irrelevance
holds definitionally for assumed elements of $\TyP$, while we only
know proof irrelevance up to propositional equality for members of
$\pfProp$.

More generally, in intensional type theory, point-free equations can
be used to describe strict algebraic structures. One has to express
the algebraic equations in a point-free way. For example, in a strict
monoid with carrier $\mathsf{M}$ and binary operation
$\blank\otimes\blank$, associativity is expressed as $\Id_{\mathsf{M}\ra \mathsf{M}\ra
  \mathsf{M}\ra \mathsf{M}}\,\big(\lambda x\,y\,z.(x\otimes y)\otimes
z\big)\,\big(\lambda x\,y\,z.x\otimes (y\otimes z)\big)$. Natural
numbers with addition are not a strict monoid because addition is only
weakly associative. An example of a strict monoid is the function space $A\ra
A$ for any type $A$ with composition as the binary operation.

\subsection{Structure of the paper}

After describing related work, in Section \ref{sec:tt} we explain our
notation and the notion of model of type theory we use (category with
families). In Section \ref{sec:internal} we define point-free
propositions and show that they are closed under $\top$, $\Sigma$ and
$\Pi$. In Section \ref{sec:external}, we show that any model of type
theory can be equipped with a sort of strict propositions. This can be
seen as the external version of Section \ref{sec:internal}. We compare
the internal and external notions of propositions in Section
\ref{sec:relation}. Then we describe how point-free propositions can
be applied to construct the setoid model. As a warmup, we define the
model construction externally (Section \ref{sec:setoid}). Then we turn
to our main application of internal point-free propositions and define
the setoid model internally to a model of intensional type theory
(Section \ref{sec:setoid_internal}). In Section
\ref{sec:algebraic_structures} we give more examples of strict
algebraic structures. We conclude in Section \ref{sec:summary}.

Sections \ref{sec:internal} and \ref{sec:setoid_internal} were
formalised in Agda \cite{formalis}, and can be understood without much
intuition about categories with families.

\subsection{Related work}

Hofmann defined two versions of the setoid model in an intensional
metatheory \cite{DBLP:books/daglib/0088162}, one of them did not have
dependent types, the other justified some computation rules
(e.g. $\beta$ rules for $\Sigma$ types) only up to propositional
equality, and not definitionally. Altenkirch
\cite{DBLP:conf/lics/Altenkirch99} justified all the rules of type
theory but relied on a definitionally proof-irrelevant universe of
propositions. He sketched a normalisation proof for a type theory with
such a universe. Coquand \cite{coquand12setoid} defined a setoid model
in intensional type theory which justifies a weak function space:
there is no substitution rule for $\lambda$ and no $\eta$
rule. Palmgren \cite{2019arXiv190901414P} formalised a set-theoretic
interpretation of extensional type theory in an intensional
metatheory. He used setoids for encoding sets as well-founded trees
quotiented by bisimulation, hence it can also be seen as a setoid
model. Thus it is similar to our Construction
\ref{constr:setoid_internal} and it justifies more types including
inductive types and a universe. It is not clear whether one can obtain
a model construction analogous to Construction
\ref{constr:setoid_external} from his interpretation.

Strict propositions were introduced in Agda and Coq in a way that is
compatible with univalence
\cite{DBLP:journals/pacmpl/GilbertCST19}. Issues with rewriting-style
normalisation for a type theory with strict propositions, a strict
identity type and a strong transport were found by Abel and Coquand
\cite{DBLP:journals/lmcs/AbelC20}. Normalisation for type theory with
strict propositions but without such an identity type was proved by
Coquand \cite{DBLP:journals/corr/abs-2103-04287}.

The setoid model as a model construction was described in
\cite{setoid} together with an Agda formalisation using strict
propositions in Agda. This was extended with an inductive-recursive
universe of setoids in \cite{DBLP:conf/fossacs/AltenkirchBKSS21}.

In \cite{setoid}, a variant of the setoid model was described in which
transport has a definitional computation rule. In the accompanying
formalisation, a point-free equation was used to ensure this property:
instead of $(a:A)\ra\coe_A\,\refl\,a = a$, the equation $(\lambda
a.\coe_A\,\refl\,a)=(\lambda a.a)$ was used. In his brilliant paper
\cite{DBLP:conf/types/Hugunin20}, Hugunin shows that function
extensionality is not needed to define natural numbers (and inductive
types) from W-types in intensional type theory. He constructs a
predicate which selects the ``canonical'' elements in natural numbers
defined by W-types. His construction has a similar ``point-free''
flavour and also essentially relies on $\eta$ for function space.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Type theory}
\label{sec:tt}

Our metatheory is extensional type theory and we use notations similar
to Agda's. We write $\Type$ for the Russell universe (we don't write
levels explicitly, but we work in a predicative setting), we write
$\equiv$ for definitional equality, we write $(x:A)\ra B$ for function
space with $\lambda(x:A).t$ or $\lambda x.t$ for abstraction,
juxtaposition for application, $(x:A)\times B$ for $\Sigma$ types with
$a,b$ for pairing and $\pi_1\,\ab$, $\pi_2\,\ab$ for projections. We
use the lower case Simonyi naming convention, e.g.\ $\ab$ is a name
for a variable in $(x:A)\times B$. We use implicit arguments and
implicit quantifications which we sometimes specify explicitly in
subscripts. We write $\top$, $\tt$ for the unit type and its
constructor. Function space, dependent products and unit have $\eta$
laws. We write $\Id_A\,a\,a'$ or $a =_A a'$ or simply $a=a'$ for the
identity type, it has constructor $\refl : \Id_A\,a\,a$ and eliminator
$\J:\big(P:(a':A)\ra a=a'\ra\Type\big)\ra P\,a\,\refl\ra (e:a=a')\ra
P\,a'\,e$ with definitional computation rules. We write
$\transp:(P:A\ra\Type)\ra a=a'\ra P\,a\ra P\,a'$, $e\sqcdot e' :
a=a''$ for $e:a=a'$ and $e':a'=a''$, $\ap\,f\,e : f\,a=f\,a'$ for
$e:a=a'$, all defined via $\J$. The empty type is denoted $\bot$ with
eliminator $\elim_\bot$. We assume quotient inductive-inductive types
(QIITs), that is, we have syntaxes for type theories (see paragraph
after the next one).

In some places (e.g.\ in sections \ref{sec:internal} and \ref{sec:setoid_internal}), we
work internally to a model of intensional type theory, and use the
same notations as for our metatheory. In these cases we specify
precisely what features our model has and we only use those features,
for example we don't use equality reflection. In such cases we use the
phrase ``external'' to refer to the metatheory.

The notion of model of type theory we use is category with families
(CwF, \cite{DBLP:journals/corr/abs-1904-00827}). Using this
presentation, type theory is a generalised algebraic theory and the
syntax of a type theory is the initial algebra which is a QIIT. In
extensional type theory, it is enough to assume the existence of a
single QIIT to obtain syntaxes for all generalised algebraic theories
\cite{popl19}. We assume the existence of this QIIT (called the theory
of QIIT signatures in \cite{popl19}).

\begin{figure}
\begin{alignat*}{10}
  & \Con                && : \Set                                                                                    && \top             && : \Ty\,\Gamma \\
  & \Sub                && : \Con\ra\Con\ra\Set                                                                      && {\top[]}         && : \top[\gamma]\equiv\top \\
  & \blank\circ\blank   && : \Sub\,\Delta\,\Gamma\ra\Sub\,\Theta\,\Delta\ra\Sub\,\Theta\,\Gamma                      && \tt              && : \Tm\,\Gamma\,\top \\
  & \mathsf{ass}        && : (\gamma\circ\delta)\circ\theta \equiv \gamma\circ(\delta\circ\theta)                    && {\top\eta}       && : (t:\Tm\,\Gamma\,\top)\ra t \equiv\tt \\
  & \id                 && : \Sub\,\Gamma\,\Gamma                                                                    && \Sigma           && : (A:\Ty\,\Gamma)\ra\Ty\,(\Gamma\rhd A)\ra\Ty\,\Gamma \\
  & \mathsf{idl}        && : \id\circ\gamma \equiv \gamma                                                            && {\Sigma[]}       && : (\Sigma\,A\,B)[\gamma] \equiv \Sigma\,(A[\gamma])\,(B[\gamma\circ\p,\q]) \\
  & \mathsf{idr}        && : \gamma\circ\id \equiv \gamma                                                            && \blank,\blank    && : (a:\Tm\,\Gamma\,A)\ra\Tm\,\Gamma\,(B[\id,a])\ra \\
  & \blackdiamond       && : \Con                                                                                    &&                  && \hphantom{{}:{}} \Tm\,\Gamma\,(\Sigma\,A\,B) \\
  & \epsilon            && : \Sub\,\Gamma\,\blackdiamond                                                             && \pi_1            && : \Tm\,\Gamma\,(\Sigma\,A\,B)\ra\Tm\,\Gamma\,A \\
  & {\blackdiamond\eta} && : (\sigma:\Sub\,\Gamma\,\blackdiamond)\ra\sigma\equiv\epsilon                             && \pi_2            && : (\ab:\Tm\,\Gamma\,(\Sigma\,A\,B))\ra \\
  & \Ty                 && : \Con\ra\Set                                                                             &&                  && \hphantom{{}:{}}\Tm\,\Gamma\,(B[\id,\pi_1\,\ab]) \\
  & \blank[\blank]      && : \Ty\,\Gamma\ra\Sub\,\Delta\,\Gamma\ra\Ty\,\Delta                                        && {\Sigma\beta}_1  && : \pi_1\,(a,b) \equiv a \\
  & [{\circ}]           && : A[\gamma\circ\delta] \equiv A[\gamma][\delta]                                           && {\Sigma\beta}_1  && : \pi_2\,(a,b) \equiv b \\
  & [\id]               && : A[\id] \equiv A                                                                         && {\Sigma\eta}     && : (\pi_1\,\ab,\pi_2\,\ab) \equiv \ab \\
  & \Tm                 && : (\Gamma:\Con)\ra\Ty\,\Gamma\ra\Set                                                      && {{,}[]}          && : (a,b)[\gamma] \equiv (a[\gamma],b[\gamma]) \\
  & \blank[\blank]      && : \Tm\,\Gamma\,A\ra(\gamma:\Sub\,\Delta\,\Gamma)\ra                                       && \Pi              && : (A:\Ty\,\Gamma)\ra\Ty\,(\Gamma\rhd A)\ra\Ty\,\Gamma \\
  &                     && \hphantom{{}:{}}\Tm\,\Delta\,(A[\gamma])                                                  && {\Pi[]}          && : (\Pi\,A\,B)[\gamma] \equiv \Pi\,(A[\gamma])\,(B[\gamma\circ\p,\q]) \\
  & [{\circ}]           && : a[\gamma\circ\delta] \equiv a[\gamma][\delta]                                           && \lam             && : \Tm\,(\Gamma\rhd A)\,B\ra\Tm\,\Gamma\,(\Pi\,A\,B) \\
  & [\id]               && : a[\id] \equiv a                                                                         && \app             && : \Tm\,\Gamma\,(\Pi\,A\,B)\ra\Tm\,(\Gamma\rhd A)\,B \\
  & \blank\rhd\blank    && : (\Gamma:\Con)\ra\Ty\,\Gamma\ra\Con                                                      && {\Pi\beta}       && : \app\,(\lam\,t) \equiv t \\
  & \blank,\blank       && : (\gamma:\Sub\,\Delta\,\Gamma)\ra\Tm\,\Delta\,(A[\gamma])\ra  \hspace{2em}               && {\Pi\eta}        && : \lam\,(\app\,t) \equiv t \\
  &                     && \hphantom{{}:{}} \Sub\,\Delta\,(\Gamma\rhd A)                                             && {\lam[]}         && : (\lam\,t)[\gamma] \equiv \lam\,(t[\gamma\circ\p,\q]) \\
  & \p_A                && : \Sub\,(\Gamma\rhd A)\,\Gamma                                                            && \bot             && : \Ty\,\Gamma \\
  & \q_A                && : \Tm\,(\Gamma\rhd A)\,(A[\p])                                                            && \bot[]           && : \bot[\gamma] \equiv \bot \\
  & {{\rhd}\beta}_1     && : \p\circ(\gamma,a)\equiv\gamma                                                           && \elim_\bot       && : \Tm\,\Gamma\,\bot\ra\Tm\,\Gamma\,A \\
  & {{\rhd}\beta}_2     && : \q[\gamma,a]\equiv a                                                                    && \elim_\bot[]     && : (\elim_\bot\,t)[\gamma] \equiv \elim_\bot\,(t[\gamma]) \\
  & {{\rhd}\eta}        && : (\p\circ\gammaa,\q[\gammaa]) \equiv \gammaa                                             && \Id_{\blank}     && : (A:\Ty\,\Gamma)\ra\Tm\,\Gamma\,A\ra\Tm\,\Gamma\,A\ra \\
  &                     &&                                                                                           &&                  && \hphantom{{}:{}}\Ty\,\Gamma \\
  &                     &&                                                                                           && \Id[]            && : (\Id_A\,a\,a')[\gamma] \equiv \Id_{A[\gamma]}\,(a[\gamma])\,(a'[\gamma]) \\
  &                     &&                                                                                           && \refl            && : \Tm\,\Gamma\,(\Id_A\,a\,a) \\
  &                     &&                                                                                           && \refl[]          && : \refl[\gamma] \equiv \refl \\
  &                     &&                                                                                           && \J               && : (P:\Ty\,(\Gamma\rhd A\rhd\Id_{A[\p]}\,(a[\p])\,\q))\ra \\
  &                     &&                                                                                           &&                  && \hphantom{{}:{}} \Tm\,\Gamma\,(P[\id,a,\refl])\ra \\
  &                     &&                                                                                           &&                  && \hphantom{{}:{}} (e:\Tm\,\Gamma\,(\Id_A\,a\,a'))\ra \\
  &                     &&                                                                                           &&                  && \hphantom{{}:{}} \Tm\,\Gamma\,(P[\id,a',e]) \\
  &                     &&                                                                                           && \J\beta          && : \J\,P\,w\,\refl \equiv w \\
  &                     &&                                                                                           && \J[]             && : (\J\,P\,w\,e)[\gamma] \equiv \\
  &                     &&                                                                                           &&                  && \hphantom{{}:{}} \J\,(P[\gamma\circ\p\circ\p,\q[\p],\q])\,(w[\gamma])\,(e[\gamma])
\end{alignat*}
\caption{A model of type theory with $\top$, $\Sigma$, $\Pi$, $\bot$,
  $\Id$. The left column is the definition of CwF, the right column
  contains the rules for the type formers, one after the other, in the
  same order.}
\label{fig:mltt}
\end{figure}
\begin{figure}
\begin{alignat*}{10}
  & {,{\circ}} && : (\gamma,a)\circ\delta \equiv (\gamma\circ\delta,a[\delta])                       \\
  & {\pi_1[]} && : (\pi_1\,\ab)[\gamma] \equiv \pi_1\,(\ab[\gamma])                                   \\
  & {\pi_2[]} && : (\pi_2\,\ab)[\gamma] \equiv \pi_2\,(\ab[\gamma])                                   \\
  & \blank\times\blank && : \Ty\,\Gamma\ra\Ty\,\Gamma\ra\Ty\,\Gamma \\
  & A\times B && :\equiv \Sigma\,A\,(B[\p]) \\
  & {\app[]} && : (\app\,t)[\gamma\circ\p,\q] \equiv \app\,(t[\gamma])                                \\
  & \blank\oldapp\blank && : \Tm\,\Gamma\,(\Pi\,A\,B)\ra(a:\Tm\,\Gamma\,A)\ra\Tm\,\Gamma\,(B[\id,a])  \\
  & t \oldapp a && :\equiv (\app\,t)[\id,a] \\
  & {\oldapp}\beta && : \lam\,t \oldapp a \equiv t[\id,a] \\
  & {\oldapp}[] && : (t\oldapp a)[\gamma] \equiv t[\gamma] \oldapp a[\gamma] \\
  & \blank\Ra\blank && : \Ty\,\Gamma\ra\Ty\,\Gamma\ra\Ty\,\Gamma \\
  & A\Ra B && :\equiv \Pi\,A\,(B[\p])
\end{alignat*}
\caption{Provable equations and definable operations in a model of type theory with $\Sigma$, $\Pi$.}
\label{fig:abbrevs}
\end{figure}
\begin{figure}
\begin{alignat*}{10}
  & \TyP                && : \Con\ra\Set                                                                      \\
  & \blank[\blank]      && : \TyP\,\Gamma\ra\Sub\,\Delta\,\Gamma\ra\TyP\,\Delta                               \\
  & [{\circ}]           && : A[\gamma\circ\delta] \equiv A[\gamma][\delta]                                    \\
  & [\id]               && : A[\id] \equiv A                                                                  \\
  & {\uparrow}          && : \TyP\,\Gamma\ra\Ty\,\Gamma                                                       \\
  & {\uparrow}[]        && : ({\uparrow}A)[\gamma] \equiv {\uparrow}(A[\gamma]) \\
  & \irr                && : (u\,v : \Tm\,\Gamma\,({\uparrow} A))\ra u\equiv v                                \\
  & {\top\P}            && : \TyP\,\Gamma                                                                     \\
  & {\top\P[]}          && : {\top\P}[\gamma] \equiv {\top\P}                                                 \\
  & {\tt\P}             && : \Tm\,\Gamma\,{\top\P}                                                            \\
  & \Sigma\P            && : (A:\TyP\,\Gamma)\ra\TyP\,(\Gamma\rhd{{\uparrow} A})\ra\TyP\,\Gamma               \\
  & {\Sigma\P[]}        && : ({\Sigma\P}\,A\,B)[\gamma] \equiv {\Sigma\P}\,(A[\gamma])\,(B[\gamma\circ\p,\q]) \\
  & \blank{{,}\P}\blank && : (a:\Tm\,\Gamma\,({\uparrow}A))\ra\Tm\,\Gamma\,({\uparrow}B[\id,a])\ra \Tm\,\Gamma\,({\uparrow}\Sigma\P\,A\,B) \\
  & \pi_1\P             && : \Tm\,\Gamma\,({\uparrow}\Sigma\P\,A\,B)\ra\Tm\,\Gamma\,A \\
  & \pi_2\P             && : (\ab:\Tm\,\Gamma\,({\uparrow}\Sigma\P\,A\,B))\ra\Tm\,\Gamma\,({\uparrow}B[\id,\pi_1\,\ab]) \\
  & \Pi\P               && : (A:\Ty\,\Gamma)\ra\TyP\,(\Gamma\rhd A)\ra\TyP\,\Gamma               \\
  & {\Pi\P[]}           && : ({\Pi\P}\,A\,B)[\gamma] \equiv {\Pi\P}\,(A[\gamma])\,(B[\gamma\circ\p,\q]) \\
  & \lam\P              && : \Tm\,(\Gamma\rhd A)\,({\uparrow}B) \ra \Tm\,\Gamma\,({\uparrow}\Pi\P\,A\,B) \\
  & \app\P              && :  \Tm\,\Gamma\,({\uparrow}\Pi\P\,A\,B)\ra\Tm\,(\Gamma\rhd A)\,({\uparrow}B)
\end{alignat*}
\caption{A model of type theory has a sort of proof-irrelevant
  propositions closed under $\top$, $\Sigma$, $\Pi$.}
\label{fig:typ}
\end{figure}

We give some intuition for the description of type theory as a CwF
here. A gentler introduction is e.g.\ \cite{popl16}. Figure
\ref{fig:mltt} lists the components of a model of type theory with
$\top$, $\Sigma$, $\Pi$, $\bot$ and $\Id$ types. A model of type
theory consists of a category with families (CwF, left hand side of
the figure), that is, a
category of contexts and substitutions ($\Con,\dots,\mathsf{idr}$)
with a terminal object (the empty context $\blackdiamond$, the empty
substitution $\epsilon$, ${\blackdiamond\eta}$), a presheaf of types
($\Ty,\dots,[\id]$) and a locally representable dependent presheaf of
terms over types ($\Tm,\dots,{{\rhd}\eta}$). Local representability is
also called comprehension, and consists of the context extension
operation $\blank\rhd\blank$ together with the natural isomorphism
$\Sub\,\Delta\,(\Gamma\rhd A) \cong
(\gamma:\Sub\,\Delta\,\Gamma)\times\Tm\,\Delta\,(A[\gamma])$ witnessed
by $\blank,\blank,\dots,{{\rhd}\eta}$. Note that many operations have
implicit arguments, for example $\blank\circ\blank$ takes $\Gamma$,
$\Delta$, $\Theta$ implicitly. Also, some equations only typecheck
because of previous equations, for example, $[\id]$ for terms depends
on $[\id]$ for types: the left hand side is in
$\Tm\,\Gamma\,(A[\id])$, the right hand side is in
$\Tm\,\Gamma\,A$. We don't write the transports because we work in
extensional type theory.

Variables are represented using typed De Bruijn indices. The zero De
Bruijn index is $\q : \Tm\,(\Gamma\rhd A)\,(A[\p])$, the one index is
given by $\q[\p] : \Tm\,(\Gamma\rhd A\rhd B)\,(A[\p][\p])$, two is
$\q[\p][\p] : \Tm\,(\Gamma\rhd A\rhd B\rhd C)\,(A[\p][\p][\p])$, and
so on. Some provable equations and definable operations are listed in
Figure \ref{fig:abbrevs}.

The right hand side of Figure \ref{fig:mltt} lists rules for $\top$,
$\Sigma$, $\Pi$, $\bot$ and $\Id$ types, in this order. The first
three type formers have $\eta$ laws, the latter two don't (they are
instances of inductive types). Every operation comes with substitution
laws (e.g.\ $\lam[]$), some of them are not listed as they are
provable (see Figure \ref{fig:abbrevs}). Non-dependent special cases of
$\Pi$ and $\Sigma$ are also listed there.

Figure \ref{fig:typ} lists the operations and equations for a model
having a sort of definitionally proof-irrelevant propositions $\Ty\P$
which is closed under $\top$, $\Sigma$ and $\Pi$. Terms of
propositional types are expressed with the help of lifting $\uparrow$
which converts a $\TyP$ into a $\Ty$. Because of $\irr$, there is no
need to state equations for terms of lifted types, all equations hold.

Two important properties of models that we sometimes assume are
canonicity \cite{DBLP:journals/tcs/Coquand19} and normalisation
\cite{lmcs:4005,DBLP:journals/tcs/Coquand19}. Canonicity for $\bot$
says that there is no $\Tm\,\blackdiamond\,\bot$. Canonicity for $\Id$
says that for any $t:\Tm\,\blackdiamond\,(\Id_A\,a\,a')$, we have
$a\equiv a'$ and $t\equiv\refl$. Normalisation says that there is a
function from terms to normal forms $\mathsf{norm} : \Tm\,\Gamma\,A
\ra \Nf\,\Gamma\,A$ such that all terms are equal to their normalised
versions ($\ulcorner\blank\urcorner$ is the inclusion from $\Nf$ to
$\Tm$): for all $a:\Tm\,\Gamma\,A$,
$\ulcorner\mathsf{norm}\,a\urcorner = a$. Normal forms for the theory
of Figure \ref{fig:mltt} are defined mutually with variables and
neutral terms by the following three inductive types.
\begin{alignat*}{10}
  & x && ::= \q \,|\, x[\p] && \text{variables} \\
  & n && ::= x \,|\, \pi_1\,n \,|\, \pi_2\,n \,|\, n\oldapp v \,|\, \elim_\bot\,n \,|\, \J\,A\,v\,n \hspace{5em} && \text{neutral terms} \\
  & v && := n^{*} \,|\, \tt \,|\, (v,v) \,|\, \lam\,v \,|\, \refl && \text{normal forms}
\end{alignat*}
These should be understood as typed rules and there is a restriction
($n^{*}$) that only neutral terms at base types are included in normal
forms. Base types are $\bot$ and $\Id$ in our case.

Sometimes we just talk about intensional type theory when we don't
want to specify precisely what type formers we have in a model.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Point-free propositions internally}
\label{sec:internal}

In this section we show that (the dependent variant of) point-free
propositions is closed under $\top$, $\Sigma$ and $\Pi$. We work
internally to a model of type theory with a universe $\Type$ closed
under type formers $\Id$, $\top$, $\Sigma$, $\Pi$. This section was
formalised in Agda \cite{formalis}.

The $\eta$ rule for $\top$ says that for any two $t,t':\top$ we have
$t\equiv t'$, so we also have that $(\lambda(t\,t':\top).t) \equiv (\lambda
t\,t'.t')$, hence $\refl : \big((\lambda t\,t'.t) = (\lambda
t\,t'.t')\big) \equiv \isPfProp\,\top$.

As a warmup for $\Sigma$, we prove closure under non-dependent products.
\begin{proposition}
  If $\isPfProp\,A$ and $\isPfProp\,B$, then $\isPfProp\,(A\times B)$.
\end{proposition}
\begin{proof}
We assumed $p_A : \isPfProp\,A \equiv
\big((\lambda(a\,a':A).a)=(\lambda a\,a'.a')\big)$ and
$p_B : \isPfProp\,B \equiv \big((\lambda(b\,b':B).b)=(\lambda b\,b'.b')\big)$
and we want to obtain that $A\times B$ is a point-free proposition.
\begin{alignat*}{10}
  & p_{A\times B} :{} && \isPfProp\,(A\times B) \equiv \big((\lambda \ab\,\ab'.\ab) = (\lambda \ab\,\ab'.\ab')\big) \equiv \\
  & && \big((\lambda \ab\,\ab'.(\pi_1\,\ab,\pi_2\,\ab))=(\lambda \ab\,\ab'.(\pi_1\,\ab',\pi_2\,\ab'))\big)
\end{alignat*}
When rewriting the type of $p_{A\times B}$, we applied the $\eta$ rule
for products which says that $\ab \equiv (\pi_1\,\ab,\pi_2\,\ab)$ for
any $\ab:A\times B$. Then we prove the equality in two steps: first we
use $p_A$ to show that $\pi_1\,\ab = \pi_1\,\ab'$ while we keep the
$\pi_2\,\ab$ component constant
\begin{alignat*}{10}
  & p_{A\times B}^1 : \big(\lambda \ab\,\ab'.(\pi_1\,\ab,\pi_2\,\ab)\big)=\big(\lambda \ab\,\ab'.(\pi_1\,\ab',\pi_2\,\ab)\big) \\
  & p_{A\times B}^1 :\equiv \ap\,\big(\lambda z.\lambda \ab\,\ab'.(z\,(\pi_1\,\ab)\,(\pi_1\,\ab'), \pi_2\,\ab)\big)\,p_A,
\end{alignat*}
then we use $p_B$ to show that $\pi_2\,\ab = \pi_2\,\ab'$ while we
keep the $\pi_1\,\ab'$ components constant. In the middle we have the
function returning the mixed pair $(\pi_1\,\ab', \pi_2\,\ab)$.
\begin{alignat*}{10}
  & p_{A\times B}^2 : \big(\lambda \ab\,\ab'.(\pi_1\,\ab',\pi_2\,\ab)\big)=\big(\lambda \ab\,\ab'.(\pi_1\,\ab',\pi_2\,\ab')\big) \\
  & p_{A\times B}^2 :\equiv{} \ap\,\big(\lambda z.\lambda \ab\,\ab'.(\pi_1\,\ab', z\,(\pi_2\,\ab)\,(\pi_2\,\ab'))\big)\,p_B
\end{alignat*}
We obtain the desired equality via transitivity:
\begin{alignat*}{10}
  & p_{A\times B} :\equiv p_{A\times B}^1 \mathbin{\sqcdot} p_{A\times B}^2 \tag*{\qedhere}
\end{alignat*}
\end{proof}

To show closure of point-free propositions under $\Sigma$ types, we
have $A:\Type$, $B:A\ra\Type$, $\isPfProp\,A$, but assuming
$(a:A)\ra\isPfProp\,(B\,a)$ is not enough. We express that $B$ is a
family of propositions using a dependent version of $\isPfProp$:
\begin{alignat*}{10}
  & \isPfPropd : (A \ra \Type)\ra\Type \\
  & \isPfPropd\,B :\equiv \big(\lambda(a:A)(b\,b':B\,a).b\big)=(\lambda a\,b\,b'.b')
\end{alignat*}
The non-dependent version is a special case when there is an element
of the indexing type $a_0:A$, because given $B:\Type$ and $p_B :
\isPfPropd\,(\lambda(a:A).B)$, we have $\ap\,(\lambda z.z\,a_0)\,p_B :
\isPfProp\,B$.

We show the dependent version of closure under $\Sigma$ types.
\begin{proposition}
Given $A : D\ra\Type$ and $B:\Sigma\,D\,A\ra\Type$, if $\isPfPropd\,A$
and $\isPfPropd\,B$, then $\isPfPropd\,(\lambda
d.\Sigma\,(A\,d)\,(\lambda a.B\,(d,a)))$.
\end{proposition}
\begin{proof}
We have $p_A : \isPfPropd\,A \equiv (\lambda d\,a\,a'.a)=(\lambda
d\,a\,a'.a')$ and $p_B : \isPfPropd\,B \equiv (\lambda
\da\,b\,b'.b)=(\lambda \da\,b\,b'.b')$, our goal is to obtain
\[
 p_{\Sigma A B} : (\lambda d\,\ab\,\ab'.\ab) = (\lambda d\,\ab\,\ab'.\ab') \equiv (\lambda d\,\ab\,\ab'.(\pi_1\,\ab,\pi_2\,\ab)) = (\lambda d\,\ab\,\ab'.(\pi_1\,\ab', \pi_2\,\ab')).
\]
We want to prove this in two steps as for non-dependent products, but
because $B$ depends on $A$, the middle pair $(\pi_1\,\ab', \pi_2\,ab)$
is not well-typed. We replace the second component $\pi_2\,\ab :
B\,(d,\pi_1\,\ab)$ with
\[
\hphantom{f\,\ab\,\ab'\,e := {}} \transp_{\lambda a.B\,(d,a)}\,\Big(\ap\,\big(\lambda z.z\,d\,(\pi_1\,\ab)\,(\pi_1\,\ab')\big)\,p_A\Big)\,(\pi_2\,\ab) \hspace{0.6em}:\hspace{0.6em} B\,(d,\pi_1\,\ab'),\hspace{100em}
\]
and we will use a more general version of this second component defined as
\[
f\,\ab\,\ab'\,e := \transp_{\lambda a.B\,(d,a)}\,\Big(\ap\,\big(\lambda z.z\,d\,(\pi_1\,\ab)\,(\pi_1\,\ab')\big)\,e\hspace{0.78em}\Big)\,(\pi_2\,\ab) \hspace{0.6em}:\hspace{0.6em} B\,(d,h\,d\,(\pi_1\,\ab)\,(\pi_1\,\ab'))
\]
for any $d$, $\ab$, $\ab'$, $h$ and $e : (\lambda d\,a\,a'.a) = h$. Now the
first step has type
\begin{alignat*}{10}
  & p_{\Sigma A B}^1 :{} &&  (\lambda d\,\ab\,\ab'.\ab) = \big(\lambda d\,\ab\,\ab'.(\pi_1\,\ab',f\,\ab\,\ab'\,p_A)\big)
\end{alignat*}
and we prove it by induction on $p_A$ using $\J$:
\[
p_{\Sigma A B}^1 :\equiv \J\, \Big(\lambda h\,e . (\lambda d\,\ab\,\ab'.\ab)=\big(\lambda d\,\ab\,\ab' .(h\,d\,(\pi_1\,\ab)\,(\pi_1\,\ab') , f\,\ab\,\ab'\,e)\big)\Big)\,\refl\,p_A
\]
In the next step we simply use $\ap$ on $p_B$ and we conclude by transitivity:
\begin{alignat*}{10}
  & p_{\Sigma A B}^2 : \big(\lambda d\,\ab\,\ab'.(\pi_1\,\ab',f\,\ab\,\ab'\,p_A)\big) = (\lambda d\,\ab\,\ab'.\ab') \\
  & p_{\Sigma A B}^2 :\equiv \ap\,\Big(\lambda z.\lambda d\,\ab\,\ab'.\big(\pi_1\,\ab', z\,(d,\pi_1\,\ab')\,(f\,\ab\,\ab'\,p_A)\,(\pi_2\,\ab')\big) \Big)\,p_B \\
  & p_{\Sigma A B} :\equiv p_{\Sigma A B}^1 \mathbin{\sqcdot} p_{\Sigma A B}^2 \tag*{\qedhere}
\end{alignat*}\end{proof}
\begin{corollary}
  For $A:\Type$ and $B:A\ra\Type$, if $\isPfProp\,A$ and
  $\isPfPropd\,B$, then $\isPfProp\,(\Sigma\,A\,B)$.
\end{corollary}
Finally, we show closure of $\isPfPropd$ under dependent function space.
\begin{proposition}
  Given $A : D\ra\Type$, $B : \Sigma\,D\,A\ra\Type$, if
  $\isPfPropd\,B$, then \\ $\isPfPropd\,(\lambda d.(a:A\,d)\ra B\,(d,a))$.
\end{proposition}
\begin{proof}
  Using $p_B : (\lambda\da\,b\,b'.b)=(\lambda\da\,b\,b'.b')$, we define
  \begin{alignat*}{10}
    & p_{\Pi A B} : (\lambda d\,f\,f'.f)=(\lambda d\,f\,f'.f') \equiv (\lambda d\,f\,f'\,a.f\,a)=(\lambda d\,f\,f'\,a.f'\,a) \\
    & p_{\Pi A B} :\equiv \ap\,(\lambda z\,d\,f\,f'\,a.z\,(d,a)\,(f\,a)\,(f'\,a))\,p_B. \tag*{\qedhere}
  \end{alignat*}
\end{proof}
\begin{corollary}
  For $A:\Type$ and $B:A\ra\Type$, if $\isPfPropd\,B$, then
  $\isPfProp\,((a:A)\ra B\,a)$.
\end{corollary}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\vspace{-1.2em}
\section{Point-free propositions externally}
\label{sec:external}

In this section we show that any model of type theory with $\top$,
$\Sigma$, $\Pi$ types has a sort $\TyP$ closed under the same type
formers. This can be seen as an externalisation of the previous
section.

Recall that a model of type theory (a CwF, see Section \ref{sec:tt})
has a sort of strict propositions if there is a presheaf $\TyP$
together with a ``lifting'' natural transformation $\uparrow$ into
$\Ty$, and terms of a lifted type are equal.

First we define a predicate on types expressing externally that the
type is a point-free proposition.
\begin{definition}
  For a type $A:\Ty\,\Gamma$ in any CwF, let $\isExtPfProp\,A :\equiv
  (\q_{A}[\p_{A[\p]}] \equiv \q_{A[\p]})$.
\end{definition}
That is, in the context $\Gamma\rhd A\rhd A[\p]$, the terms $\q[\p]$
and $\q$ (1 and 0 De Bruijn indices, both having type $A[\p][\p]$) are
definitionally equal. We call this the external variant of $\pfProp$
because it is clear that it is equivalent to saying
$\lam\,(\lam\,(\q[\p])) \equiv \lam\,(\lam\,\q)$ which is the external
statement of $\lambda x\,y.x = \lambda x\,y.y$. In the next section,
we will relate the external and internal variants formally.

Elements of a type which $\isExtPfProp$ are equal in any context.
\begin{proposition}\label{prop:extpfprop-equiv}
For a type A, $\isExtPfProp\,A$ is equivalent to
\[
u \equiv v \text{ for all } \gamma:\Sub\,\Delta\,\Gamma \text{ and } u,v:\Tm\,\Delta\,(A[\gamma]).
\]
\end{proposition}
\begin{proof}
  Left to right: we have $\q[\p][\gamma,u,v] \equiv \q[\gamma,u,v]$,
  hence $u\equiv v$. Right to left: we choose $u:\equiv\q[\p]$,
  $v:\equiv\q$.
\end{proof}

In category theory, external point-free propositions over $\Gamma$ are
called subobjects of $\Gamma$.
\begin{proposition}\label{prop:subobject}
For an $A : \Ty\,\Gamma$, $\isExtPfProp\,A$ is equivalent to the
morphism $\p_A : \Sub\,(\Gamma\rhd A)\,\Gamma$ being a monomorphism.
\end{proposition}
\begin{proof}
  Left to right: given $\p_A\circ(\gamma,a) \equiv
  \p_A\circ(\gamma',a')$, we need to show $(\gamma,a) \equiv
  (\gamma',a')$. Using the assumption we have $\gamma \equiv
  \p_A\circ(\gamma,a) \equiv \p_A\circ(\gamma',a') \equiv \gamma'$,
  hence $a$ and $a'$ are both in $\Tm\,\Delta\,(A[\gamma])$. We get $a
  \equiv a'$ from Proposition \ref{prop:extpfprop-equiv}.

  Right to left: given two terms $a, a' : \Tm\,\Gamma\,(A[\gamma])$,
  we have $\p_A\circ(\gamma,a) \equiv \gamma \equiv
  \p_A\circ(\gamma,a')$, hence by assumption $(\gamma,a) \equiv
  (\gamma,a')$ and applying $\q[\blank]$ to both sides we obtain $a \equiv a'$.
\end{proof}


\begin{construction}\label{constr:typ}
  Every CwF with $\top$, $\Sigma$, $\Pi$ can be equipped with a sort
  of strict propositions closed under the same type formers.
\end{construction}
\begin{proof}[Construction]
  We have to define all components in Figure \ref{fig:typ}. We define
  \[
  \TyP\,\Gamma :\equiv (A:\Ty\,\Gamma)\times \isExtPfProp\,A.
  \]
  Substitution is defined by ordinary type substitution of the first
  component and the equation for substituted types holds by the
  following argument.
  \begin{alignat*}{10}
    & \q_{A[\gamma]}[\p_{A[\gamma][\p]}] \\[-0.7em]
    & && \equiv ([{\circ}], {\rhd\beta}_1, {\rhd\beta}_2) \\[-0.7em]
    & \q_A[\p_{A[\p]}][\gamma\circ\p\circ\p,\q_{A[\gamma]}[\p_{A[\gamma][\p]}],\q_{A[\gamma][\p]}] \\[-0.7em]
    & && \equiv \text{(assumption)} \\[-0.7em]
    & \q_{A[\p]}[\gamma\circ\p\circ\p,\q_{A[\gamma]}[\p_{A[\gamma][\p]}],\q_{A[\gamma][\p]}] \\[-0.7em]
    & && \equiv ({\rhd\beta}_2) \\[-0.7em]
    & \q_{A[\gamma][\p]})
  \end{alignat*}
  The $\uparrow$ operation is defined by ${\uparrow}(A,p_A) :\equiv
  A$. Irrelevance holds by Proposition
  \ref{prop:extpfprop-equiv}. $\top\P$ is defined as $\top$ and
  $\isExtPfProp\,\top$ holds by $\top\eta$. We define
  $\Sigma\P\,(A,p_A)\,(B,p_B)$ by $(\Sigma\,A\,B,p_{\Sigma A B})$
  where $p_{\Sigma A B}$ is proven using Proposition
  \ref{prop:extpfprop-equiv} for
  $u,v:\Tm\,\Delta\,(\Sigma\,A\,B[\gamma])$ by
  \[
     u \overset{\Sigma\eta}{\equiv} (\pi_1\,u,\pi_2\,u) \overset{p_A, p_B}{\equiv} (\pi_1\,v,\pi_2\,v) \overset{\Sigma\eta}{\equiv} v.
  \]
  We define $\Pi\P\,A\,(B,p_B)$ by $(\Pi\,A\,B,p_{\Pi A B})$ where
  $p_{\Pi A B}$ is proven using Proposition \ref{prop:extpfprop-equiv}
  for $u,v:\Tm\,\Delta\,(\Pi\,A\,B[\gamma])$ by
  \[
     u \overset{\Pi\eta}{\equiv} \lam\,(\app\,u) \overset{p_B}{\equiv}
     \lam\,(\app\,v) \overset{\Pi\eta}{\equiv} v. \tag*{\qedhere}
  \]
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Relationship of different notions of being a proposition}
\label{sec:relation}

For a type family $A:D\ra\Type$, being a family of homotopy
propositions and a family of point-free propositions were defined
internally as follows.
\begin{alignat*}{10}
  & \isHPropd\, A && \equiv (d:D)(a\,a':A\,d)\ra\Id_{(A\,d)}\,a\,a' \\
  & \isPfPropd\,A && \equiv \Id_{((d:D)\ra A\,d\ra A\,d\ra A\,d)}\,(\lambda d\,a\,a'.a)\,(\lambda d\,a\,a'.a')
\end{alignat*}
Externally, these can be seen as the following two elements of
$\Ty\,\blackdiamond$ for $A : \Ty\,(\blackdiamond\rhd D)$. We also
repeat the definition of $\isExtPfProp$ for comparison which is a
metatheoretic equality.
\begin{alignat*}{10}
  & \isHPropd\,A && \equiv \Pi\,D\,\Big(\Pi\,A\,\big(\Pi\,(A[\p])\,(\Id_{A[\p][\p]}\,(\q[\p])\,\q)\big)\Big) \\
  & \isPfPropd\,A && \equiv \Id_{\Pi\,D\,(A\Ra A\Ra A)}\,\big(\lam\,(\lam\,(\lam\,(\q[\p])))\big)\,\big(\lam\,(\lam\,(\lam\,\q))\big) \\
  & \isExtPfProp\,A && \equiv (\q[\p] \equiv \q) \hspace{5.7em} \text{(both sides in $\Tm\,(\blackdiamond\rhd D\rhd A\rhd A[\p])\,(A[\p][\p])$)}
\end{alignat*}
We first compare internal point-free propositions and external
ones. They coincide for a type where we collect all dependencies into
a single closed type $D$.
\begin{proposition}\label{prop:intext}
  In a model of type theory with $\Pi$, $\Id$ and canonicity, given an
  $A : \Ty\,(\blackdiamond\rhd D)$, there is a
  $\Tm\,\blackdiamond\,(\isPfPropd\,A)$ if and only if
  $\isExtPfProp\,A$.
\end{proposition}
\begin{proof}
  Right to left: if $\q[\p] \equiv \q$ in $\Tm\,(\blackdiamond\rhd
  D)\,A$, then
  $\lam\,(\lam\,(\lam\,(\q[\p])))\equiv\lam\,(\lam\,(\lam\,\q))$,
  hence $\refl : \Tm\,\blackdiamond\,(\isPfPropd\,A)$.

  Left to right: we have $ t :
  \Tm\,\blackdiamond\,\Big(\Id_{\Pi\,D\,(A\Ra A\Ra
    A)}\,\big(\lam\,(\lam\,(\lam\,(\q[\p])))\big)\,\big(\lam\,(\lam\,(\lam\,\q))\big)\Big).
  $ Canonicity for $\Id$ implies that $\lam\,(\lam\,(\lam\,(\q[\p])))
  \equiv \lam\,(\lam\,(\lam\,\q))$, hence
  \[
  \app\,(\app\,(\app\,(\lam\,(\lam\,(\lam\,(\q[\p])))))) \equiv \app\,(\app\,(\app\,(\lam\,(\lam\,(\lam\,\q))))).
  \]
  Now using $\Pi\beta$ three times on both sides we obtain $\q[\p]
  \equiv \q$ where both sides are in $\Tm\,(\blackdiamond\rhd D\rhd
  A\rhd A[\p])\,(A[\p][\p])$, and this is $\isExtPfProp\,A$.
\end{proof}
\begin{corollary}\label{cor:intext}
  In a model of type theory with $\Pi$, $\Id$ and canonicity, given a
  closed type $A$, $\Tm\,\blackdiamond\,(\isPfProp\,A)$ if and only if
  $\isExtPfProp\,A$.
\end{corollary}
In an open context, external point-free propositions are stronger than
internal ones.
\begin{proposition}
  In a model of type theory with $\Pi$, $\Id$, a type $\U$ and a
  family over it $\El$ (a possibly empty universe) and normalisation, we have
  $A:\Ty\,\Gamma$ such that $\Tm\,\Gamma\,(\isPfProp\,A)$, but not
  $\isExtPfProp\,A$.
\end{proposition}
\begin{proof}
  Pick $\Gamma :\equiv
  \blackdiamond\rhd\U\rhd\Id_{\El\,\q\Ra\El\,\q\Ra\El\,\q}\,(\lam\,(\lam\,(\q[\p])))\,(\lam\,(\lam\,\q))$
  and $A :\equiv \El\,(\q[\p])$. Now $\q[\p]$ and $\q$ both in
  $\Tm\,(\Gamma\rhd A\rhd A[\p])\,(A[\p\circ\p])$ have different normal forms.
\end{proof}
Next, we describe the relationship of homotopy and point-free
propositions. Here we use the non-dependent variants.
\begin{proposition}\label{prop:hpropPfProp}
  \begin{enumerate}[(i)]
  \item In a model of type theory with $\Pi$ and $\Id$, $\isPfProp\,A$
    implies $\isHProp\,A$.
  \item In a model of type theory with $\Pi$, $\Id$, an inductively
    defined $\bot$ and normalisation,
    \begin{enumerate}[(a)]
    \item we have $\isHProp\,\bot$, but not $\isPfProp\,\bot$.
    \item we don't have that for any type $A$,
      $\isPfProp\,(\isPfProp\,A)$.
    \end{enumerate}
  \item In a model of type theory with $\Pi$, $\Id$ and function
    extensionality, $\isHProp\,A$ implies $\isPfProp\,A$.
  \end{enumerate}
\end{proposition}
\begin{proof}
  \begin{enumerate}[(i)]
  \item We work internally. Given $p_A : \isPfProp\,A \equiv (\lambda
    (a\,a':A).a)=(\lambda a\,a'.a')$, we define $\lambda
    a\,a'.\ap\,(\lambda z.z\,a\,a')\,p_A : \isHProp\,A$.
  \item
    \begin{enumerate}[(a)]
    \item Internally, we have $\lambda b.\elim_\bot\,b :
      \isHProp\,\bot$. Let's assume
      $\Tm\,\blackdiamond\,(\isPfProp\,\bot)$. From Corollary
      \ref{cor:intext} and Proposition \ref{prop:extpfprop-equiv}, any
      two elements of $\bot$ in any context are equal. But from
      normalisation we have $\q[\p]\not\equiv \q :
      \Tm\,(\blackdiamond\rhd\bot\rhd\bot)\,\bot$ as they have
      different normal forms.
    \item Assuming $\isPfProp\,(\isPfProp\,\bot)$, we obtain
      \[
      \q[\p]\equiv \q : \Tm\,(\blackdiamond\rhd\isPfProp\,\bot\rhd\isPfProp\,\bot)\,(\isPfProp\,\bot)
      \]
      the same way as in (a), but they have different normal forms.
    \end{enumerate}
  \item We have to show that $\isHProp\,A$ implies $\isPfProp\,A$. We
    work internally by the following double application of function
    extensionality.
    \begin{alignat*}{10}
      & \isHProp\,A \\[-0.7em]
      & && \equiv \\[-0.7em]
      & \big((a\,a':A)\ra a=a'\big) \\[-0.7em]
      & && \equiv \\[-0.7em]
      & \big((a:A)(a':A)\ra(\lambda a'.a)\,a'=(\lambda a'.a')\,a'\big) \\[-0.7em]
      & && \ra \text{(function extensionality)} \\[-0.7em]
      & \big((a:A)\ra(\lambda a'.a)=(\lambda a'.a')\big) \\[-0.7em]
      & && \equiv \\[-0.7em]
      & \big((a:A)\ra(\lambda a\,a'.a)\,a=(\lambda a\,a'.a')\,a\big) \\[-0.7em]
      & && \ra \text{(function extensionality)} \\[-0.7em]
      & (\lambda a\,a'.a')=(\lambda a\,a'.a') \\[-0.7em]
      & && \equiv \\[-0.7em]
      & \isPfProp\,A \tag*{\qedhere}
    \end{alignat*}
  \end{enumerate}
\end{proof}
%\vspace{-0.5em}
From the previous section, we know that $\TyP$ can be defined using
$\isExtPfProp$. If we start with a model that already has $\TyP$, it
is natural to ask about the relationship of $\TyP$ and the other
notions of being a proposition.
\begin{proposition}
  \begin{enumerate}[(i)]
  \item In a model of type theory with $\Pi$, $\Id$ and $\TyP$, if
    $A:\TyP\,\Gamma$, then $\Tm\,\Gamma\,(\isHProp\,({\uparrow}A))$,
    $\Tm\,\Gamma\,(\isPfProp\,({\uparrow}A))$ and $\isExtPfProp\,({\uparrow}A)$.
  \item In a model of type theory with $\Pi$, $\Sigma$ and $\Id$, if for
    every type $A$, $\isHProp\,A$ implies $\isExtPfProp\,A$, then the
    model has equality reflection.
  \end{enumerate}
\end{proposition}
\begin{proof}
  \begin{enumerate}[(i)]
  \item Because any two terms of type ${\uparrow} A$ are
    definitionally equal by $\irr$, internally $\lambda a\,a'.\refl :
    \isHProp\,A$ and $\refl : \isPfProp\,A$.
  \item The proof is from
    \cite{DBLP:journals/pacmpl/GilbertCST19}. Singleton types are in
    $\hProp$, that is, internally
    $\isHProp\,((a':A)\times\Id_A\,a\,a')$ holds for any $a$, but if
    $\isExtPfProp\,((a':A)\times\Id_A\,a\,a')$, then for any $e :
    \Id_A\,a\,a'$, we have $(a,\refl) \equiv (a',e)$, hence $a \equiv
    \pi_1\,(a,\refl) \equiv \pi_1\,(a',e) \equiv a'$.
  \end{enumerate}
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\vspace{-1.5em}

\section{The setoid model externally}
\label{sec:setoid}

In this section, from a model of type theory with $\top$, $\Sigma$ and
$\Pi$, we build another model of type theory with the same type
formers and a strict identity type, a strong transport rule and
function extensionality. Strictness of the identity type means that
any two elements of the identity type are definitionally equal (it is
an external point-free proposition, $\isExtPfProp$). Strength of
transport means that we can transport an element of any family of
types, not only families of strict propositions. In contrast, Agda and
the method described in \cite{DBLP:journals/pacmpl/GilbertCST19} only
support a strict identity type with a weak transport: the identity
type is $\mathsf{Prop}$-valued and we can only transport along
$\mathsf{Prop}$-valued families.

In Section \ref{sec:setoid_internal}, we describe an internal version
of this model construction where we define a model internally to an
intensional metatheory. Section \ref{sec:setoid_internal} relates to
this section as the section on internal point-free propositions
(Section \ref{sec:internal}) relates to the section on external
point-free propositions (Section \ref{sec:external}).
%
The model construction in this section follows those in
\cite{setoid,DBLP:conf/fossacs/AltenkirchBKSS21} with some small
improvements, but is defined in a more restricted setting: we do not
assume that the input model has a universe of strict propositions.

Note that even if our metatheory is extensional type theory, we do not
rely on any extensionality features in the input model. We only use an
extensional metatheory for convenience. Following Hofmann's
conservativity theorem \cite{hofmann95conservativity}, our arguments
can be replayed in an intensional metatheory with function
extensionality and uniqueness of identity proofs.

\begin{construction}\label{constr:setoid_external}
  From an input model of type theory with $\top$, $\Sigma$, $\Pi$, a
  sort $\Ty\P$ closed under $\top\P$, $\Sigma\P$ and $\Ty\P$ (as in
  Figure \ref{fig:typ}), we construct a model of type theory with the
  same type formers and a $\Ty\P$-valued identity type with a strong
  transport rule and function extensionality.
\end{construction}
\begin{proof}[Construction]
A context in the output model is a context in the input model together
with an $\hProp$-valued equivalence relation on substitutions into
that context. Note that as our metatheory is extensional type theory,
$\hProp$ and $\pfProp$ coincide.
\begin{alignat*}{10}
  & \Con :\equiv && && (|\Gamma| && :\Con) \\
  & && \times && (\Gamma^\sim && : \Sub\,\Xi\,|\Gamma|\ra\Sub\,\Xi\,|\Gamma|\ra\hProp) \\
  & && \times && (\blank[\blank]_\Gamma && : \Gamma^\sim\,\gamma_0\,\gamma_1\ra(\xi:\Sub\,\Xi'\,\Xi)\ra \Gamma^\sim\,(\gamma_0\circ\xi)\,(\gamma_1\circ\xi)) \\
  & && \times && (\RR_\Gamma && : (\gamma:\Sub\,\Xi\,|\Gamma|)\ra\Gamma^\sim\,\gamma\,\gamma) \\
  & && \times && (\SS_\Gamma && : \Gamma^\sim\,\gamma_0\,\gamma_1\ra\Gamma^\sim\,\gamma_1\,\gamma_0) \\
  & && \times && (\TT_\Gamma && : \Gamma^\sim\,\gamma_0\,\gamma_1\ra\Gamma^\sim\,\gamma_1\,\gamma_2\ra\Gamma^\sim\,\gamma_0\,\gamma_2)
\end{alignat*}
In \cite{setoid}, the relation for contexts was $\Ty\P$-valued, not
metatheoretic proposition ($\hProp$)-valued. We chose to use $\hProp$
for reasons of modularity: now the category part of the output model
($\Con$, $\Sub$) only refers to the category part of the input
model. Note that the relation for types is $\Ty\P$-valued.

Substitutions are substitutions in the input model which respect the relation.
\[
  \Sub\,\Delta\,\Gamma :\equiv (|\gamma|:\Sub\,|\Delta|\,|\Gamma|) \times  (\gamma^\sim  : \Delta^\sim\,\delta_0\,\delta_1\ra\Gamma^\sim\,(|\gamma|\circ\delta_0)\,(|\gamma|\circ\delta_1))
\]
Composition and identities are composition and identities from the
input model where the $^\sim$ components are defined by function
composition and the identity function. In fact, up to $\Pi$ types, all
the $|\blank|$ components in the output model are the corresponding
components of the input model.

The empty context is defined as $|\blackdiamond|:\equiv\blackdiamond$
and $\blackdiamond^\sim\,\sigma_0\,\sigma_1 :\equiv \top$ which is
trivially an equivalence relation.

Types are displayed setoids with $\TyP$-valued relations together with
coercion and coherence operations.
\begin{alignat*}{10}
  & \rlap{$\Ty\,\Gamma :\equiv$} \\
  & && (|A| && :\Ty\,|\Gamma|) \\
  & \times && (A^\sim && : \Gamma^\sim\,\gamma_0\,\gamma_1\ra\Tm\,\Xi\,(|A|[\gamma_0])\ra\Tm\,\Xi\,(|A|[\gamma_1])\ra\TyP\,\Xi) \\
  & \times && (A^\sim[] && : (A^\sim\,\gamma_{01}\,a_0\,a_1)[\xi] \equiv A^\sim\,(\gamma_{01}[\xi]_\Gamma)\,(a_0[\xi])\,(a_1[\xi])) \\
  & \times && (\RR_A && : (a:\Tm\,\Xi\,(|A|[\gamma]))\ra\Tm\,\Xi\,({\uparrow}A^\sim\,(\RR_\Gamma\,\gamma)\,a\,\,a)) \\
  & \times && (\SS_A && : \Tm\,\Xi\,({\uparrow}A^\sim\,\gamma_{01}\,a_0\,a_1)\ra\Tm\,\Xi\,({\uparrow}A^\sim\,(\SS_\Gamma\,\gamma_{01})\,a_1\,a_0)) \\
  & \times && (\TT_A && : \Tm\,\Xi\,({\uparrow}A^\sim\,\gamma_{01}\,a_0\,a_1)\ra\Tm\,\Xi\,({\uparrow}A^\sim\,\gamma_{12}\,a_1\,a_2)\ra\Tm\,\Xi\,({\uparrow}A^\sim\,(\TT_\Gamma\,\gamma_{01}\,\gamma_{12})\,a_0\,a_2)) \\
  & \times && (\coe_A && : \Tm\,\Xi\,({\uparrow}\Gamma^\sim\,\gamma_0\,\gamma_1)\ra\Tm\,\Xi\,(|A|[\gamma_0])\ra\Tm\,\Xi\,(|A|[\gamma_1])) \\
  & \times && (\coe_A[] && : \coe_A\,\gamma_{01}\,a_0[\xi] \equiv \coe_A\,(\gamma_{01}[\xi]_\Gamma)\,(a_0[\xi])) \\
  & \times && (\coh_A && : (\gamma_{01}:\Tm\,\Xi\,({\uparrow}\Gamma^\sim\,\gamma_0\,\gamma_1))(a_0:\Tm\,\Xi\,(|A|[\gamma_0]))\ra\Tm\,\Xi\,({\uparrow}A^\sim\,\gamma_{01}\,a_0\,(\coe_A\,\gamma_{01}\,a_0)))
\end{alignat*}
Type substitution is given by type substitution in the input model and
function composition for the other components.

Terms are terms which respect the (displayed) equivalence relations.
\[
   \Tm\,\Gamma\,A :\equiv   (|t|  :\Tm\,|\Gamma|\,|A|) \times  (t^\sim  : (\gamma_{01}:\Gamma^\sim\,\gamma_0\,\gamma_1)\ra\Tm\,\Xi\,({\uparrow}A^\sim\,\gamma_{01}\,(|t|[\gamma_0])\,(|t|[\gamma_1])))
\]
Term substitution is given by term substitution in the input model and
function composition for the $^\sim$ component.

Context extension is context extension $|\Gamma\rhd A| :\equiv
|\Gamma|\rhd|A|$, the relation is given by metatheoretic $\Sigma$
types: $(\Gamma\rhd A)^\sim\,(\gamma_0,a_0)\,(\gamma_1,a_1) :\equiv
(\gamma_{01}:\Gamma^\sim\,\gamma_0\,\gamma_1)\times\Tm\,\Xi\,({\uparrow}A^\sim\,\gamma_{01}\,a_0\,a_1)$. This
is an equivalence relation because $\Gamma^\sim$ is an equivalence
relation and $A^\sim$ is a displayed equivalence relation. The $^\sim$
components of $\blank,\blank$, $\p$ and $\q$ are given by pairing and
projections for metatheoretic $\Sigma$ types. The equations
${\rhd}\beta_1$, ${\rhd}\beta_2$, ${\rhd}\eta$ follow from $\beta$,
$\eta$ for metatheoretic $\Sigma$ types.
%
The unit type $\top$ is given by $|\top|:\equiv\top$, $\top^\sim\,\gamma_{01}\,t_0\,t_1 :\equiv \top\P$.

$\Sigma$ types use $\Sigma\P$ for the relation:
we define $|\Sigma\,A\,B|:\equiv\Sigma\,|A|\,|B|$ and
\[
(\Sigma\,A\,B)^\sim\,\gamma_{01}\,(a_0,b_0)\,(a_1,b_1) :\equiv \Sigma\P\,(A^\sim\,\gamma_{01}\,a_0\,a_1)\,(B^\sim\,(\gamma_{01}[\p],\q)\,(b_0[\p])\,(b_1[\p])).
\]
All the other components are pointwise, for example $\RR_{\Sigma\,A\,B}\,(a,b) :\equiv (\RR_A\,a \mathbin{{,}\P} \RR_B\,b)$ and
\[
\coe_{\Sigma\,A\,B}\,\gamma_{01}\,(a_0,b_0):\equiv (\coe_A\,\gamma_{01}\,a_0,\coe_B\,(\gamma_{01},\coh_A\,\gamma_{01}\,a_0)\,b_0).
\]
Pairing, first and second projection and the computation rules are
straightforward. Note that to prove e.g.\ $\pi_1\,(a,b) \equiv a$, it
is enough to compare the first components, i.e.\ $|\pi_1\,(a,b)|
\equiv |a|$ as the second components are equal by $\irr$.

For $\Pi$ types, the $|\blank|$ component includes $^\sim$ components of the constituent types:
\begin{alignat*}{10}
  & \rlap{$|\Pi\,A\,B| :\equiv$} \\
  & \hspace{2em} \Sigma\, && (\Pi\,|A|\,|B|)\,\\
  & && \bigg(\Pi\P\,(|A|[\p])\,\Big(\Pi\P\,(|A|[\p^2])\,\big(\Pi\P\, && ({\uparrow}A^\sim\,(\RR_\Gamma\,\p^3)\,(\q[\p])\,\q) \\[-1em]
  & && && (B^\sim\,(\RR_\Gamma\,\p^4,\q)\,(\q[\p^3]\oldapp\q[\p^2])\,(\q[\p^3]\oldapp\q[\p]))\big)\Big)\bigg)
\end{alignat*}
Functions are given by functions which respect the relation: for any
two elements of $|A|$ that are related by $A^\sim$, the outputs of the
function are related by $B^\sim$. We wrote $\p^2$ for $\p\circ\p$.
With variable names and without weakenings, the same definition is
written
\[
\Sigma(f:\Pi(a:|A|).|B|).\Pi\P(a_0\,a_1:|A|,a_{01}:{\uparrow}A^\sim\,(\RR_\Gamma\,\id)\,a_0\,a_1).B^\sim\,(\RR_\Gamma\,\id,a_{01})\,(f\oldapp a_0)\,(f\oldapp a_1)).
\]
The relation for $\Pi$ types says
that two functions are related if they map related inputs to related
outputs:
\begin{alignat*}{10}
  & (\Pi\,A\,B)^\sim\,\gamma_{01}\,t_0\,t_1 :\equiv \\
  & \hspace{0.5em} \Pi\P\,(|A|[\gamma_0])\,\Big(\Pi\P\,(|A|[\gamma_1\circ\p])\,\big(\Pi\P\, && ({\uparrow}A^\sim\,(\gamma_{01}[\p^2]_\Gamma)\,(\q[\p])\,\q) \\[-0.5em]
  & && (B^\sim\,(\gamma_{01}[\p^3]_\Gamma,\q)\,(t_0[\p^3]\oldapp(\q[\p^2]))\,(t_1[\p^3]\oldapp(\q[\p])))\big)\Big)
\end{alignat*}
Reflexivity for $\Pi$ types is second projection: $\RR_{\Pi\,A\,B}\,t
:\equiv \pi_2\,t$. The other components are defined as in
\cite{setoid}. The definition of $\lam$ and $\app$ are
straightforward. Just as for $\Pi$, the definition of $|\lam\,t|$
involves both $|t|$ and $t^\sim$. When comparing two elements of
$|\Pi\,A\,B|$ for equality, only the first components of the $\Sigma$
types have to be compared, the second components are equal by $\irr$.

The sort $\Ty\P$ is defined by $\Ty\P$s in the input model together with coercion.
\[
\Ty\P\,\Gamma :\equiv (|A|:\Ty\P\,|\Gamma|)\times(\coe_A : \Gamma^\sim\,\gamma_0\,\gamma_1\ra\Tm\,\Xi\,({\uparrow}|A|[\gamma_0])\ra\Tm\,\Xi\,({\uparrow}|A|[\gamma_1]))
\]
Compared to $\Ty$ which had nine components, $\Ty\P$ has only two. All
the other components that $\Ty$ had are irrelevant for propositional
types. Lifting is given by lifting in the input model, the relation is
trivial and coercion comes from the coercion component in $\Ty\P$:
\[
   |{\uparrow}A| :\equiv {\uparrow}|A| \hspace{6em}   ({\uparrow}A)^\sim\,\gamma_{01}\,a_0\,a_1 :\equiv \top\P \hspace{6em}  \coe_{{\uparrow}A}\,\gamma_{01}\,a_0 :\equiv \coe_A\,\gamma_{01}\,a_0
\]

$\Ty\P$ is closed under $\top\P$, $\Sigma\P$ and $\Pi\P$.

Thus we constructed a model of type theory with $\top$, $\Pi$,
$\Sigma$ and a sort $\Ty\P$ closed under the same type formers.

This model has an identity type $\Id_A\,a\,a' : \Ty\P\,\Gamma$ for $a,a' : \Tm\,\Gamma\,A$.
\begin{alignat*}{10}
  & |\Id_A\,a\,a'| :\equiv A^\sim\,(\RR_\Gamma\,\id)\,a\,a'  \hspace{6em} (\Id_A\,a\,a')^\sim\,\gamma_{01}\,e_0\,e_1 :\equiv \top\P \\
  & \coe_{\Id_A\,a\,a'}\,\gamma_{01}\,\hspace{-2em}\underbrace{e}_{: A^\sim\,(\RR_\Gamma\,\gamma_0)\,(a[\gamma_0])\,(a'[\gamma_0])} :\equiv \underbrace{\TT_A\,\underbrace{(a^\sim\,(\SS_\Gamma\,\gamma_{01}))}_{: A^\sim\,(\SS_\Gamma\,\gamma_{01})\,(a[\gamma_1])\,(a[\gamma_0])}\,\big(\TT_A\,e\,\underbrace{({a'}^\sim\,\gamma_{01})}_{: A^\sim\,\gamma_{01}\,(a'[\gamma_0])\,(a'[\gamma_1])}\big)}_{: A^\sim\,(\RR_\Gamma\,\gamma_1)\,(a[\gamma_1])\,(a'[\gamma_1])}
\end{alignat*}
It has a constructor $\refl$ and an eliminator $\transp$ ($\J$ is a
consequence of transport as equality is proof-irrelevant).
\begin{alignat*}{10}
  & \refl && : \Tm\,\Gamma\,({\uparrow}\Id_A\,a\,a) \\
  & |\refl| && :\equiv \RR_A\,a \\
  & \refl^\sim\,\gamma_{01} && :\equiv \tt\P \\
  & \transp && : (P:\Ty\,(\Gamma\rhd A))\ra\Tm\,\Gamma\,({\uparrow}\Id_A\,a\,a')\ra\Tm\,\Gamma\,(P[\id,a])\ra\Tm\,\Gamma\,(P[\id,a']) \\
  & |\transp\,P\,e\,u| && :\equiv \coe_P\,(\RR_\Gamma\,\id,|e|)\,|u|
\end{alignat*}
The computation rule of $\transp$ only holds up to $\Id$, but as
described in \cite{setoid}, the model can be refined to support a
definitional computation rule. Note that transport works with
arbitrary $\Ty$-motive, the motive does not have to be $\TyP$ (as
opposed to the inductively defined $\mathsf{Prop}$-valued identity
type in Agda). Function extensionality holds by definition of the
identity type.
\end{proof}

\begin{construction}
  From an input model of type theory with $\top$, $\Sigma$, $\Pi$, we
  construct a model of type theory with $\top$, $\Sigma$, $\Pi$, a
  sort of propositions $\Ty\P$ closed under $\top$, $\Sigma$, $\Pi$
  and a $\Ty\P$-valued identity type with a strong transport rule and
  function extensionality.
\end{construction}
\begin{proof}[Construction]
  We take the input model, equip it with $\Ty\P$ using Construction
  \ref{constr:typ}, then invoke Construction \ref{constr:setoid_external}.
\end{proof}

The above construction can be extended with the empty type: if the
input model has $\bot:\Ty$, the output model also supports $\bot:\Ty$
with its elimination rule, but we do not have $\bot:\Ty\P$ (unless
$\isExtPfProp\,\bot$ in the input model). Similarly, to justify
booleans in the output model, we need that the input model has
booleans and a definitionally proof-irrelevant family over booleans
that we can use to define identity for booleans:
\begin{alignat*}{10}
  & \Id\Bool && : \Ty\,(\Gamma\rhd\Bool\rhd\Bool) \\
  & \Id\true && : \Tm\,\Gamma\,(\Id\Bool[\id,\true,\true]) \\
  & \Id\false && : \Tm\,\Gamma\,(\Id\Bool[\id,\false,\false]) \\
  & \Id\irr && : (e\,e':\Tm\,(\Gamma\rhd\Bool\rhd\Bool)\,\Id\Bool)\ra e\equiv e'
\end{alignat*}
But then we might as well require $\Ty\P$ in the input model with
closure under inductive types.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{The setoid model internally}
\label{sec:setoid_internal}

In the previous section we showed how a setoid model can be
constructed without requiring a sort $\Ty\P$ in the input model. Can
we redo the same internally to intensional type theory using
point-free propositions? That is, can we define a setoid model in Agda
(which can be viewed as the initial model of intensional type theory)
without using strict propositions ($\mathsf{Prop}$, $\Ty\P$)?

Compared to Construction \ref{constr:setoid_external} of the previous
section, the role of the input model is taken by our metatheory
(Agda), the role of the output model is the model we construct. The
equations of our model are given by the identity type of the
metatheory. If all the equations can be proven by $\refl$, it means
that the model is strict. In such a case an external model
construction can be obtained from the internal model (see
\cite[Section 3]{setoid} for an exposition of model constructions
vs.\ internal models through the example of the graph model). Model
constructions are also called syntactic translations, see
\cite{next700} for such a presentation.

The notion of model we construct is described in Figures
\ref{fig:mltt}, \ref{fig:abbrevs}, \ref{fig:typ} in extensional type
theory. As some operations and equations typecheck only because of
previous equations (e.g.\ ${\lam[]}$ depends on ${\Pi[]}$), the
complete intensional description of the notion of model has many
transports compared to this (see \cite{popl16} for an exposition using
explicit transports). However if an equation is proved by $\refl$ in
the model, then transports over it disappear, so \emph{concrete}
strict models can be defined in Agda without using any transports.

External model constructions where the definitions of types (and
substitutions and terms) don't involve equations can be internalised
immediately as strict models. This is the case for the setoid model
using $\Ty\P$, see \cite{setoid}. In our case however, there is an
equation expressing that the equivalence relation is a
proposition. This makes the construction more involved as we have to
prove that the witnesses of propositionality are equal.

The answer to the above question is yes. This section was formalised
in Agda \cite{formalis}.

\begin{construction}\label{constr:setoid_internal}
  We construct a model of type theory with $\bot$, $\top$, $\Sigma$,
  $\Pi$, a sort of propositions $\Ty\P$ closed under $\top$, $\Sigma$,
  $\Pi$, a $\Ty\P$-valued identity type with a strong transport rule
  and function extensionality. All equations of our model hold
  definitionally, with the exceptions $\irr$, $\Sigma[]$, ${{,}[]}$,
  $\Pi\eta$, $\Pi[]$, $\lam[]$.
\end{construction}
\begin{proof}[Construction]
  We explain the main components, for details consult the formalisation.

  We define contexts as setoids where the equivalence relation is a
  point-free proposition. Compare it with how contexts were defined in
  the external Construction \ref{constr:setoid_external}.
  \begin{alignat*}{10}
    & \Con :\equiv && && (|\Gamma| && : \Type) \\
    & && \times\, && (\Gamma^\sim && : |\Gamma|\times|\Gamma|\ra\Type) \\
    & && \times && (\Gamma^\p && : \isPfPropd\,\Gamma^\sim)  \\
    & && \times && (\RR_\Gamma && : (\gamma_x : |\Gamma|)\ra\Gamma^\sim\,(\gamma_x,\gamma_x)) \\
    & && \times && (\SS_\Gamma && : \Gamma^\sim\,(\gamma_0,\gamma_1)\ra\Gamma^\sim\,(\gamma_1,\gamma_0)) \\
    & && \times && (\TT_\Gamma && : \Gamma^\sim\,(\gamma_0,\gamma_1)\ra\Gamma^\sim\,(\gamma_1,\gamma_2)\ra\Gamma^\sim\,(\gamma_0,\gamma_2))
  \end{alignat*}
  We don't have equations on contexts, so it is not an issue that
  there is an equation ($\Gamma^\p$) as one of the components. There
  will be an issue for types, see below.

  Substitutions are functions that respect the relations.
  \[
    \Sub\,\Delta\,\Gamma :\equiv (|\gamma|:|\Delta|\ra|\Gamma|) \times  (\gamma^\sim  : \Delta^\sim\,(\delta_0,\delta_1)\ra\Gamma^\sim\,(|\gamma|\,\delta_0, |\gamma|\,\delta_1))
  \]
  They form a category with function composition (for both $|\blank|$
  and $\blank^\sim$ components) and the identity function. The
  categorical laws are definitional. The empty context is given by
  $\top$ with the constant $\top$ relation.

  Types are displayed setoids with coercion and coherence (note that
  later we will replace types by their strictified variants).
  \begin{alignat*}{10}
    & \rlap{$\Ty\,\Gamma :\equiv$} \\
    & && (|A| && :|\Gamma|\ra\Type) \\
    & \times && (A^\sim && : (\gamma_0:|\Gamma|)\times(\gamma_1:|\Gamma|)\times\Gamma^\sim\,\gamma_0\,\gamma_1\times|A|\,\gamma_0\times|A|\,\gamma_1\ra\Type) \\
    & \times && (A^\p && : \isPfPropd\,A^\sim)  \\
    & \times && (\RR_A && : (a_x:|A|\,\gamma_x)\ra A^\sim\,(\gamma_x, \gamma_x,\RR_\Gamma\,\gamma_x, a_x, a_x)) \\
    & \times && (\SS_A && : A^\sim\,(\gamma_0,\gamma_1,\gamma_{01},a_0,a_1)\ra A^\sim\,(\gamma_1,\gamma_0,\SS_\Gamma\,\gamma_{01},a_1,a_0)) \\
    & \times && (\TT_A && : A^\sim\,(\gamma_0,\gamma_1,\gamma_{01},a_0,a_1)\ra A^\sim\,(\gamma_1,\gamma_2,\gamma_{12},a_1,a_2)\ra A^\sim\,(\gamma_0,\gamma_2,\TT_\Gamma\,\gamma_{01}\,\gamma_{12},a_0,a_2)) \\
    & \times && (\coe_A && : \Gamma^\sim\,(\gamma_0,\gamma_1)\ra |A|\,\gamma_0\ra|A|\,\gamma_1) \\
    & \times && (\coh_A && : (\gamma_{01}:\Gamma^\sim\,(\gamma_0,\gamma_1))(a_0:|A|\,\gamma_0)\ra A^\sim\,(\gamma_0,\gamma_1,\gamma_{01},a_0,\coe_A\,\gamma_{01}\,a_0))
  \end{alignat*}
  Compared to the external version, we don't need substitution laws
  ($A^\sim[]$ and $\coe_A[]$) and instead of making the relation
  $\mathsf{Prop}$-valued we add an element of the identity type saying
  that $A^\sim$ is a point-free proposition.  We can prove that two
  types are equal if their $|\blank|$, $\blank^\sim$, $\blank^\p$,
  $\coe$ components are equal. The other components will be equal by
  $\blank^\p$. Unfortunately, due to Proposition
  \ref{prop:hpropPfProp} part (ii) (b), we have to show that the
  proofs of propositionalities $\blank^\p$ coincide.

  Substitution of types is given by function composition for the
  $|\blank|$ and $\blank^\sim$ components, for the $\blank^\p$
  component we use the fact that dependent point-free propositions are
  closed under reindexing. The reflexivity, symmetry and transitivity
  components of $A[\gamma]$ are constructed using transport and the
  corresponding components of $A$. The exact way they are constructed
  does not matter as they are proof irrelevant by $A^\p$. We prove the
  substitution laws $[{\circ}]$ and $[\id]$ up to the identity type
  using $\J$.

  Terms are like substitutions, but with dependent functions.
  \[
  \Tm\,\Gamma\,A :\equiv   (|t|  :(\gamma_x:|\Gamma|)\ra|A|\,\gamma_x) \times  (t^\sim  : (\gamma_{01}:\Gamma^\sim\,(\gamma_0,\gamma_1))\ra A^\sim\,(\gamma_0,\gamma_1,\gamma_{01},|t|\,\gamma_0,,|t|\,\gamma_1))
  \]
  The $|\blank|$ and $\blank^\sim$ components of context extension are
  given by $\Sigma$ types, the propositionality component is using the
  fact that point-free propositions are closed under $\Sigma$.

  Analogously to the model in the previous section, we can show that
  we have $\bot$, $\top$, $\Sigma$ and $\Pi$ types. The $\beta$ rules
  are definitional for both $\Sigma$ and $\Pi$, however for $\Pi$ the
  $\eta$ rule only holds up to the metatheoretic identity type. The
  reason is that $|\Pi\,A\,B|$ is defined as a $\Sigma$ type
  consisting of a function from $|A|$ to $|B|$ and a proof that it
  respects the relation.
  \begin{alignat*}{10}
    & |\Pi\,A\,B|\,\gamma_x :\equiv \big(f:(a_x:|A|\,\gamma_x)\ra|B|\,(\gamma_x,a_x)\big) \times \\
    & \hspace{2em} (a_{01}:A^\sim\,(\gamma_x,\gamma_x,\RR_\Gamma\,\gamma_x,a_0,a_1))\ra B^\sim\,((\gamma_x,a_0),(\gamma_x,a_1),(\RR_\Gamma\,\gamma_x,a_{01}),f\,a_0,f\,a_1)
  \end{alignat*}
  Two functions are related by $(\Pi\,A\,B)^\sim$ if they map related
  inputs to related outputs. Hence there are two (definitionally)
  different ways of proving that a $t : \Tm\,\Gamma\,(\Pi\,A\,B)$
  respects a (homogeneous) relation $a_{01}:
  A^\sim\,(\gamma_x,\gamma_x,\RR_\Gamma\,\gamma_x,a_0,a_1)$. One is
  $\pi_2\,(|t|\,\gamma_x)\,a_{01}$, the other is
  $t^\sim\,(\RR_\Gamma\,\gamma_x)\,a_{01}$. Because $B^\sim$ is a
  proposition, these are equal, but only up to the identity type. And
  the eta rule computes to the usage of the two different versions on
  the two sides of the equation. We do not prove the substitution laws
  $\bot[]$, $\top[]$, $\Sigma[]$, ${,}[]$, $\Pi[]$, $\lam[]$
  yet. There is no need to worry, we will prove them after replacing
  $\Ty$ with its strictified variant.

  If an equation is not definitional and there are later components in
  the model that depend on it (as $\lam[]$ depends on $\Pi[]$), it
  makes the model construction extremely tedious. The situation one
  ends up in is also known as ``transport hell''. As the functor laws
  $[{\circ}]$, $[\id]$ for types and terms are not definitional,
  almost every operation that mentions substitutions involves
  transports. Instead of fighting in transport hell and proving the
  transported versions of the laws $\bot[]$, \dots, $\lam[]$, we
  follow the local universes approach \cite{10.1145/2754931}. We wrap
  $\Ty$ into $\Ty'$ which contains a base context, a substitution into
  this context and a $\Ty$ in this base context.
  \[
  \Ty'\,\Gamma :\equiv (\con_A : \Con)\times(\sub_A : \Sub\,\Gamma\,\con_A)\times(\ty_A : \Ty\,\con_A)
  \]
  Substitution for $\Ty'$ is defined as composition in the $\sub$
  component, and as composition in the category is definitional, the
  laws $[{\circ}]$, $[\id]$ become definitional. Terms $\Tm'$ and
  context extension $\blank\rhd'\blank$ can be defined, and all the
  CwF equations are definitional. The type formers can be redefined as
  their primed versions $\bot'$, $\Sigma'$ and $\Pi'$. $\bot'[]$ and
  $\top'[]$ hold definitionally, but $\Sigma'[]$ and $\Pi'[]$ rely on
  definitional $\beta$ and $\eta$ for $\Sigma$ and $\Pi$ (the ones
  defined for $\Ty$), and we are missing an $\eta$ for $\Pi$. Hence
  $\Sigma[]$, ${{,}[]}$, $\Pi\eta$, $\Pi[]$, $\lam[]$ only hold up to
  the identity type.

  We define $\Ty\P\,\Gamma$ as those families over $|\Gamma|$ that are
  (point-free) propositional and which have coercion.
  \[
  \Ty\P\,\Gamma :\equiv (|A|:|\Gamma|\ra\Type)\times (A^\p: \isPfPropd\,|A|)\times(\coe_A : \Gamma^\sim\,(\gamma_0,\gamma_1)\ra|A|\,\gamma_0\ra|A|\,\gamma_1)
  \]
  $\uparrow$ is given by letting the relation be constant $\top$, and
  showing closure under $\top$, $\Sigma$ and $\Pi$ is
  straightforward. Proof irrelevance $\irr$ comes from the assumed
  equation $A^\p$, hence it is not definitional. Definition of the
  $\Ty\P$-valued identity type is analogous to the construction in the
  previous section. Strictification of $\Ty\P$ is analogous to that of
  $\Ty$.
\end{proof}

We conjecture that without strictification (the replacement of $\Ty$
by $\Ty'$) we can still prove all the equations, however this seems to
be very difficult due to ``transport hell''.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Examples of strict algebraic structures}
\label{sec:algebraic_structures}

Point-free equations can be used to define strict variants of
algebraic structures. For example, internally to a model of type
theory with a universe $\Type$ closed under $\Pi$, $\Sigma$, $\Id$, a
strict monoid is defined as follows.
\begin{alignat*}{10}
  & \mathsf{M} && : \Type \\
  & \blank\otimes\blank && : \mathsf{M}\ra \mathsf{M}\ra \mathsf{M} \\
  & \mathsf{ass} && : \Id_{\mathsf{M}\ra \mathsf{M}\ra \mathsf{M}\ra \mathsf{M}}\,(\lambda x\,y\,z.(x\otimes y)\otimes z)\,(\lambda x\,y\,z.x\otimes (y\otimes z)) \\
  & \mathsf{o} && : \mathsf{M} \\
  & \mathsf{idl} && : \Id_{\mathsf{M}\ra\mathsf{M}}\,(\lambda x.\mathsf{o}\otimes x)\,(\lambda x.x) \\
  & \mathsf{idr} && : \Id_{\mathsf{M}\ra\mathsf{M}}\,(\lambda x.x\otimes\mathsf{o})\,(\lambda x.x)
\end{alignat*}
Compare it with the usual definition of monoid where the laws are stated using universal quantification:
\begin{alignat*}{10}
  & \mathsf{ass} && : (x\,y\,z:\mathsf{M})\ra\Id_{\mathsf{M}}\,((x\otimes y)\otimes z)\,(x\otimes (y\otimes z)) \\
  & \mathsf{idl} && : (x:\mathsf{M})\ra\Id_{\mathsf{M}}\,(\mathsf{o}\otimes x)\,x \\
  & \mathsf{idr} && : (x:\mathsf{M})\ra\Id_{\mathsf{M}}\,(x\otimes\mathsf{o})\,x
\end{alignat*}
If our model has canonicity, then in the empty context, for any strict
monoid, the laws hold definitionally. For example, booleans where
conjunction is defined as $a \wedge b :\equiv \mathsf{if}\, a
\,\mathsf{then}\,b\,\mathsf{else}\,\false$ do not form a strict
monoid.  We do have $\mathsf{idl} : \true\wedge b \equiv b$, but we
don't have $\mathsf{idr}$ or associativity definitionally, only
propositionally. So booleans with $\blank{\wedge}\blank$ form a usual
monoid, but not a strict monoid. Similarly, natural numbers with
addition form a usual monoid, but not a strict monoid.

In contrast, for any type $A$, the function space $A\ra A$ forms a
monoid with $f\otimes g :\equiv \lambda x.f\,(g\,x)$ and
$\mathsf{o}:\equiv\lambda x.x$. We have associativity as $\lambda
f\,g\,h.(f\otimes g)\otimes g \equiv \lambda
f\,g\,h\,x.f\,(g\,(h\,x))\equiv \lambda f\,g\,h.f\otimes (g\otimes h)$
and the identity laws hold as e.g.\ $\lambda f.\mathsf{o}\otimes f \equiv
\lambda f\,x.f\,x \equiv \lambda f.f$.

Strict monoids are closed under finite products following the $\eta$
rule for $\times$. We can define displayed strict monoids over a
strict monoid, and dependent product of strict monoids. Strict monoids
are also closed by $A$-ary products for any type $A$. That is, given a
strict monoid with carrier $M$, $A\ra M$ is also a strict monoid.

Point-free propositions are another strict algebraic structure with no
operations and only one equation: any two elements are equal. Closure
under $\top$ and $\Sigma$ give closure under (dependent) finite
products, closure under $\Pi$ is the same as having $A$-ary
(dependent) products for any type $A$.

We conjecture that for any (generalised) algebraic structure, we have
a CwF with $\top$, $\Sigma$ and extensional $\Id$ of strict algebras
internally to any model of intensional type theory. The category part
of the CwF is the category of algebras and homomorphisms, terms and
types are displayed algebras and sections, context extension is
dependent product of algebras, and so on. This semantics was called
finite limit CwF in \cite{popl19}.

The term ``strict'' algebraic structure is only correct in intensional
type theory. In a model with function extensionality, strict and usual
monoids coincide.

There is a stronger sense in which algebraic structures can be
``strict''. Obviously, to define a strict monoid in the empty context,
all laws have to hold definitionally. However when \emph{assuming} a
strict monoid and using it in a construction in this open context, the
laws only hold up to propositional equality. It would be convenient to
have implementations of type theory with strict algebraic structures
in this stronger sense. Currently, Agda only supports one algebraic
structure which is strict in this stronger sense: propositions.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Summary}
\label{sec:summary}

In this paper we attempted to push the limits of what can be done in
intensional type theory without function extensionality or uniqueness
of identity proofs. We exploited the fact that in intensional type
theory, in the empty context propositional and definitional equality
coincide. We used this to define a dynamic universe of strict
propositions internally. We expect that other strict algebraic
structures with the expected properties can be defined along the same
lines. In a strict algebraic structure, all equations are
definitional. As we cannot assume definitional equalities in type
theory, when we assume a member of a strict algebraic structure, the
equations only hold propositionally. This makes it difficult to use
such algebraic structures in practice. However we think that model
constructions of type theory can be formalised as functions between
strict models. We conjecture that the canonicity and normalisation
displayed models from the corresponding proofs for type theory
\cite{DBLP:journals/tcs/Coquand19,lmcs:4005} can be formalised in pure
intensional type theory. These would be displayed over a strict model
defined as a point-free algebraic structure. There are other inherent
limitations of point-free propositions, e.g.\ the fact that we cannot
prove that being a point-free proposition is a point-free proposition.

Internal strict models can be externalised directly. We would like to
understand in which circumstances internal non-strict models can be
externalised into model constructions. Another open problem is whether
$\isHProp\,(\isPfProp\,A)$ is provable in intensional type theory.

A strict proposition-valued identity type with a strong transport rule
was used to define presheaves \cite{DBLP:conf/lics/Pedrot20} and a
universe of setoids closed under dependent function space
\cite{DBLP:conf/fossacs/AltenkirchBKSS21}. It is not clear whether
such a type theory has normalisation
\cite{DBLP:journals/lmcs/AbelC20}. Currently the only justification
that we know for this strong transport rule is the setoid model
construction. We showed that such an identity type can be derived in
intensional type theory using point-free propositions. It seems that
our construction is limited, the model we constructed does not include
a universe of propositions or inductive types. In the future, we would
like to circumscribe the exact conditions that the input model has to
satisfy in order to obtain inductive types and universes from the
setoid model construction.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\bibliography{b}

\end{document}
