Advances report, reordered some equations
This commit is contained in:
parent
e9eedbff2d
commit
2956b62cc1
GPG Key ID:
7054D5D6A90F084F
@ -213,6 +213,20 @@ module FFOLInitial where
|
||||
p∀∀i : {A : For (Γₜ ▹t⁰)} → Pf (Γₜ ▹t⁰) (Γₚ ▹tp) A → Pf Γₜ Γₚ (∀∀ A)
|
||||
|
||||
|
||||
-- The action on Cont's morphisms of Pf functor
|
||||
_[_]pvₜ : {A : For Δₜ}→ PfVar Δₜ Δₚ A → (σ : Subt Γₜ Δₜ)→ PfVar Γₜ (Δₚ [ σ ]c) (A [ σ ]f)
|
||||
pvzero [ σ ]pvₜ = pvzero
|
||||
pvnext pv [ σ ]pvₜ = pvnext (pv [ σ ]pvₜ)
|
||||
_[_]pₜ : {A : For Δₜ} → Pf Δₜ Δₚ A → (σ : Subt Γₜ Δₜ) → Pf Γₜ (Δₚ [ σ ]c) (A [ σ ]f)
|
||||
var pv [ σ ]pₜ = var (pv [ σ ]pvₜ)
|
||||
app pf pf' [ σ ]pₜ = app (pf [ σ ]pₜ) (pf' [ σ ]pₜ)
|
||||
lam pf [ σ ]pₜ = lam (pf [ σ ]pₜ)
|
||||
_[_]pₜ {Δₚ = Δₚ} {Γₜ = Γₜ} (p∀∀e {A = A} {t = t} pf) σ =
|
||||
substP (λ F → Pf Γₜ (Δₚ [ σ ]c) F) (≡tran² (≡sym []f-∘) (cong (λ σ → A [ σ ]f)
|
||||
(cong₂ _,ₜ_ (≡tran² wkₜ∘ₜ,ₜ idrₜ (≡sym idlₜ)) refl)) ([]f-∘))
|
||||
(p∀∀e {t = t [ σ ]t} (pf [ σ ]pₜ))
|
||||
_[_]pₜ {Γₜ = Γₜ} (p∀∀i pf) σ
|
||||
= p∀∀i (substP (λ Ξₚ → Pf (Γₜ ▹t⁰) (Ξₚ) _) ▹tp-lfₜ (pf [ lfₜσₜ σ ]pₜ))
|
||||
|
||||
|
||||
|
||||
@ -266,6 +280,12 @@ module FFOLInitial where
|
||||
data Subp : {Δₜ : Cont} → Conp Δₜ → Conp Δₜ → Set₁ where
|
||||
εₚ : Subp Δₚ ◇p
|
||||
_,ₚ_ : {A : For Δₜ} → (σ : Subp Δₚ Δₚ') → Pf Δₜ Δₚ A → Subp Δₚ (Δₚ' ▹p⁰ A)
|
||||
|
||||
-- The action of Cont's morphisms on Subp
|
||||
_[_]σₚ : Subp {Δₜ} Δₚ Δₚ' → (σ : Subt Γₜ Δₜ) → Subp {Γₜ} (Δₚ [ σ ]c) (Δₚ' [ σ ]c)
|
||||
εₚ [ σₜ ]σₚ = εₚ
|
||||
(σₚ ,ₚ pf) [ σₜ ]σₚ = (σₚ [ σₜ ]σₚ) ,ₚ (pf [ σₜ ]pₜ)
|
||||
|
||||
-- They are indeed stronger than renamings
|
||||
Ren→Sub : Ren Δₚ Δₚ' → Subp {Δₜ} Δₚ' Δₚ
|
||||
Ren→Sub zeroRen = εₚ
|
||||
@ -289,19 +309,7 @@ module FFOLInitial where
|
||||
|
||||
|
||||
|
||||
_[_]pvₜ : {A : For Δₜ} → PfVar Δₜ Δₚ A → (σ : Subt Γₜ Δₜ) → PfVar Γₜ (Δₚ [ σ ]c) (A [ σ ]f)
|
||||
pvzero [ σ ]pvₜ = pvzero
|
||||
pvnext pv [ σ ]pvₜ = pvnext (pv [ σ ]pvₜ)
|
||||
_[_]pₜ : {A : For Δₜ} → Pf Δₜ Δₚ A → (σ : Subt Γₜ Δₜ) → Pf Γₜ (Δₚ [ σ ]c) (A [ σ ]f)
|
||||
var pv [ σ ]pₜ = var (pv [ σ ]pvₜ)
|
||||
app pf pf' [ σ ]pₜ = app (pf [ σ ]pₜ) (pf' [ σ ]pₜ)
|
||||
lam pf [ σ ]pₜ = lam (pf [ σ ]pₜ)
|
||||
_[_]pₜ {Δₚ = Δₚ} {Γₜ = Γₜ} (p∀∀e {A = A} {t = t} pf) σ = substP (λ F → Pf Γₜ (Δₚ [ σ ]c) F) (≡tran² (≡sym []f-∘) (cong (λ σ → A [ σ ]f) (cong₂ _,ₜ_ (≡tran² wkₜ∘ₜ,ₜ idrₜ (≡sym idlₜ)) refl)) ([]f-∘)) (p∀∀e {t = t [ σ ]t} (pf [ σ ]pₜ))
|
||||
_[_]pₜ {Γₜ = Γₜ} (p∀∀i pf) σ = p∀∀i (substP (λ Ξₚ → Pf (Γₜ ▹t⁰) (Ξₚ) _) ▹tp-lfₜ (pf [ lfₜσₜ σ ]pₜ))
|
||||
|
||||
_[_]σₚ : Subp {Δₜ} Δₚ Δₚ' → (σ : Subt Γₜ Δₜ) → Subp {Γₜ} (Δₚ [ σ ]c) (Δₚ' [ σ ]c)
|
||||
εₚ [ σₜ ]σₚ = εₚ
|
||||
(σₚ ,ₚ pf) [ σₜ ]σₚ = (σₚ [ σₜ ]σₚ) ,ₚ (pf [ σₜ ]pₜ)
|
||||
|
||||
wkₜσₚ : Subp {Δₜ} Δₚ' Δₚ → Subp {Δₜ ▹t⁰} (Δₚ' ▹tp) (Δₚ ▹tp)
|
||||
wkₜσₚ εₚ = εₚ
|
||||
|
||||
6
Makefile
6
Makefile
@ -18,7 +18,7 @@ agda-tex-FIni: latex/FFOLInitial.tex
|
||||
mkdir -p report/agda
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/ICont.tex,'Term\\ contexts\\ are\\ isomorphic\\ to\\ Nat','\\>\[0\]\\<')
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/ITm.tex,'A\\ term\\ variable\\ is\\ a\\ de-bruijn','\\>\[0\]\\<')
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/IFor.tex,'Now\\ we\\ can\\ define\\ formul','\\>\[0\]\\<')
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/IFor.tex,'Now\\ we\\ can\\ define\\ formul','\\AgdaEmptyExtraSkip')
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/ISubt.tex,'Then\\ we\\ define\\ term\\ substitutions','\\>\[0\]\\<')
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/ISubtT.tex,'We\\ now\\ define\\ the\\ action\\ of\\ term\\ substitutions','\\>\[0\]\\<')
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/ISubtF.tex,'We\\ can\\ now\\ subst\\ on\\ formul','\\AgdaEmptyExtraSkip')
|
||||
@ -31,11 +31,11 @@ agda-tex-FIni: latex/FFOLInitial.tex
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/ISubp.tex,'But\\ we\\ need\\ something\\ stronger\\ than\\ just\\ renamings','They\\ are\\ indeed\\ stronger\\ than\\ renamings')
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/ISubtP.tex,'\\>\[2\]\\AgdaOperator{\\AgdaFunction{\\AgdaUnderscore{}\[\\AgdaUnderscore{}\]pv','\\>\[0\]\\<')
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/ISubtS.tex,'\\>\[2\]\\AgdaOperator{\\AgdaFunction{\\AgdaUnderscore{}\[\\AgdaUnderscore{}\]σ','\\AgdaEmptyExtraSkip')
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/ISubpP.tex,'\\>\[2\]\\AgdaOperator{\\AgdaFunction{\\AgdaUnderscore{}\[\\AgdaUnderscore{}\]p}}','\\>\[0\]\\<')
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/ISubpP.tex,'\\>\[2\]\\AgdaOperator{\\AgdaFunction{\\AgdaUnderscore{}\[\\AgdaUnderscore{}\]p}}','\\AgdaEmptyExtraSkip')
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/IIdCompP.tex,'We\\ can\\ now\\ define\\ identity\\ and\\ composition\\ on\\ proof\\ substitutions','\\AgdaEmptyExtraSkip')
|
||||
@cat latex/FFOLInitial.tex | grep -A5000 -m1 'We\\ can\\ now\\ merge\\ the\\ two\\ notions\\ of\\ contexts,\\ substitutions,\\ and\\ everything' | grep -B5000 -m1 '\\>\[0\]\\<' > report/agda/ICon.tex
|
||||
@cat latex/FFOLInitial.tex | grep -A5000 -B1 -m1 '\\AgdaRecord{Sub}\\AgdaSpace{}%' | grep -B5000 -m1 '\\AgdaEmptyExtraSkip' > report/agda/ISub.tex
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/IIdComp.tex,'(Con,Sub)\\ is\\ a\\ category\\ with\\ an\\ initial\\ object','\\>\[2\]\\AgdaOperator{\\AgdaFunction{\\AgdaUnderscore{}')
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/IIdComp.tex,'(Con,Sub)\\ is\\ a\\ category\\ with\\ an\\ initial\\ object','\\>\[2\]\\AgdaFunction{idl}\\AgdaSpace{}')
|
||||
@$(call extract,latex/FFOLInitial.tex,report/agda/ICExt.tex,'We\\ have\\ our\\ two\\ context\\ extension\\ operators','\\AgdaEmptyExtraSkip')
|
||||
|
||||
agda-tex-FFOL: latex/FFOL.tex
|
||||
|
||||
@ -35,12 +35,19 @@
|
||||
\subsection{Motivation}
|
||||
\subsection{Structure of this report}
|
||||
\section{A first account of Completeness and Normalization}
|
||||
\subsection{Normalization for ZOL}
|
||||
\subsection{Normalization for IFOL}
|
||||
\subsection{Normalization for Propositional Logic}
|
||||
\subsection{Normalization for Infinitary First Order Logic}
|
||||
\subsection{Merging the two proofs}
|
||||
\section{Predicate Logic}
|
||||
\subsection{SOGAT Presentation of FFOL}
|
||||
\subsection{SOGAT Presentation of Predicate Logic}
|
||||
|
||||
In order to find all the definitions, functions and more importantly, all the equations that a model of Predicate Logic has to verify, Ambrus gave me a Second Order Generalized Algebraic Theory (SOGAT) of the models. It goes as described in \autoref{fig:ffol-sogat}.
|
||||
|
||||
Why is this definition \enquote{Second Order} ? That's because some definitions are not strictly positive. These are the definitions of $\lam$ and $\foralli$. This SOGAT definition makes sense because of the ${}^+$ in $\Tm$ and $\Pf$ definitions, that indicates that those two objects should be \emph{locally representable}. It means that one can use \emph{term variables} and \emph{proof variables}.
|
||||
|
||||
We can notice that there is no equations in this SOGAT.
|
||||
|
||||
\begin{figure}
|
||||
\begin{tcolorbox}
|
||||
\[
|
||||
\begin{array}{lcl}
|
||||
@ -52,146 +59,248 @@
|
||||
\R & : & \Tm \rightarrow \Tm \rightarrow \For\\
|
||||
\\
|
||||
\Pf & : & \For \rightarrow \Prop^+ \\
|
||||
\lam & : & (\Pf A \rightarrow \Pf B) \rightarrow \Pf (A \implies B)\\
|
||||
\lam & : & (\Pf A \rightarrow^+ \Pf B) \rightarrow \Pf (A \implies B)\\
|
||||
\app & : & \Pf (A \implies B) \rightarrow (\Pf A \rightarrow \Pf B)\\
|
||||
\foralli & : & (t : \Tm \rightarrow^+ A\;t) \rightarrow \Pf (\forall A)\\
|
||||
\foralle & : & \Pf (\forall A) \rightarrow (t : \Tm) \rightarrow \Pf (A\;t)\\
|
||||
\end{array}
|
||||
\]
|
||||
\end{tcolorbox}
|
||||
\caption{FFOL Sogat Presentation}
|
||||
\label{fig:ffol-sogat}
|
||||
\end{figure}
|
||||
|
||||
\subsection{Turning a SOGAT Presentation into a GAT}
|
||||
|
||||
But now, we want to encode in Agda a Sogat Algebra, which we can't do (for now), as Agda can only understand simple Generalized Algebraic Theories (or GAT).
|
||||
|
||||
In order to break this apparent strict positivity, we will translate every object of the SOGAT into a functor from a context category called $\bCon$. This context category shall have an initial object and two endo-mappings called \emph{context extensions}. They can be understood as adding to a context a proof variable or a term variable. We will also call \emph{substitutions} morphisms from the $\bCon$ category, and for a morphism $\sigma$ and a functor $F$, we will denote $\_\left[\sigma\right]$ the action of the functor on the morphism $\sigma$.
|
||||
|
||||
We will first define this category, its initial object, and every rule that these components should obey.
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/Con.tex}
|
||||
\vspace{-7.5ex}
|
||||
\end{tcolorbox}
|
||||
|
||||
|
||||
We can now define terms, formulæ and proofs, which are functors from $\bCon$ to $\bSet$ (and proofs are a more complex functor from $\bCon$ to XXXXX). For each of them, we define the action of the functors on morphisms, and we also write the equalities that describe the functionality.
|
||||
|
||||
\def\agdasep{\vspace{-10.5ex}\begin{center}\rule{0.9\linewidth}{0.4pt}\end{center}\vspace{-3.5ex}}
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/Tm.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agda{agda/Tm+.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agdasep
|
||||
\agda{agda/For.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agdasep
|
||||
\agda{agda/Pf.tex}
|
||||
\vspace{-7.5ex}
|
||||
\end{tcolorbox}
|
||||
|
||||
|
||||
Then we define our context extensions. We also have constructors for substitutions to extended contexts. This constructor should work as a product, which means that we have two \enquote{projections} that can revert the mapping. The constructor should finally be consistent with $\circ$.
|
||||
|
||||
Please ignore the \verb*|substP| for now, this notion will be explained in \autoref{sec:transport-hell}.
|
||||
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/Tm+.tex}
|
||||
\vspace{-7.5ex}
|
||||
\end{tcolorbox}
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/Pf+.tex}
|
||||
\vspace{-7.5ex}
|
||||
\end{tcolorbox}
|
||||
|
||||
Finally, with those context extensions, we can define our operators on functions and proofs. Those operators have to commute with the images of substitutions (the equations are unneeded for proof operators, as they are in prop).
|
||||
|
||||
We can take a closer look at where our apparently strictly positive application should be ($\lam$ and $\foralli$). We can see that instead of an application, we only have a formula (or a proof) that goes from an extended context to a base contexts. This \enquote{removal} of the term variable stands for the strictly positive function that would have taken a term/proof as a parameter.
|
||||
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/R.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agdasep
|
||||
\agda{agda/Imp.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agdasep
|
||||
\agda{agda/Forall.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agdasep
|
||||
\agda{agda/LamApp.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agdasep
|
||||
\agda{agda/ForallR.tex}
|
||||
\vspace{-7.5ex}
|
||||
\end{tcolorbox}
|
||||
|
||||
We now have a generalized algebraic theory that describes all the models of Predicate logic. A model is indeed an implementation of the agda record described above.
|
||||
|
||||
\section{Implementing the Syntax}
|
||||
|
||||
We will now try de define a strict syntax for that model. This means that we want to define \enquote{physically} a model that will be as tiny as possible.
|
||||
|
||||
\subsection{Separated Contexts}
|
||||
|
||||
A first intuition to help us construct this syntax is that we can split the $\bCon$ category in two. A first part will be related to term-extensions and the second part will be related to proof-extensions.
|
||||
|
||||
One difficulty is that those two parts are not intependent. Indeed, a proof-extension related context (or \emph{proof context}) will depend on formulæ, that will depend on term-extension related contexts (or \emph{term contexts}).
|
||||
|
||||
So, we first define the term contexts, which simply describes how many terms they are in the context (therefore, it is isomorphic to Nat).
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/ICont.tex}
|
||||
\vspace{-7.5ex}
|
||||
\end{tcolorbox}
|
||||
|
||||
Then, we can define terms (which can only be term variables in our simplified version), and formulæ (with only one binary relation). They are both indexed only on a term context, and we will need make them $\bCon \rightarrow \bSet$ rather than $\textbf{Cont} \rightarrow \bSet$. But this will be only a trivial extraction of the $\textbf{Cont}$ inside the $\bCon$, as we can notice that the terms and formulæ defined by a context doesn't depend on the proof variables available. We simply give the constructors described in the algebra.
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agda{agda/IFor.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agda{agda/ISubt.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/ITm.tex}
|
||||
\agdasep
|
||||
\agda{agda/IFor.tex}
|
||||
\vspace{-7.5ex}
|
||||
\end{tcolorbox}
|
||||
|
||||
We now can define term substitutions. The algebra gives us two ways of constructing them: with $,_t$ and as a morphism from the initial object. That's how we make our constructor The two projections $\pi_t^1$ and $\pi_t^2$ are then simply obtained by destroying the $,_t$ constructor and getting the first or second term. The equalities between $\pi_t¹$, $\pi_t²$ and $,_t$ can be proven easily in that layout.
|
||||
|
||||
We also have to define the action of term substitutions on terms and formulæ. The definitions are really natural, as we just go down the formulæ to get to the term variables and transform them into the terms specified in the substitution.
|
||||
|
||||
We also define the categorical constructors for the $\textbf{Cont}$ category, that is, the $id_t$ and $\circ_t$ operators, and we obviously have to show their three categorical laws.
|
||||
|
||||
We finally have to show the functorality of $\_\left[\_\right]\!t$ and $\_\left[\_\right]\!f$ i.e. that they do nothing on identity and that applying two substitutions one after the other is like applying their composition.
|
||||
|
||||
You can see we use some helper functions that are called $\operatorname{wk}_t$ and $\operatorname{lf}_t$. Those stands for weakening and lifting. I don't show their definitions here, because they are only helper functions, but $\operatorname{wk}_t$ means that from something going from a context $\Gamma$, we create something going from the context $\Gamma \triangleright_t$ that does not uses the added variable. $\operatorname{lf}_t$ means that we add one variable in the source, one variable in the goal, and that this variable is mapped to itself.
|
||||
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/ISubt.tex}
|
||||
\agdasep
|
||||
\agda{agda/ISubtT.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agdasep
|
||||
\agda{agda/ISubTF.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agdasep
|
||||
\agda{agda/IIdCompT.tex}
|
||||
\vspace{-7.5ex}
|
||||
\end{tcolorbox}
|
||||
|
||||
We can now start creating the other category. For that, we can define the base set of the category like we did with term contexts. But this time, our extension constructor has another parameter: The formula the added proof proves. Therefore, we have a dependency of $\operatorname{Conp}$ on $\operatorname{Cont}$, because formula is defined in conp.
|
||||
|
||||
This new $\textbf{Conp}$ category is in fact a functor from $\textbf{Cont}$ to $\bSet$. So we have to define its action on $\textbf{Cont}$'s morphisms. And we also have to proove that this action respects the functorality of $\operatorname{Conp}$.
|
||||
|
||||
We will finally create another operator on $\textbf{Conp}$: $\triangleright tp$. This operator does a term extension of a proof context, which doesn't add any information to the proofs, it only adds one unused variable to them (we substitute all the proofs with $\operatorname{wk}_t \operatorname{id}_t$). It can be understood as the action of the general $\triangleright_t$ functor on $\textbf{Conp}$.
|
||||
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/IConp.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agdasep
|
||||
\agda{agda/ISubtC.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agdasep
|
||||
\agda{agda/IConpTp.tex}
|
||||
\vspace{-7.5ex}
|
||||
\end{tcolorbox}
|
||||
|
||||
We now have everything we need to define proofs. As we are in the syntax, the only constructors for proofs will be those defined in the algebra, plus proof variables. These definitions are pretty straightforward as they are directly induced from the algebra. You can notice that we have separated term and proof contexts in the definitions, but it is only for the sake of readability, because operations on proofs will often modify the proof context without changing the term context.
|
||||
|
||||
We also define the action of term-substitutions on proofs (because Pf is a functor that is indexed by $\textbf{Cont}$). Terms substitutions does nothing to the proofs, they only affect formulæ and terms, which you cannot find inside a proof. So it is only changing the type of a proof from $\Pf Δ_t\;Δ_p\;A$ to $\Pf Γ_t\;Δ_p[σ]\; A[σ]$.
|
||||
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/IPf.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agda{agda/IRen.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agda{agda/ISubp.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agdasep
|
||||
\agda{agda/ISubtP.tex}
|
||||
\vspace{-7.5ex}
|
||||
\end{tcolorbox}
|
||||
|
||||
Before we can define proof substitutions, we need to define a weaker version of them, that are called \emph{renamings}. A renaming from a proof context $Γ_p$ to a proof context $Δ_p$ that have the same term-context, is a way of re-ordering, duplicating or deleting the proofs contained inside of $Δ_p$. If we were to understand proof contexts as list of formulæ, then a renaming from $Γ_p$ to $Δ_p$ would be a witness that each formula in $Δ_p$ is contained at least one time in $Γ_p$. That's why we use $\operatorname{PfVar}$, as $\operatorname{PfVar} Γ_t Γ_p A$ is a witness that proof-context $Γ_p$ contains the formula $A$.
|
||||
|
||||
For these renamings, we make some constructors, for example the identity renaming, or the weakening of a renaming. We will finally make a operator that weakens a proof in $Γ_p$ with a renaming from $Γ_p$ to $Δ_p$ into a proof in $Δ_p$.
|
||||
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/IRen.tex}
|
||||
\vspace{-7.5ex}
|
||||
\end{tcolorbox}
|
||||
|
||||
Now, we are defining a complete proof substitution, that can also be understood as a list a proofs of the formulæ described in the goal proof-context.
|
||||
|
||||
We can notice that those proof substitutions works with a fixed term-context. So they are weaker than the final substitutions we well have to define for our algebra, that have to be able to be morphisms between contexts that can differ on term-contexts and proof context at the same time. But this is not an issue and we can define all substitutions using only those restricted proof-substitutions.
|
||||
|
||||
Again, these substitutions are a functor over the category $\textbf{Cont}$, so we have to construct the action on morphisms, which is simply applying the transformations to all the proofs contained in the substitution.
|
||||
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/ISubp.tex}
|
||||
\agdasep
|
||||
\agda{agda/ISubtS.tex}
|
||||
\vspace{-7.5ex}
|
||||
\end{tcolorbox}
|
||||
|
||||
With this new kind of substitution, we can substitute on proofs (that's what they're for). In other words, we have to describe the action of the $\Pf$ functor on the morphisms of the category $\textbf{Conp}$.
|
||||
|
||||
Proof substitution of proofs is simple to define, as we only get down the proof until we find a proof variable, in which case we replace it with the proof in the substitution, like we did for term-substitutions and formulæ.
|
||||
|
||||
Again, we have defined $\operatorname{wk}_p$ and $\operatorname{lf}_p$. The former will add an unused proof variable (an assumption) in a substitution, and the latter adds a formula in the goal which is proven using an assumption.
|
||||
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/ISubpP.tex}
|
||||
\vspace{-7.5ex}
|
||||
\end{tcolorbox}
|
||||
|
||||
This definition of proof substitutions allows us to define the categorical operators for proof substitutions.
|
||||
|
||||
Of course, we have to show that the categorical laws apply to them, that $\_[\_]\sigma_p$ respects them, as we did for the Subt's laws.
|
||||
|
||||
The proofs of these laws contains a lot of transports, which will be described more precisely in \autoref{sec:transport-hell}.
|
||||
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/IIdCompP.tex}
|
||||
\vspace{-7.5ex}
|
||||
\end{tcolorbox}
|
||||
|
||||
The last step is to merge our two kinds of contexts and substitutions in order to match the algebra.
|
||||
|
||||
For contexts, we simply have a record type. But for substitutions, we defined Subp to only describe substitutions between Conp{\footnotesize s} with \emph{the same Conp}. Our solution is to understand global substitutions as a sequence of substitutions, first on terms, and then on proofs. That's why the \enquote{proof} part of the substitution can only be applyed to proofs on $\Delta_p [t]p$, i.e. proofs that have already been term-substituted by the \enquote{term} part of the substitution. The definition of the algebra's substitution is given after, and you can see that substitutions works exactly as described, first, the proof and everything inside is substituted using the \enquote{term} part of the substitution, and only after that the \enquote{proof} part of the substitution is applied.
|
||||
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/ICon.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agdasep
|
||||
\agda{agda/ISub.tex}
|
||||
\vspace{-13.5ex}
|
||||
\begin{center}\rule{0.9\linewidth}{0.4pt}\end{center}
|
||||
\vspace{-3ex}
|
||||
\begin{code}
|
||||
\>[4]\AgdaOperator{\AgdaField{\AgdaUnderscore{}[\AgdaUnderscore{}]p}}\AgdaSpace{}%
|
||||
\AgdaSymbol{=}\AgdaSpace{}%
|
||||
\AgdaSymbol{λ}\AgdaSpace{}%
|
||||
\AgdaBound{pf}\AgdaSpace{}%
|
||||
\AgdaBound{σ}\AgdaSpace{}%
|
||||
\AgdaSymbol{→}\AgdaSpace{}%
|
||||
\AgdaSymbol{(}\AgdaBound{pf}\AgdaSpace{}%
|
||||
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
|
||||
\AgdaField{Sub.t}\AgdaSpace{}%
|
||||
\AgdaBound{σ}\AgdaSpace{}%
|
||||
\AgdaOperator{\AgdaFunction{]pₜ}}\AgdaSymbol{)}\AgdaSpace{}%
|
||||
\AgdaOperator{\AgdaFunction{[}}\AgdaSpace{}%
|
||||
\AgdaField{Sub.p}\AgdaSpace{}%
|
||||
\AgdaBound{σ}\AgdaSpace{}%
|
||||
\AgdaOperator{\AgdaFunction{]p}}\<%
|
||||
\end{code}
|
||||
\vspace{-5ex}
|
||||
\end{tcolorbox}
|
||||
|
||||
And we can finally define our categorical operators for the merged version. They are only concatenation of the previously defined operators, so no hard logic here. Those constructions are obviously followed by equations needed for the algebra.
|
||||
|
||||
\begin{tcolorbox}
|
||||
\vspace{-2ex}
|
||||
\agda{agda/IIdComp.tex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\begin{tcolorbox}
|
||||
\agdasep
|
||||
\agda{agda/ICExt.tex}
|
||||
\vspace{-7.5ex}
|
||||
\end{tcolorbox}
|
||||
|
||||
\subsection{Transport Hell}
|
||||
|
||||
\label{sec:transport-hell}
|
||||
|
||||
\section{Summary}
|
||||
|
||||
|
||||
@ -101,6 +101,9 @@
|
||||
\newcommand\foralli{\operatorname{\operatorname{\forall i}}}
|
||||
\newcommand\foralle{\operatorname{\operatorname{\forall e}}}
|
||||
\newcommand\Pf{\operatorname{Pf}\;}
|
||||
\newcommand\bCon{\textbf{Con}}
|
||||
\newcommand\bSet{\textbf{Set}}
|
||||
\newcommand\bProp{\textbf{Prop}}
|
||||
|
||||
% Agda Config
|
||||
\usepackage{agda}
|
||||
@ -108,6 +111,9 @@
|
||||
\newunicodechar{∘}{\ensuremath{\mathnormal{\circ}}}
|
||||
\newunicodechar{≡}{\ensuremath{\mathnormal{\equiv}}}
|
||||
\newunicodechar{◇}{\ensuremath{\mathnormal{\diamond}}}
|
||||
\newunicodechar{Γ}{\ensuremath{\mathnormal{\Gamma}}}
|
||||
\newunicodechar{Δ}{\ensuremath{\mathnormal{\Delta}}}
|
||||
\newunicodechar{Ξ}{\ensuremath{\mathnormal{\Xi}}}
|
||||
\newunicodechar{α}{\ensuremath{\mathnormal{\alpha}}}
|
||||
\newunicodechar{β}{\ensuremath{\mathnormal{\beta}}}
|
||||
\newunicodechar{γ}{\ensuremath{\mathnormal{\gamma}}}
|
||||
@ -115,6 +121,7 @@
|
||||
\newunicodechar{ε}{\ensuremath{\mathnormal{\varepsilon}}}
|
||||
\newunicodechar{σ}{\ensuremath{\mathnormal{\sigma}}}
|
||||
\newunicodechar{π}{\ensuremath{\mathnormal{\pi}}}
|
||||
\newunicodechar{λ}{\ensuremath{\mathnormal{\lambda}}}
|
||||
\newunicodechar{▹}{\ensuremath{\mathnormal{\triangleright}}}
|
||||
\newunicodechar{⊢}{\ensuremath{\mathnormal{\vdash}}}
|
||||
\newunicodechar{⇒}{\ensuremath{\mathnormal{\Rightarrow}}}
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user