\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}