From f4ae6c990f1aee5ae56073dd74c9db7634b7bff5 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 25 Apr 2022 21:47:57 -0400 Subject: [PATCH] hopefully these are the last purely cosmetic changes to the code --- doc/TYPES2021/Demos/HSP.tex | 475 ++++++++++++++++++------------------ src/Demos/HSP.lagda | 118 +++++---- 2 files changed, 300 insertions(+), 293 deletions(-) diff --git a/doc/TYPES2021/Demos/HSP.tex b/doc/TYPES2021/Demos/HSP.tex index b51426ff..3001007b 100644 --- a/doc/TYPES2021/Demos/HSP.tex +++ b/doc/TYPES2021/Demos/HSP.tex @@ -6165,8 +6165,7 @@ \subsection{Terms} \AgdaSymbol{:}\AgdaSpace{}% \AgdaRecord{Algebra}\AgdaSpace{}% \AgdaGeneralizable{α}\AgdaSpace{}% -\AgdaGeneralizable{ρᵃ}\AgdaSymbol{\}}% -\>[41]\AgdaSymbol{\{}\AgdaBound{𝑩}\AgdaSpace{}% +\AgdaGeneralizable{ρᵃ}\AgdaSymbol{\}\{}\AgdaBound{𝑩}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaRecord{Algebra}\AgdaSpace{}% \AgdaGeneralizable{β}\AgdaSpace{}% @@ -6180,36 +6179,37 @@ \subsection{Terms} \>[0][@{}l@{\AgdaIndent{0}}]% \>[1]\AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{Environment}\AgdaSpace{}% -\AgdaBound{𝑨}\AgdaSpace{}% -\AgdaKeyword{using}\AgdaSpace{}% +\AgdaBound{𝑨}% +\>[21]\AgdaKeyword{using}\AgdaSpace{}% \AgdaSymbol{(}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧}}\AgdaSpace{}% -\AgdaSymbol{)}% -\>[35]\AgdaSymbol{;}% -\>[41]\AgdaKeyword{open}\AgdaSpace{}% +\AgdaSymbol{)}\<% +\\ +% +\>[1]\AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{Environment}\AgdaSpace{}% -\AgdaBound{𝑩}\AgdaSpace{}% +\AgdaBound{𝑩}% +\>[21]\AgdaKeyword{using}\AgdaSpace{}% +\AgdaSymbol{()}\AgdaSpace{}% \AgdaKeyword{renaming}\AgdaSpace{}% \AgdaSymbol{(}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧}}\AgdaSpace{}% \AgdaSymbol{to}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧ᴮ}}\AgdaSpace{}% -\AgdaSymbol{)}% -\>[86]\AgdaKeyword{using}\AgdaSpace{}% -\AgdaSymbol{()}\<% +\AgdaSymbol{)}\<% \\ % \>[1]\AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{Setoid}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% \AgdaBound{𝑩}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{]}}\AgdaSpace{}% -\AgdaKeyword{using}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{]}}% +\>[21]\AgdaKeyword{using}\AgdaSpace{}% \AgdaSymbol{(}\AgdaSpace{}% \AgdaOperator{\AgdaField{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSpace{}% \AgdaSymbol{;}\AgdaSpace{}% \AgdaFunction{refl}% -\>[40]\AgdaSymbol{)}\<% +\>[41]\AgdaSymbol{)}\<% \\ % \>[1]\AgdaKeyword{private}\AgdaSpace{}% @@ -6225,6 +6225,8 @@ \subsection{Terms} \AgdaFunction{hfunc}\<% \\ % +\\[\AgdaEmptyExtraSkip]% +% \>[1]\AgdaFunction{comm-hom-term}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaSymbol{(}\AgdaBound{t}\AgdaSpace{}% @@ -6258,28 +6260,30 @@ \subsection{Terms} \>[1]\AgdaFunction{comm-hom-term}\AgdaSpace{}% \AgdaSymbol{(}\AgdaInductiveConstructor{ℊ}\AgdaSpace{}% \AgdaBound{x}\AgdaSymbol{)}\AgdaSpace{}% -\AgdaBound{a}% -\>[29]\AgdaSymbol{=}% -\>[35]\AgdaFunction{refl}\<% +\AgdaBound{a}\AgdaSpace{}% +\AgdaSymbol{=}\AgdaSpace{}% +\AgdaFunction{refl}\<% \\ % \>[1]\AgdaFunction{comm-hom-term}\AgdaSpace{}% \AgdaSymbol{(}\AgdaInductiveConstructor{node}\AgdaSpace{}% \AgdaBound{f}\AgdaSpace{}% \AgdaBound{t}\AgdaSymbol{)}\AgdaSpace{}% -\AgdaBound{a}% -\>[29]\AgdaSymbol{=}% -\>[35]\AgdaOperator{\AgdaFunction{begin}}\<% +\AgdaBound{a}\AgdaSpace{}% +\AgdaSymbol{=}\<% \\ \>[1][@{}l@{\AgdaIndent{0}}]% -\>[2]\AgdaFunction{h}\AgdaSymbol{(}\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% +\>[2]\AgdaOperator{\AgdaFunction{begin}}\<% +\\ +\>[2][@{}l@{\AgdaIndent{0}}]% +\>[3]\AgdaFunction{h}\AgdaSymbol{(}\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% \AgdaInductiveConstructor{node}\AgdaSpace{}% \AgdaBound{f}\AgdaSpace{}% \AgdaBound{t}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}% \AgdaOperator{\AgdaField{⟨\$⟩}}\AgdaSpace{}% \AgdaBound{a}\AgdaSymbol{)}% -\>[35]\AgdaFunction{≈⟨}\AgdaSpace{}% +\>[36]\AgdaFunction{≈⟨}\AgdaSpace{}% \AgdaField{compatible}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{∥}}\AgdaSpace{}% \AgdaBound{hh}\AgdaSpace{}% @@ -6287,7 +6291,7 @@ \subsection{Terms} \AgdaFunction{⟩}\<% \\ % -\>[2]\AgdaSymbol{(}\AgdaBound{f}\AgdaSpace{}% +\>[3]\AgdaSymbol{(}\AgdaBound{f}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{̂}}\AgdaSpace{}% \AgdaBound{𝑩}\AgdaSymbol{)(λ}\AgdaSpace{}% \AgdaBound{i}\AgdaSpace{}% @@ -6298,7 +6302,7 @@ \subsection{Terms} \AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}% \AgdaOperator{\AgdaField{⟨\$⟩}}\AgdaSpace{}% \AgdaBound{a}\AgdaSymbol{))}% -\>[37]\AgdaFunction{≈⟨}\AgdaSpace{}% +\>[36]\AgdaFunction{≈⟨}\AgdaSpace{}% \AgdaField{cong}\AgdaSymbol{(}\AgdaField{Interp}\AgdaSpace{}% \AgdaBound{𝑩}\AgdaSymbol{)(}\AgdaInductiveConstructor{≡.refl}\AgdaSpace{}% \AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}% @@ -6307,10 +6311,11 @@ \subsection{Terms} \AgdaSymbol{→}\AgdaSpace{}% \AgdaFunction{comm-hom-term}\AgdaSymbol{(}\AgdaBound{t}\AgdaSpace{}% \AgdaBound{i}\AgdaSymbol{)}\AgdaSpace{}% -\AgdaBound{a}\AgdaSymbol{)}\AgdaFunction{⟩}\<% +\AgdaBound{a}\AgdaSymbol{)}\AgdaSpace{}% +\AgdaFunction{⟩}\<% \\ % -\>[2]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% +\>[3]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% \AgdaInductiveConstructor{node}\AgdaSpace{}% \AgdaBound{f}\AgdaSpace{}% \AgdaBound{t}\AgdaSpace{}% @@ -6318,10 +6323,12 @@ \subsection{Terms} \AgdaOperator{\AgdaField{⟨\$⟩}}\AgdaSpace{}% \AgdaSymbol{(}\AgdaFunction{h}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{∘}}\AgdaSpace{}% -\AgdaBound{a}\AgdaSymbol{)}% -\>[35]\AgdaOperator{\AgdaFunction{∎}}\AgdaSpace{}% -\AgdaKeyword{where}% -\>[44]\AgdaKeyword{open}\AgdaSpace{}% +\AgdaBound{a}\AgdaSymbol{)}\<% +\\ +% +\>[2]\AgdaOperator{\AgdaFunction{∎}}\AgdaSpace{}% +\AgdaKeyword{where}\AgdaSpace{}% +\AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{SetoidReasoning}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% \AgdaBound{𝑩}\AgdaSpace{}% @@ -6356,15 +6363,16 @@ \subsection{Terms} \AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% \AgdaFunction{⨅}\AgdaSpace{}% \AgdaBound{𝒜}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{]}}\AgdaSpace{}% -\AgdaKeyword{using}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{]}}% +\>[23]\AgdaKeyword{using}\AgdaSpace{}% \AgdaSymbol{(}\AgdaSpace{}% \AgdaOperator{\AgdaField{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSpace{}% -\AgdaSymbol{)}\AgdaSpace{}% -\AgdaSymbol{;}\AgdaSpace{}% -\AgdaKeyword{open}\AgdaSpace{}% -\AgdaModule{Environment}\AgdaSpace{}% -\AgdaKeyword{using}\AgdaSpace{}% +\AgdaSymbol{)}\<% +\\ +% +\>[1]\AgdaKeyword{open}\AgdaSpace{}% +\AgdaModule{Environment}% +\>[23]\AgdaKeyword{using}\AgdaSpace{}% \AgdaSymbol{(}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧}}\AgdaSpace{}% \AgdaSymbol{;}\AgdaSpace{}% @@ -6372,6 +6380,8 @@ \subsection{Terms} \AgdaSymbol{)}\<% \\ % +\\[\AgdaEmptyExtraSkip]% +% \>[1]\AgdaFunction{interp-prod}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaSymbol{(}\AgdaBound{p}\AgdaSpace{}% @@ -6790,7 +6800,7 @@ \section{Equational Logic} \>[1]\AgdaInductiveConstructor{app}% \>[13]\AgdaSymbol{:}% \>[16]\AgdaSymbol{∀\{}\AgdaBound{Y}\AgdaSymbol{\}\{}\AgdaBound{ps}% -\>[4268I]\AgdaBound{qs}\AgdaSpace{}% +\>[4267I]\AgdaBound{qs}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{∥}}\AgdaSpace{}% \AgdaBound{𝑆}\AgdaSpace{}% @@ -6800,7 +6810,7 @@ \section{Equational Logic} \AgdaDatatype{Term}\AgdaSpace{}% \AgdaBound{Y}\AgdaSymbol{\}}\<% \\ -\>[4268I][@{}l@{\AgdaIndent{0}}]% +\>[4267I][@{}l@{\AgdaIndent{0}}]% \>[26]\AgdaSymbol{→}\AgdaSpace{}% \AgdaSymbol{(∀}\AgdaSpace{}% \AgdaBound{i}\AgdaSpace{}% @@ -7476,7 +7486,6 @@ \section{Equational Logic} An important property of the binary relation \aof{⊧} is \emph{algebraic invariance} (i.e., invariance under isomorphism). We formalize this result as follows. -\ifshort\else \begin{code}% \>[0]\<% \\ @@ -7499,12 +7508,8 @@ \section{Equational Logic} \AgdaDatatype{Term}\AgdaSpace{}% \AgdaBound{X}\AgdaSymbol{)}\AgdaSpace{}% \AgdaKeyword{where}\<% -\end{code} -\fi -\begin{code}% -\>[0]\<% \\ -\>[0][@{}l@{\AgdaIndent{1}}]% +\>[0][@{}l@{\AgdaIndent{0}}]% \>[1]\AgdaFunction{⊧-I-invar}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaBound{𝑨}\AgdaSpace{}% @@ -7532,54 +7537,56 @@ \section{Equational Logic} \AgdaBound{f∼g}\AgdaSpace{}% \AgdaBound{g∼f}\AgdaSymbol{)}\AgdaSpace{}% \AgdaBound{ρ}\AgdaSpace{}% -\AgdaSymbol{=}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{begin}}\<% +\AgdaSymbol{=}\<% \\ \>[1][@{}l@{\AgdaIndent{0}}]% -\>[6]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% +\>[2]\AgdaOperator{\AgdaFunction{begin}}\<% +\\ +% +\>[2]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% \AgdaBound{p}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟧}}% -\>[14]\AgdaOperator{\AgdaField{⟨\$⟩}}% -\>[32]\AgdaBound{ρ}% -\>[37]\AgdaFunction{≈˘⟨}% -\>[42]\AgdaField{cong}\AgdaSpace{}% +\>[12]\AgdaOperator{\AgdaField{⟨\$⟩}}% +\>[28]\AgdaBound{ρ}% +\>[33]\AgdaFunction{≈˘⟨}% +\>[38]\AgdaField{cong}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% \AgdaBound{p}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}% \AgdaSymbol{(}\AgdaBound{f∼g}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{∘}}\AgdaSpace{}% \AgdaBound{ρ}\AgdaSymbol{)}% -\>[70]\AgdaFunction{⟩}\<% +\>[66]\AgdaFunction{⟩}\<% \\ % -\>[6]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% +\>[2]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% \AgdaBound{p}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟧}}% -\>[14]\AgdaOperator{\AgdaField{⟨\$⟩}}\AgdaSpace{}% -\AgdaSymbol{(}\AgdaFunction{f}% -\>[22]\AgdaOperator{\AgdaFunction{∘}}% -\>[25]\AgdaSymbol{(}\AgdaFunction{g}% -\>[29]\AgdaOperator{\AgdaFunction{∘}}% -\>[32]\AgdaBound{ρ}\AgdaSymbol{))}% -\>[37]\AgdaFunction{≈˘⟨}% -\>[42]\AgdaFunction{comm-hom-term}\AgdaSpace{}% +\>[12]\AgdaOperator{\AgdaField{⟨\$⟩}}\AgdaSpace{}% +\AgdaSymbol{(}\AgdaFunction{f}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{∘}}% +\>[22]\AgdaSymbol{(}\AgdaFunction{g}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{∘}}% +\>[28]\AgdaBound{ρ}\AgdaSymbol{))}% +\>[33]\AgdaFunction{≈˘⟨}% +\>[38]\AgdaFunction{comm-hom-term}\AgdaSpace{}% \AgdaBound{fh}\AgdaSpace{}% \AgdaBound{p}\AgdaSpace{}% \AgdaSymbol{(}\AgdaFunction{g}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{∘}}\AgdaSpace{}% \AgdaBound{ρ}\AgdaSymbol{)}% -\>[70]\AgdaFunction{⟩}\<% +\>[66]\AgdaFunction{⟩}\<% \\ -\>[1][@{}l@{\AgdaIndent{0}}]% -\>[4]\AgdaFunction{f}\AgdaSymbol{(}\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% +% +\>[2]\AgdaFunction{f}\AgdaSymbol{(}\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% \AgdaBound{p}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟧ᴬ}}% -\>[14]\AgdaOperator{\AgdaField{⟨\$⟩}}% -\>[25]\AgdaSymbol{(}\AgdaFunction{g}% -\>[29]\AgdaOperator{\AgdaFunction{∘}}% -\>[32]\AgdaBound{ρ}\AgdaSymbol{))}% -\>[37]\AgdaFunction{≈⟨}% -\>[42]\AgdaField{cong}\AgdaSpace{}% +\>[12]\AgdaOperator{\AgdaField{⟨\$⟩}}% +\>[22]\AgdaSymbol{(}\AgdaFunction{g}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{∘}}% +\>[28]\AgdaBound{ρ}\AgdaSymbol{))}% +\>[33]\AgdaFunction{≈⟨}% +\>[38]\AgdaField{cong}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{∣}}\AgdaSpace{}% \AgdaBound{fh}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{∣}}\AgdaSpace{}% @@ -7587,58 +7594,58 @@ \section{Equational Logic} \AgdaSymbol{(}\AgdaFunction{g}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{∘}}\AgdaSpace{}% \AgdaBound{ρ}\AgdaSymbol{))}% -\>[70]\AgdaFunction{⟩}\<% +\>[66]\AgdaFunction{⟩}\<% \\ % -\>[4]\AgdaFunction{f}\AgdaSymbol{(}\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% +\>[2]\AgdaFunction{f}\AgdaSymbol{(}\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% \AgdaBound{q}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟧ᴬ}}% -\>[14]\AgdaOperator{\AgdaField{⟨\$⟩}}% -\>[25]\AgdaSymbol{(}\AgdaFunction{g}% -\>[29]\AgdaOperator{\AgdaFunction{∘}}% -\>[32]\AgdaBound{ρ}\AgdaSymbol{))}% -\>[37]\AgdaFunction{≈⟨}% -\>[42]\AgdaFunction{comm-hom-term}\AgdaSpace{}% +\>[12]\AgdaOperator{\AgdaField{⟨\$⟩}}% +\>[22]\AgdaSymbol{(}\AgdaFunction{g}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{∘}}% +\>[28]\AgdaBound{ρ}\AgdaSymbol{))}% +\>[33]\AgdaFunction{≈⟨}% +\>[38]\AgdaFunction{comm-hom-term}\AgdaSpace{}% \AgdaBound{fh}\AgdaSpace{}% \AgdaBound{q}\AgdaSpace{}% \AgdaSymbol{(}\AgdaFunction{g}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{∘}}\AgdaSpace{}% \AgdaBound{ρ}\AgdaSymbol{)}% -\>[70]\AgdaFunction{⟩}\<% +\>[66]\AgdaFunction{⟩}\<% \\ -\>[4][@{}l@{\AgdaIndent{0}}]% -\>[6]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% +% +\>[2]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% \AgdaBound{q}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟧}}% -\>[14]\AgdaOperator{\AgdaField{⟨\$⟩}}\AgdaSpace{}% -\AgdaSymbol{(}\AgdaFunction{f}% -\>[22]\AgdaOperator{\AgdaFunction{∘}}% -\>[25]\AgdaSymbol{(}\AgdaFunction{g}% -\>[29]\AgdaOperator{\AgdaFunction{∘}}% -\>[32]\AgdaBound{ρ}\AgdaSymbol{))}% -\>[37]\AgdaFunction{≈⟨}% -\>[42]\AgdaField{cong}\AgdaSpace{}% +\>[12]\AgdaOperator{\AgdaField{⟨\$⟩}}\AgdaSpace{}% +\AgdaSymbol{(}\AgdaFunction{f}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{∘}}% +\>[22]\AgdaSymbol{(}\AgdaFunction{g}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{∘}}% +\>[28]\AgdaBound{ρ}\AgdaSymbol{))}% +\>[33]\AgdaFunction{≈⟨}% +\>[38]\AgdaField{cong}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% \AgdaBound{q}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}% \AgdaSymbol{(}\AgdaBound{f∼g}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{∘}}\AgdaSpace{}% \AgdaBound{ρ}\AgdaSymbol{)}% -\>[70]\AgdaFunction{⟩}\<% +\>[66]\AgdaFunction{⟩}\<% \\ % -\>[6]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% +\>[2]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% \AgdaBound{q}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟧}}% -\>[14]\AgdaOperator{\AgdaField{⟨\$⟩}}% -\>[32]\AgdaBound{ρ}% -\>[37]\AgdaOperator{\AgdaFunction{∎}}\<% +\>[12]\AgdaOperator{\AgdaField{⟨\$⟩}}% +\>[28]\AgdaBound{ρ}% +\>[33]\AgdaOperator{\AgdaFunction{∎}}\<% \\ -\>[1][@{}l@{\AgdaIndent{0}}]% +% \>[2]\AgdaKeyword{where}\<% \\ -% -\>[2]\AgdaKeyword{private}\AgdaSpace{}% +\>[2][@{}l@{\AgdaIndent{0}}]% +\>[3]\AgdaKeyword{private}\AgdaSpace{}% \AgdaFunction{f}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaOperator{\AgdaField{\AgdaUnderscore{}⟨\$⟩\AgdaUnderscore{}}}\AgdaSpace{}% @@ -7654,10 +7661,10 @@ \section{Equational Logic} \AgdaOperator{\AgdaFunction{∣}}\<% \\ % -\>[2]\AgdaKeyword{open}\AgdaSpace{}% +\>[3]\AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{Environment}\AgdaSpace{}% \AgdaBound{𝑨}% -\>[25]\AgdaKeyword{using}\AgdaSpace{}% +\>[23]\AgdaKeyword{using}\AgdaSpace{}% \AgdaSymbol{()}\AgdaSpace{}% \AgdaKeyword{renaming}\AgdaSpace{}% \AgdaSymbol{(}\AgdaSpace{}% @@ -7667,16 +7674,16 @@ \section{Equational Logic} \AgdaSymbol{)}\<% \\ % -\>[2]\AgdaKeyword{open}\AgdaSpace{}% +\>[3]\AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{Environment}\AgdaSpace{}% \AgdaBound{𝑩}% -\>[25]\AgdaKeyword{using}\AgdaSpace{}% +\>[23]\AgdaKeyword{using}\AgdaSpace{}% \AgdaSymbol{(}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧}}\AgdaSpace{}% \AgdaSymbol{)}\<% \\ % -\>[2]\AgdaKeyword{open}\AgdaSpace{}% +\>[3]\AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{SetoidReasoning}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% \AgdaBound{𝑩}\AgdaSpace{}% @@ -7949,9 +7956,9 @@ \section{Equational Logic} \\ \>[1][@{}l@{\AgdaIndent{0}}]% \>[2]\AgdaSymbol{(}% -\>[4982I]\AgdaOperator{\AgdaFunction{begin}}\<% +\>[4986I]\AgdaOperator{\AgdaFunction{begin}}\<% \\ -\>[.][@{}l@{}]\<[4982I]% +\>[.][@{}l@{}]\<[4986I]% \>[4]\AgdaFunction{h}\AgdaSpace{}% \AgdaSymbol{(}% \>[9]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% @@ -9524,26 +9531,23 @@ \section{Free Algebras} \>[0]\<% \\ \>[0]\AgdaKeyword{module}\AgdaSpace{}% -\AgdaModule{\AgdaUnderscore{}}% -\>[10]\AgdaSymbol{\{}\AgdaBound{𝑨}\AgdaSpace{}% +\AgdaModule{\AgdaUnderscore{}}\AgdaSpace{}% +\AgdaSymbol{\{}\AgdaBound{𝑨}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaRecord{Algebra}\AgdaSpace{}% \AgdaSymbol{(}\AgdaGeneralizable{α}\AgdaSpace{}% \AgdaOperator{\AgdaPrimitive{⊔}}\AgdaSpace{}% \AgdaGeneralizable{ρᵃ}\AgdaSpace{}% \AgdaOperator{\AgdaPrimitive{⊔}}\AgdaSpace{}% -\AgdaGeneralizable{ℓ}\AgdaSymbol{)}\AgdaSpace{}% -\AgdaSymbol{(}\AgdaGeneralizable{α}\AgdaSpace{}% +\AgdaGeneralizable{ℓ}\AgdaSymbol{)(}\AgdaGeneralizable{α}\AgdaSpace{}% \AgdaOperator{\AgdaPrimitive{⊔}}\AgdaSpace{}% \AgdaGeneralizable{ρᵃ}\AgdaSpace{}% \AgdaOperator{\AgdaPrimitive{⊔}}\AgdaSpace{}% -\AgdaGeneralizable{ℓ}\AgdaSymbol{)\}}\AgdaSpace{}% -\AgdaSymbol{\{}\AgdaBound{𝒦}\AgdaSpace{}% +\AgdaGeneralizable{ℓ}\AgdaSymbol{)\}\{}\AgdaBound{𝒦}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaFunction{Pred}\AgdaSymbol{(}\AgdaRecord{Algebra}\AgdaSpace{}% \AgdaGeneralizable{α}\AgdaSpace{}% -\AgdaGeneralizable{ρᵃ}\AgdaSymbol{)}\AgdaSpace{}% -\AgdaSymbol{(}\AgdaGeneralizable{α}\AgdaSpace{}% +\AgdaGeneralizable{ρᵃ}\AgdaSymbol{)(}\AgdaGeneralizable{α}\AgdaSpace{}% \AgdaOperator{\AgdaPrimitive{⊔}}\AgdaSpace{}% \AgdaGeneralizable{ρᵃ}\AgdaSpace{}% \AgdaOperator{\AgdaPrimitive{⊔}}\AgdaSpace{}% @@ -9552,27 +9556,6 @@ \section{Free Algebras} \AgdaKeyword{where}\<% \\ \>[0][@{}l@{\AgdaIndent{0}}]% -\>[1]\AgdaKeyword{open}\AgdaSpace{}% -\AgdaModule{Setoid}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% -\AgdaBound{𝑨}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{]}}\AgdaSpace{}% -\AgdaKeyword{using}\AgdaSpace{}% -\AgdaSymbol{(}\AgdaSpace{}% -\AgdaFunction{refl}\AgdaSpace{}% -\AgdaSymbol{;}\AgdaSpace{}% -\AgdaFunction{sym}% -\>[40]\AgdaSymbol{;}\AgdaSpace{}% -\AgdaFunction{trans}\AgdaSpace{}% -\AgdaSymbol{)}% -\>[51]\AgdaKeyword{renaming}% -\>[61]\AgdaSymbol{(}\AgdaSpace{}% -\AgdaField{Carrier}% -\>[72]\AgdaSymbol{to}\AgdaSpace{}% -\AgdaField{A}\AgdaSpace{}% -\AgdaSymbol{)}\<% -\\ -% \>[1]\AgdaKeyword{private}\AgdaSpace{}% \AgdaFunction{c}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% @@ -9585,20 +9568,44 @@ \section{Free Algebras} \AgdaFunction{ι}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaFunction{ov}\AgdaSpace{}% -\AgdaFunction{c}% -\>[41]\AgdaSymbol{;}% -\>[52]\AgdaKeyword{open}\AgdaSpace{}% +\AgdaFunction{c}\<% +\\ +% +\>[1]\AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{FreeAlgebra}\AgdaSpace{}% \AgdaSymbol{\{}\AgdaArgument{χ}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaFunction{c}\AgdaSymbol{\}(}\AgdaFunction{Th}\AgdaSpace{}% \AgdaBound{𝒦}\AgdaSymbol{)}% -\>[84]\AgdaKeyword{using}\AgdaSpace{}% +\>[35]\AgdaKeyword{using}\AgdaSpace{}% \AgdaSymbol{(}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{𝔽[\AgdaUnderscore{}]}}\AgdaSpace{}% \AgdaSymbol{)}\<% \\ % +\>[1]\AgdaKeyword{open}\AgdaSpace{}% +\AgdaModule{Setoid}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% +\AgdaBound{𝑨}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{]}}% +\>[35]\AgdaKeyword{using}\AgdaSpace{}% +\AgdaSymbol{(}\AgdaSpace{}% +\AgdaFunction{refl}\AgdaSpace{}% +\AgdaSymbol{;}\AgdaSpace{}% +\AgdaFunction{sym}\AgdaSpace{}% +\AgdaSymbol{;}\AgdaSpace{}% +\AgdaFunction{trans}\AgdaSpace{}% +\AgdaSymbol{)}\AgdaSpace{}% +\AgdaKeyword{renaming}\AgdaSpace{}% +\AgdaSymbol{(}\AgdaSpace{}% +\AgdaField{Carrier}\AgdaSpace{}% +\AgdaSymbol{to}\AgdaSpace{}% +\AgdaField{A}\AgdaSpace{}% +\AgdaSymbol{)}\<% +\\ +% +\\[\AgdaEmptyExtraSkip]% +% \>[1]\AgdaFunction{F-ModTh-epi}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaBound{𝑨}\AgdaSpace{}% @@ -9626,15 +9633,15 @@ \section{Free Algebras} \\ \>[1][@{}l@{\AgdaIndent{0}}]% \>[2]\AgdaKeyword{where}% -\>[6058I]\AgdaKeyword{open}\AgdaSpace{}% +\>[9]\AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{FreeHom}\AgdaSpace{}% \AgdaSymbol{\{}\AgdaArgument{ℓ}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaBound{ℓ}\AgdaSymbol{\}}\AgdaSpace{}% \AgdaSymbol{\{}\AgdaBound{𝒦}\AgdaSymbol{\}}\<% \\ -\>[.][@{}l@{}]\<[6058I]% -\>[8]\AgdaFunction{φ}\AgdaSpace{}% +% +\>[9]\AgdaFunction{φ}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{𝔽[}}\AgdaSpace{}% @@ -9647,23 +9654,23 @@ \section{Free Algebras} \AgdaOperator{\AgdaFunction{]}}\<% \\ % -\>[8]\AgdaOperator{\AgdaField{\AgdaUnderscore{}⟨\$⟩\AgdaUnderscore{}}}\AgdaSpace{}% -\AgdaFunction{φ}\AgdaSpace{}% -\AgdaSymbol{=}\AgdaSpace{}% +\>[9]\AgdaOperator{\AgdaField{\AgdaUnderscore{}⟨\$⟩\AgdaUnderscore{}}}\AgdaSpace{}% +\AgdaFunction{φ}% +\>[28]\AgdaSymbol{=}\AgdaSpace{}% \AgdaFunction{free-lift}\AgdaSymbol{\{}\AgdaArgument{𝑨}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaBound{𝑨}\AgdaSymbol{\}}\AgdaSpace{}% \AgdaFunction{id}\<% \\ % -\>[8]\AgdaField{cong}\AgdaSpace{}% +\>[9]\AgdaField{cong}\AgdaSpace{}% \AgdaFunction{φ}\AgdaSpace{}% \AgdaSymbol{\{}\AgdaBound{p}\AgdaSymbol{\}}\AgdaSpace{}% \AgdaSymbol{\{}\AgdaBound{q}\AgdaSymbol{\}}\AgdaSpace{}% \AgdaBound{pq}% -\>[27]\AgdaSymbol{=}% -\>[30]\AgdaFunction{trans}% -\>[37]\AgdaSymbol{(}\AgdaSpace{}% +\>[28]\AgdaSymbol{=}% +\>[31]\AgdaFunction{trans}% +\>[38]\AgdaSymbol{(}\AgdaSpace{}% \AgdaFunction{sym}\AgdaSpace{}% \AgdaSymbol{(}\AgdaFunction{free-lift-interp}\AgdaSymbol{\{}\AgdaArgument{𝑨}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% @@ -9673,9 +9680,9 @@ \section{Free Algebras} \AgdaSymbol{)}\<% \\ % -\>[27]\AgdaSymbol{(}% -\>[30]\AgdaFunction{trans}% -\>[37]\AgdaSymbol{(}\AgdaSpace{}% +\>[28]\AgdaSymbol{(}% +\>[31]\AgdaFunction{trans}% +\>[38]\AgdaSymbol{(}\AgdaSpace{}% \AgdaBound{A∈ModThK}\AgdaSymbol{\{}\AgdaArgument{p}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaBound{p}\AgdaSymbol{\}\{}\AgdaBound{q}\AgdaSymbol{\}}\AgdaSpace{}% @@ -9685,7 +9692,7 @@ \section{Free Algebras} \AgdaSymbol{)}\<% \\ % -\>[37]\AgdaSymbol{(}\AgdaSpace{}% +\>[38]\AgdaSymbol{(}\AgdaSpace{}% \AgdaFunction{free-lift-interp}\AgdaSymbol{\{}\AgdaArgument{𝑨}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaBound{𝑨}\AgdaSymbol{\}}\AgdaSpace{}% @@ -9695,7 +9702,7 @@ \section{Free Algebras} \AgdaSymbol{)}\<% \\ % -\>[8]\AgdaFunction{isEpi}\AgdaSpace{}% +\>[9]\AgdaFunction{isEpi}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaRecord{IsEpi}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{𝔽[}}\AgdaSpace{}% @@ -9705,7 +9712,7 @@ \section{Free Algebras} \AgdaFunction{φ}\<% \\ % -\>[8]\AgdaField{compatible}\AgdaSpace{}% +\>[9]\AgdaField{compatible}\AgdaSpace{}% \AgdaSymbol{(}\AgdaField{isHom}\AgdaSpace{}% \AgdaFunction{isEpi}\AgdaSymbol{)}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% @@ -9720,7 +9727,7 @@ \section{Free Algebras} \AgdaFunction{refl}\AgdaSymbol{))}\<% \\ % -\>[8]\AgdaField{isSurjective}\AgdaSpace{}% +\>[9]\AgdaField{isSurjective}\AgdaSpace{}% \AgdaFunction{isEpi}\AgdaSpace{}% \AgdaSymbol{\{}\AgdaBound{y}\AgdaSymbol{\}}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% @@ -9837,7 +9844,7 @@ \subsection{Informal proof} \ab g (\af{⟦~\T{X}~⟧} \ab q) = \af{⟦~\Free{X}~⟧} \ab q,\\[8pt] so \ab{𝒦} \af{⊫} \ab p \af{≈} \ab q, thus (\ab p , \ab q) \af{∈} \af{Th} \ab{𝒦}. Since \ab{𝑨} \af{∈} \af{Mod} (\af{Th} \ab{𝒦}) = -\af{Mod} (\af{Th} \ab{𝒦}), we obtain \ab{𝑨} \af{⊧} \ab p \af{≈} \ab q, which implies +\af{Mod} (\af{Th} \ab{𝒦}), we obtain \ab{𝑨}~\af{⊧}~\ab p~\af{≈}~\ab q, which implies that \ab h \ab u = (\af{⟦~\ab{𝑨}~⟧} \ab p) \aofld{⟨\$⟩} \ab{ρ} = (\af{⟦~\ab{𝑨}~⟧} \ab q) \aofld{⟨\$⟩} \ab{ρ} = \ab h \ab v, as desired. @@ -9870,6 +9877,8 @@ \subsection{Formal proof} \AgdaGeneralizable{ℓ}\AgdaSymbol{))}\AgdaSpace{}% \AgdaKeyword{where}\<% \\ +% +\\[\AgdaEmptyExtraSkip]% \>[0][@{}l@{\AgdaIndent{0}}]% \>[1]\AgdaFunction{V-expa}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% @@ -9919,8 +9928,8 @@ \subsection{Formal proof} \AgdaModule{Setoid}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% \AgdaBound{𝑨}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{]}}\AgdaSpace{}% -\AgdaKeyword{using}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{]}}% +\>[32]\AgdaKeyword{using}\AgdaSpace{}% \AgdaSymbol{(}\AgdaSpace{}% \AgdaFunction{refl}\AgdaSpace{}% \AgdaSymbol{)}\<% @@ -9934,8 +9943,8 @@ \subsection{Formal proof} \AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}% \AgdaSymbol{→}\AgdaSpace{}% \AgdaBound{𝑨}\AgdaSymbol{)}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{]}}\AgdaSpace{}% -\AgdaKeyword{using}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{]}}% +\>[32]\AgdaKeyword{using}\AgdaSpace{}% \AgdaSymbol{()}\AgdaSpace{}% \AgdaKeyword{renaming}\AgdaSpace{}% \AgdaSymbol{(}\AgdaSpace{}% @@ -9945,6 +9954,8 @@ \subsection{Formal proof} \AgdaSymbol{)}\<% \\ % +\\[\AgdaEmptyExtraSkip]% +% \>[2]\AgdaFunction{to⨅}% \>[9]\AgdaSymbol{:}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% @@ -9960,21 +9971,6 @@ \subsection{Formal proof} \AgdaOperator{\AgdaFunction{]}}\<% \\ % -\>[2]\AgdaFunction{from⨅}% -\>[9]\AgdaSymbol{:}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% -\AgdaFunction{⨅}\AgdaSpace{}% -\AgdaSymbol{(λ}\AgdaSpace{}% -\AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}% -\AgdaSymbol{→}\AgdaSpace{}% -\AgdaBound{𝑨}\AgdaSymbol{)}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{]}}% -\>[29]\AgdaOperator{\AgdaRecord{⟶}}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% -\AgdaBound{𝑨}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{]}}\<% -\\ -% \>[2]\AgdaFunction{to⨅}% \>[9]\AgdaSymbol{=}\AgdaSpace{}% \AgdaKeyword{record}\AgdaSpace{}% @@ -9998,6 +9994,21 @@ \subsection{Formal proof} \\ % \>[2]\AgdaFunction{from⨅}% +\>[9]\AgdaSymbol{:}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% +\AgdaFunction{⨅}\AgdaSpace{}% +\AgdaSymbol{(λ}\AgdaSpace{}% +\AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}% +\AgdaSymbol{→}\AgdaSpace{}% +\AgdaBound{𝑨}\AgdaSymbol{)}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{]}}% +\>[29]\AgdaOperator{\AgdaRecord{⟶}}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% +\AgdaBound{𝑨}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{]}}\<% +\\ +% +\>[2]\AgdaFunction{from⨅}% \>[9]\AgdaSymbol{=}\AgdaSpace{}% \AgdaKeyword{record}\AgdaSpace{}% \AgdaSymbol{\{}\AgdaSpace{}% @@ -10034,21 +10045,17 @@ \subsection{Formal proof} % \>[2]\AgdaFunction{Goal}% \>[9]\AgdaSymbol{=}\AgdaSpace{}% -\AgdaInductiveConstructor{mkiso}\AgdaSpace{}% -\AgdaSymbol{(}\AgdaFunction{to⨅}\AgdaSpace{}% +\AgdaInductiveConstructor{mkiso}\AgdaSymbol{(}\AgdaFunction{to⨅}\AgdaSpace{}% \AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}% \AgdaInductiveConstructor{mkhom}\AgdaSpace{}% -\AgdaFunction{refl⨅}\AgdaSymbol{)}\AgdaSpace{}% -\AgdaSymbol{(}\AgdaFunction{from⨅}\AgdaSpace{}% +\AgdaFunction{refl⨅}\AgdaSymbol{)(}\AgdaFunction{from⨅}\AgdaSpace{}% \AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}% \AgdaInductiveConstructor{mkhom}\AgdaSpace{}% -\AgdaFunction{refl}\AgdaSymbol{)}\AgdaSpace{}% -\AgdaSymbol{(λ}\AgdaSpace{}% +\AgdaFunction{refl}\AgdaSymbol{)(λ}\AgdaSpace{}% \AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}% \AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}% \AgdaSymbol{→}\AgdaSpace{}% -\AgdaFunction{refl}\AgdaSymbol{)}\AgdaSpace{}% -\AgdaSymbol{(λ}\AgdaSpace{}% +\AgdaFunction{refl}\AgdaSymbol{)(λ}\AgdaSpace{}% \AgdaBound{\AgdaUnderscore{}}\AgdaSpace{}% \AgdaSymbol{→}\AgdaSpace{}% \AgdaFunction{refl}\AgdaSymbol{)}\<% @@ -10102,6 +10109,8 @@ \subsection{Formal proof} \>[36]\AgdaComment{--\ an\ arbitrary\ equational\ class}\<% \\ % +\\[\AgdaEmptyExtraSkip]% +% \>[1]\AgdaFunction{EqCl⇒Var}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaFunction{V}\AgdaSpace{}% @@ -10193,6 +10202,8 @@ \subsection{Formal proof} \AgdaFunction{c}\<% \\ % +\\[\AgdaEmptyExtraSkip]% +% \>[1]\AgdaFunction{ModTh-closure}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaFunction{V}\AgdaSymbol{\{}\AgdaArgument{β}\AgdaSpace{}% @@ -10624,14 +10635,14 @@ \subsection{Formal proof} \>[2]\AgdaFunction{free-lift}\AgdaSpace{}% \AgdaBound{ρ}\AgdaSpace{}% \AgdaBound{p}% -\>[18]\AgdaFunction{≈˘⟨}\AgdaSpace{}% -\AgdaFunction{free-lift-interp}\AgdaSpace{}% +\>[18]\AgdaFunction{≈˘⟨}% +\>[23]\AgdaFunction{free-lift-interp}\AgdaSpace{}% \AgdaSymbol{\{}\AgdaArgument{𝑨}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaBound{𝑨}\AgdaSymbol{\}}\AgdaSpace{}% \AgdaBound{ρ}\AgdaSpace{}% -\AgdaBound{p}\AgdaSpace{}% -\AgdaFunction{⟩}\<% +\AgdaBound{p}% +\>[65]\AgdaFunction{⟩}\<% \\ % \>[2]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% @@ -10639,8 +10650,8 @@ \subsection{Formal proof} \AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}% \AgdaOperator{\AgdaField{⟨\$⟩}}\AgdaSpace{}% \AgdaBound{ρ}% -\>[19]\AgdaFunction{≈⟨}\AgdaSpace{}% -\AgdaFunction{S-id1}\AgdaSpace{}% +\>[18]\AgdaFunction{≈⟨}% +\>[23]\AgdaFunction{S-id1}\AgdaSpace{}% \AgdaSymbol{\{}\AgdaArgument{ℓ}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaBound{ℓ}\AgdaSymbol{\}}\AgdaSpace{}% @@ -10652,8 +10663,8 @@ \subsection{Formal proof} \AgdaBound{pKq}\AgdaSymbol{)}\AgdaSpace{}% \AgdaBound{𝑨}\AgdaSpace{}% \AgdaBound{sA}\AgdaSpace{}% -\AgdaBound{ρ}\AgdaSpace{}% -\AgdaFunction{⟩}\<% +\AgdaBound{ρ}% +\>[65]\AgdaFunction{⟩}\<% \\ % \>[2]\AgdaOperator{\AgdaFunction{⟦}}\AgdaSpace{}% @@ -10661,14 +10672,14 @@ \subsection{Formal proof} \AgdaOperator{\AgdaFunction{⟧}}\AgdaSpace{}% \AgdaOperator{\AgdaField{⟨\$⟩}}\AgdaSpace{}% \AgdaBound{ρ}% -\>[19]\AgdaFunction{≈⟨}\AgdaSpace{}% -\AgdaFunction{free-lift-interp}\AgdaSpace{}% +\>[18]\AgdaFunction{≈⟨}% +\>[23]\AgdaFunction{free-lift-interp}\AgdaSpace{}% \AgdaSymbol{\{}\AgdaArgument{𝑨}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaBound{𝑨}\AgdaSymbol{\}}\AgdaSpace{}% \AgdaBound{ρ}\AgdaSpace{}% -\AgdaBound{q}\AgdaSpace{}% -\AgdaFunction{⟩}\<% +\AgdaBound{q}% +\>[65]\AgdaFunction{⟩}\<% \\ % \>[2]\AgdaFunction{free-lift}\AgdaSpace{}% @@ -10678,33 +10689,33 @@ \subsection{Formal proof} \\ % \>[2]\AgdaKeyword{where}% -\>[6704I]\AgdaKeyword{open}\AgdaSpace{}% +\>[9]\AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{Environment}\AgdaSpace{}% \AgdaBound{𝑨}% -\>[28]\AgdaKeyword{using}\AgdaSpace{}% +\>[29]\AgdaKeyword{using}\AgdaSpace{}% \AgdaSymbol{(}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{⟦\AgdaUnderscore{}⟧}}\AgdaSpace{}% \AgdaSymbol{)}\<% \\ -\>[.][@{}l@{}]\<[6704I]% -\>[8]\AgdaKeyword{open}\AgdaSpace{}% +% +\>[9]\AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{Setoid}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% \AgdaBound{𝑨}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{]}}% -\>[28]\AgdaKeyword{using}\AgdaSpace{}% +\>[29]\AgdaKeyword{using}\AgdaSpace{}% \AgdaSymbol{(}\AgdaSpace{}% \AgdaOperator{\AgdaField{\AgdaUnderscore{}≈\AgdaUnderscore{}}}\AgdaSpace{}% \AgdaSymbol{)}% -\>[43]\AgdaSymbol{;}% -\>[46]\AgdaKeyword{open}\AgdaSpace{}% +\>[44]\AgdaSymbol{;}% +\>[47]\AgdaKeyword{open}\AgdaSpace{}% \AgdaModule{SetoidReasoning}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{𝔻[}}\AgdaSpace{}% \AgdaBound{𝑨}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{]}}\<% \\ % -\>[8]\AgdaFunction{ζ}\AgdaSpace{}% +\>[9]\AgdaFunction{ζ}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaSymbol{∀\{}\AgdaBound{p}\AgdaSpace{}% \AgdaBound{q}\AgdaSymbol{\}}\AgdaSpace{}% @@ -10725,7 +10736,7 @@ \subsection{Formal proof} \AgdaBound{q}\<% \\ % -\>[8]\AgdaFunction{ζ}\AgdaSpace{}% +\>[9]\AgdaFunction{ζ}\AgdaSpace{}% \AgdaBound{x}\AgdaSpace{}% \AgdaBound{𝑨}\AgdaSpace{}% \AgdaBound{kA}\AgdaSpace{}% @@ -11149,7 +11160,7 @@ \subsection{Formal proof} \end{itemize} \begin{itemize} \item \ref{item:2}. We show that every algebra in \af{Mod} (\af{Th} (\af{V} -\ab{𝒦})) is a homomorphic image of \af{𝔽[~\ab{X}~]}, as follows. +\ab{𝒦})) is a homomorphic image of \af{𝔽[~\ab{X}~]}. \begin{code}% \>[0]\<% \\ @@ -11181,20 +11192,11 @@ \subsection{Formal proof} \AgdaFunction{ι}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% \AgdaFunction{ov}\AgdaSpace{}% -\AgdaFunction{c}\AgdaSpace{}% -\AgdaSymbol{;}\AgdaSpace{}% -\AgdaKeyword{open}\AgdaSpace{}% -\AgdaModule{FreeAlgebra}\AgdaSpace{}% -\AgdaSymbol{\{}\AgdaArgument{χ}\AgdaSpace{}% -\AgdaSymbol{=}\AgdaSpace{}% -\AgdaFunction{c}\AgdaSymbol{\}(}\AgdaFunction{Th}\AgdaSpace{}% -\AgdaBound{𝒦}\AgdaSymbol{)}\AgdaSpace{}% -\AgdaKeyword{using}\AgdaSpace{}% -\AgdaSymbol{(}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{𝔽[\AgdaUnderscore{}]}}\AgdaSpace{}% -\AgdaSymbol{)}\<% +\AgdaFunction{c}\<% \\ % +\\[\AgdaEmptyExtraSkip]% +% \>[1]\AgdaFunction{Var⇒EqCl}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaSymbol{∀}\AgdaSpace{}% @@ -11227,7 +11229,10 @@ \subsection{Formal proof} \AgdaOperator{\AgdaFunction{]}}\AgdaSpace{}% \AgdaOperator{\AgdaFunction{]}}\AgdaSpace{}% \AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}% -\AgdaSymbol{(}\AgdaFunction{spFA}\AgdaSpace{}% +\AgdaSymbol{(}\AgdaFunction{SPF}\AgdaSymbol{\{}\AgdaArgument{ℓ}\AgdaSpace{}% +\AgdaSymbol{=}\AgdaSpace{}% +\AgdaBound{ℓ}\AgdaSymbol{\}}\AgdaSpace{}% +\AgdaBound{𝒦}\AgdaSpace{}% \AgdaOperator{\AgdaInductiveConstructor{,}}\AgdaSpace{}% \AgdaFunction{Aim}\AgdaSymbol{)}\<% \\ @@ -11235,28 +11240,16 @@ \subsection{Formal proof} \>[2]\AgdaKeyword{where}\<% \\ % -\>[2]\AgdaFunction{spFA}\AgdaSpace{}% -\AgdaSymbol{:}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{𝔽[}}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{𝕌[}}\AgdaSpace{}% -\AgdaBound{𝑨}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{]}}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{]}}\AgdaSpace{}% -\AgdaOperator{\AgdaFunction{∈}}\AgdaSpace{}% -\AgdaFunction{S}\AgdaSymbol{\{}\AgdaFunction{ι}\AgdaSymbol{\}}\AgdaSpace{}% -\AgdaFunction{ι}\AgdaSpace{}% -\AgdaSymbol{(}\AgdaFunction{P}\AgdaSpace{}% -\AgdaBound{ℓ}\AgdaSpace{}% -\AgdaFunction{ι}\AgdaSpace{}% -\AgdaBound{𝒦}\AgdaSymbol{)}\<% -\\ -% -\>[2]\AgdaFunction{spFA}\AgdaSpace{}% -\AgdaSymbol{=}\AgdaSpace{}% -\AgdaFunction{SPF}\AgdaSymbol{\{}\AgdaArgument{ℓ}\AgdaSpace{}% +\>[2]\AgdaKeyword{open}\AgdaSpace{}% +\AgdaModule{FreeAlgebra}\AgdaSpace{}% +\AgdaSymbol{\{}\AgdaArgument{χ}\AgdaSpace{}% \AgdaSymbol{=}\AgdaSpace{}% -\AgdaBound{ℓ}\AgdaSymbol{\}}\AgdaSpace{}% -\AgdaBound{𝒦}\<% +\AgdaFunction{c}\AgdaSymbol{\}(}\AgdaFunction{Th}\AgdaSpace{}% +\AgdaBound{𝒦}\AgdaSymbol{)}\AgdaSpace{}% +\AgdaKeyword{using}\AgdaSpace{}% +\AgdaSymbol{(}\AgdaSpace{}% +\AgdaOperator{\AgdaFunction{𝔽[\AgdaUnderscore{}]}}\AgdaSpace{}% +\AgdaSymbol{)}\<% \\ % \>[2]\AgdaFunction{epiFlA}\AgdaSpace{}% @@ -11287,6 +11280,8 @@ \subsection{Formal proof} \AgdaBound{p}\AgdaSymbol{\}\{}\AgdaBound{q}\AgdaSymbol{\})}\<% \\ % +\\[\AgdaEmptyExtraSkip]% +% \>[2]\AgdaFunction{φ}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaFunction{Lift-Alg}\AgdaSpace{}% @@ -11316,6 +11311,8 @@ \subsection{Formal proof} \AgdaFunction{epiFlA}\<% \\ % +\\[\AgdaEmptyExtraSkip]% +% \>[2]\AgdaFunction{Aim}\AgdaSpace{}% \AgdaSymbol{:}\AgdaSpace{}% \AgdaBound{𝑨}\AgdaSpace{}% diff --git a/src/Demos/HSP.lagda b/src/Demos/HSP.lagda index 7a3dcee9..2b5dd6a4 100644 --- a/src/Demos/HSP.lagda +++ b/src/Demos/HSP.lagda @@ -1342,19 +1342,25 @@ The first is the assertion that every term commutes with every homomorphism (\af the second is the interpretation of a term in a product algebra (\af{interp-prod}). \begin{code} -module _ {X : Type χ}{𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ}(hh : hom 𝑨 𝑩) where - open Environment 𝑨 using ( ⟦_⟧ ) ; open Environment 𝑩 renaming ( ⟦_⟧ to ⟦_⟧ᴮ ) using () - open Setoid 𝔻[ 𝑩 ] using ( _≈_ ; refl ) +module _ {X : Type χ}{𝑨 : Algebra α ρᵃ}{𝑩 : Algebra β ρᵇ}(hh : hom 𝑨 𝑩) where + open Environment 𝑨 using ( ⟦_⟧ ) + open Environment 𝑩 using () renaming ( ⟦_⟧ to ⟦_⟧ᴮ ) + open Setoid 𝔻[ 𝑩 ] using ( _≈_ ; refl ) private hfunc = ∣ hh ∣ ; h = _⟨$⟩_ hfunc + comm-hom-term : (t : Term X) (a : X → 𝕌[ 𝑨 ]) → h (⟦ t ⟧ ⟨$⟩ a) ≈ ⟦ t ⟧ᴮ ⟨$⟩ (h ∘ a) - comm-hom-term (ℊ x) a = refl - comm-hom-term (node f t) a = begin - h(⟦ node f t ⟧ ⟨$⟩ a) ≈⟨ compatible ∥ hh ∥ ⟩ - (f ̂ 𝑩)(λ i → h(⟦ t i ⟧ ⟨$⟩ a)) ≈⟨ cong(Interp 𝑩)(≡.refl , λ i → comm-hom-term(t i) a)⟩ - ⟦ node f t ⟧ᴮ ⟨$⟩ (h ∘ a) ∎ where open SetoidReasoning 𝔻[ 𝑩 ] + comm-hom-term (ℊ x) a = refl + comm-hom-term (node f t) a = + begin + h(⟦ node f t ⟧ ⟨$⟩ a) ≈⟨ compatible ∥ hh ∥ ⟩ + (f ̂ 𝑩)(λ i → h(⟦ t i ⟧ ⟨$⟩ a)) ≈⟨ cong(Interp 𝑩)(≡.refl , λ i → comm-hom-term(t i) a) ⟩ + ⟦ node f t ⟧ᴮ ⟨$⟩ (h ∘ a) + ∎ where open SetoidReasoning 𝔻[ 𝑩 ] module _ {X : Type χ}{ι : Level} {I : Type ι} (𝒜 : I → Algebra α ρᵃ) where - open Setoid 𝔻[ ⨅ 𝒜 ] using ( _≈_ ) ; open Environment using ( ⟦_⟧ ; ≃→Equal ) + open Setoid 𝔻[ ⨅ 𝒜 ] using ( _≈_ ) + open Environment using ( ⟦_⟧ ; ≃→Equal ) + interp-prod : (p : Term X) → ∀ ρ → (⟦ ⨅ 𝒜 ⟧ p) ⟨$⟩ ρ ≈ λ i → (⟦ 𝒜 i ⟧ p) ⟨$⟩ λ x → (ρ x) i interp-prod (ℊ x) = λ ρ i → ≃→Equal (𝒜 i) (ℊ x) (ℊ x) ≃-isRefl λ _ → (ρ x) i interp-prod (node f t) = λ ρ → cong (Interp (⨅ 𝒜)) ( ≡.refl , λ j k → interp-prod (t j) ρ k ) @@ -1561,27 +1567,23 @@ module _ {α ρᵃ β ρᵇ γ ρᶜ δ ρᵈ : Level} where An important property of the binary relation \aof{⊧} is \emph{algebraic invariance} (i.e., invariance under isomorphism). We formalize this result as follows. -\ifshort\else \begin{code} module _ {X : Type χ}{𝑨 : Algebra α ρᵃ}(𝑩 : Algebra β ρᵇ)(p q : Term X) where -\end{code} -\fi -\begin{code} - ⊧-I-invar : 𝑨 ⊧ p ≈ q → 𝑨 ≅ 𝑩 → 𝑩 ⊧ p ≈ q - ⊧-I-invar Apq (mkiso fh gh f∼g g∼f) ρ = begin - ⟦ p ⟧ ⟨$⟩ ρ ≈˘⟨ cong ⟦ p ⟧ (f∼g ∘ ρ) ⟩ - ⟦ p ⟧ ⟨$⟩ (f ∘ (g ∘ ρ)) ≈˘⟨ comm-hom-term fh p (g ∘ ρ) ⟩ - f(⟦ p ⟧ᴬ ⟨$⟩ (g ∘ ρ)) ≈⟨ cong ∣ fh ∣ (Apq (g ∘ ρ)) ⟩ - f(⟦ q ⟧ᴬ ⟨$⟩ (g ∘ ρ)) ≈⟨ comm-hom-term fh q (g ∘ ρ) ⟩ - ⟦ q ⟧ ⟨$⟩ (f ∘ (g ∘ ρ)) ≈⟨ cong ⟦ q ⟧ (f∼g ∘ ρ) ⟩ - ⟦ q ⟧ ⟨$⟩ ρ ∎ + ⊧-I-invar Apq (mkiso fh gh f∼g g∼f) ρ = + begin + ⟦ p ⟧ ⟨$⟩ ρ ≈˘⟨ cong ⟦ p ⟧ (f∼g ∘ ρ) ⟩ + ⟦ p ⟧ ⟨$⟩ (f ∘ (g ∘ ρ)) ≈˘⟨ comm-hom-term fh p (g ∘ ρ) ⟩ + f(⟦ p ⟧ᴬ ⟨$⟩ (g ∘ ρ)) ≈⟨ cong ∣ fh ∣ (Apq (g ∘ ρ)) ⟩ + f(⟦ q ⟧ᴬ ⟨$⟩ (g ∘ ρ)) ≈⟨ comm-hom-term fh q (g ∘ ρ) ⟩ + ⟦ q ⟧ ⟨$⟩ (f ∘ (g ∘ ρ)) ≈⟨ cong ⟦ q ⟧ (f∼g ∘ ρ) ⟩ + ⟦ q ⟧ ⟨$⟩ ρ ∎ where - private f = _⟨$⟩_ ∣ fh ∣ ; g = _⟨$⟩_ ∣ gh ∣ - open Environment 𝑨 using () renaming ( ⟦_⟧ to ⟦_⟧ᴬ ) - open Environment 𝑩 using ( ⟦_⟧ ) - open SetoidReasoning 𝔻[ 𝑩 ] + private f = _⟨$⟩_ ∣ fh ∣ ; g = _⟨$⟩_ ∣ gh ∣ + open Environment 𝑨 using () renaming ( ⟦_⟧ to ⟦_⟧ᴬ ) + open Environment 𝑩 using ( ⟦_⟧ ) + open SetoidReasoning 𝔻[ 𝑩 ] \end{code} Identities modeled by an algebra \ab{𝑨} are also modeled by every homomorphic image of @@ -1922,20 +1924,22 @@ then there exists an epimorphism from \Free{A} onto \ab{𝑨}. \begin{code} -module _ {𝑨 : Algebra (α ⊔ ρᵃ ⊔ ℓ) (α ⊔ ρᵃ ⊔ ℓ)} {𝒦 : Pred(Algebra α ρᵃ) (α ⊔ ρᵃ ⊔ ov ℓ)} where - open Setoid 𝔻[ 𝑨 ] using ( refl ; sym ; trans ) renaming ( Carrier to A ) - private c = α ⊔ ρᵃ ⊔ ℓ ; ι = ov c ; open FreeAlgebra {χ = c}(Th 𝒦) using ( 𝔽[_] ) +module _ {𝑨 : Algebra (α ⊔ ρᵃ ⊔ ℓ)(α ⊔ ρᵃ ⊔ ℓ)}{𝒦 : Pred(Algebra α ρᵃ)(α ⊔ ρᵃ ⊔ ov ℓ)} where + private c = α ⊔ ρᵃ ⊔ ℓ ; ι = ov c + open FreeAlgebra {χ = c}(Th 𝒦) using ( 𝔽[_] ) + open Setoid 𝔻[ 𝑨 ] using ( refl ; sym ; trans ) renaming ( Carrier to A ) + F-ModTh-epi : 𝑨 ∈ Mod (Th (V ℓ ι 𝒦)) → epi 𝔽[ A ] 𝑨 F-ModTh-epi A∈ModThK = φ , isEpi - where open FreeHom {ℓ = ℓ} {𝒦} - φ : 𝔻[ 𝔽[ A ] ] ⟶ 𝔻[ 𝑨 ] - _⟨$⟩_ φ = free-lift{𝑨 = 𝑨} id - cong φ {p} {q} pq = trans ( sym (free-lift-interp{𝑨 = 𝑨} id p) ) - ( trans ( A∈ModThK{p = p}{q} (kernel-in-theory pq) id ) - ( free-lift-interp{𝑨 = 𝑨} id q ) ) - isEpi : IsEpi 𝔽[ A ] 𝑨 φ - compatible (isHom isEpi) = cong (Interp 𝑨) (≡.refl , (λ _ → refl)) - isSurjective isEpi {y} = eq (ℊ y) refl + where open FreeHom {ℓ = ℓ} {𝒦} + φ : 𝔻[ 𝔽[ A ] ] ⟶ 𝔻[ 𝑨 ] + _⟨$⟩_ φ = free-lift{𝑨 = 𝑨} id + cong φ {p} {q} pq = trans ( sym (free-lift-interp{𝑨 = 𝑨} id p) ) + ( trans ( A∈ModThK{p = p}{q} (kernel-in-theory pq) id ) + ( free-lift-interp{𝑨 = 𝑨} id q ) ) + isEpi : IsEpi 𝔽[ A ] 𝑨 φ + compatible (isHom isEpi) = cong (Interp 𝑨) (≡.refl , (λ _ → refl)) + isSurjective isEpi {y} = eq (ℊ y) refl \end{code} \ifshort\else @@ -2011,7 +2015,7 @@ Therefore,\\[-4pt] \ab g (\af{⟦~\T{X}~⟧} \ab q) = \af{⟦~\Free{X}~⟧} \ab q,\\[8pt] so \ab{𝒦} \af{⊫} \ab p \af{≈} \ab q, thus (\ab p , \ab q) \af{∈} \af{Th} \ab{𝒦}. Since \ab{𝑨} \af{∈} \af{Mod} (\af{Th} \ab{𝒦}) = -\af{Mod} (\af{Th} \ab{𝒦}), we obtain \ab{𝑨} \af{⊧} \ab p \af{≈} \ab q, which implies +\af{Mod} (\af{Th} \ab{𝒦}), we obtain \ab{𝑨}~\af{⊧}~\ab p~\af{≈}~\ab q, which implies that \ab h \ab u = (\af{⟦~\ab{𝑨}~⟧} \ab p) \aofld{⟨\$⟩} \ab{ρ} = (\af{⟦~\ab{𝑨}~⟧} \ab q) \aofld{⟨\$⟩} \ab{ρ} = \ab h \ab v, as desired. @@ -2029,18 +2033,20 @@ classes \ab{𝒦}, is called the \defn{expansive} property of \af{V}. \begin{code} module _ (𝒦 : Pred(Algebra α ρᵃ) (α ⊔ ρᵃ ⊔ ov ℓ)) where + V-expa : 𝒦 ⊆ V ℓ (ov (α ⊔ ρᵃ ⊔ ℓ)) 𝒦 V-expa {x = 𝑨} kA = 𝑨 , (𝑨 , (⊤ , (λ _ → 𝑨) , (λ _ → kA), Goal), ≤-reflexive), IdHomImage where - open Setoid 𝔻[ 𝑨 ] using ( refl ) - open Setoid 𝔻[ ⨅ (λ _ → 𝑨) ] using () renaming ( refl to refl⨅ ) + open Setoid 𝔻[ 𝑨 ] using ( refl ) + open Setoid 𝔻[ ⨅ (λ _ → 𝑨) ] using () renaming ( refl to refl⨅ ) + to⨅ : 𝔻[ 𝑨 ] ⟶ 𝔻[ ⨅ (λ _ → 𝑨) ] - from⨅ : 𝔻[ ⨅ (λ _ → 𝑨) ] ⟶ 𝔻[ 𝑨 ] to⨅ = record { f = λ x _ → x ; cong = λ xy _ → xy } + from⨅ : 𝔻[ ⨅ (λ _ → 𝑨) ] ⟶ 𝔻[ 𝑨 ] from⨅ = record { f = λ x → x tt ; cong = λ xy → xy tt } Goal : 𝑨 ≅ ⨅ (λ x → 𝑨) - Goal = mkiso (to⨅ , mkhom refl⨅) (from⨅ , mkhom refl) (λ _ _ → refl) (λ _ → refl) + Goal = mkiso(to⨅ , mkhom refl⨅)(from⨅ , mkhom refl)(λ _ _ → refl)(λ _ → refl) \end{code} Observe how \ab{𝑨} is expressed as (isomorphic to) a product with just one factor (\ab{𝑨} itself); that is, the product @@ -2056,6 +2062,7 @@ class, then \af V \ab{𝒦} \aof{⊆} \ab{𝒦}, as we now confirm. module _ {ℓ : Level}{X : Type ℓ}{ℰ : {Y : Type ℓ} → Pred (Term Y × Term Y) (ov ℓ)} where private 𝒦 = Mod{α = ℓ}{ℓ}{X} ℰ -- an arbitrary equational class + EqCl⇒Var : V ℓ (ov ℓ) 𝒦 ⊆ 𝒦 EqCl⇒Var {𝑨} vA {p} {q} pℰq ρ = V-id1 ℓ {𝒦} {p} {q} (λ _ x τ → x pℰq τ) 𝑨 vA ρ @@ -2076,6 +2083,7 @@ consequence of the fact that \af{Mod} \af{Th} is a closure operator. module _ (𝒦 : Pred(Algebra α ρᵃ) (α ⊔ ρᵃ ⊔ ov ℓ)){X : Type (α ⊔ ρᵃ ⊔ ℓ)} where private c = α ⊔ ρᵃ ⊔ ℓ ; ι = ov c + ModTh-closure : V{β = β}{ρᵇ}{γ}{ρᶜ}{δ}{ρᵈ} ℓ ι 𝒦 ⊆ Mod{X = X} (Th (V ℓ ι 𝒦)) ModTh-closure {x = 𝑨} vA {p} {q} x ρ = x 𝑨 vA ρ @@ -2180,14 +2188,14 @@ We state and prove this in \agda as follows. open FreeHom {ℓ = ℓ}{𝒦} kerF⊆kerC : ker ∣ homF[ X ] ∣ ⊆ ker ∣ homC ∣ kerF⊆kerC {p , q} pKq (𝑨 , sA , ρ) = begin - free-lift ρ p ≈˘⟨ free-lift-interp {𝑨 = 𝑨} ρ p ⟩ - ⟦ p ⟧ ⟨$⟩ ρ ≈⟨ S-id1 {ℓ = ℓ} {p = p} {q} (ζ pKq) 𝑨 sA ρ ⟩ - ⟦ q ⟧ ⟨$⟩ ρ ≈⟨ free-lift-interp {𝑨 = 𝑨} ρ q ⟩ + free-lift ρ p ≈˘⟨ free-lift-interp {𝑨 = 𝑨} ρ p ⟩ + ⟦ p ⟧ ⟨$⟩ ρ ≈⟨ S-id1 {ℓ = ℓ} {p = p} {q} (ζ pKq) 𝑨 sA ρ ⟩ + ⟦ q ⟧ ⟨$⟩ ρ ≈⟨ free-lift-interp {𝑨 = 𝑨} ρ q ⟩ free-lift ρ q ∎ - where open Environment 𝑨 using ( ⟦_⟧ ) - open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) ; open SetoidReasoning 𝔻[ 𝑨 ] - ζ : ∀{p q} → (Th 𝒦) ⊢ X ▹ p ≈ q → 𝒦 ⊫ p ≈ q - ζ x 𝑨 kA = sound (λ y ρ → y 𝑨 kA ρ) x where open Soundness (Th 𝒦) 𝑨 + where open Environment 𝑨 using ( ⟦_⟧ ) + open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) ; open SetoidReasoning 𝔻[ 𝑨 ] + ζ : ∀{p q} → (Th 𝒦) ⊢ X ▹ p ≈ q → 𝒦 ⊫ p ≈ q + ζ x 𝑨 kA = sound (λ y ρ → y 𝑨 kA ρ) x where open Soundness (Th 𝒦) 𝑨 open FreeAlgebra{χ = c}(Th 𝒦) using ( 𝔽[_] ) homFC : hom 𝔽[ X ] 𝑪 @@ -2256,20 +2264,22 @@ This completes stage \ref{item:1} of the proof. \end{itemize} \begin{itemize} \item \ref{item:2}. We show that every algebra in \af{Mod} (\af{Th} (\af{V} -\ab{𝒦})) is a homomorphic image of \af{𝔽[~\ab{X}~]}, as follows. +\ab{𝒦})) is a homomorphic image of \af{𝔽[~\ab{X}~]}. \begin{code} module _ {𝒦 : Pred(Algebra α ρᵃ) (α ⊔ ρᵃ ⊔ ov ℓ)} where - private c = α ⊔ ρᵃ ⊔ ℓ ; ι = ov c ; open FreeAlgebra {χ = c}(Th 𝒦) using ( 𝔽[_] ) + private c = α ⊔ ρᵃ ⊔ ℓ ; ι = ov c + Var⇒EqCl : ∀ 𝑨 → 𝑨 ∈ Mod (Th (V ℓ ι 𝒦)) → 𝑨 ∈ V ℓ ι 𝒦 - Var⇒EqCl 𝑨 ModThA = 𝔽[ 𝕌[ 𝑨 ] ] , (spFA , Aim) + Var⇒EqCl 𝑨 ModThA = 𝔽[ 𝕌[ 𝑨 ] ] , (SPF{ℓ = ℓ} 𝒦 , Aim) where - spFA : 𝔽[ 𝕌[ 𝑨 ] ] ∈ S{ι} ι (P ℓ ι 𝒦) - spFA = SPF{ℓ = ℓ} 𝒦 + open FreeAlgebra {χ = c}(Th 𝒦) using ( 𝔽[_] ) epiFlA : epi 𝔽[ 𝕌[ 𝑨 ] ] (Lift-Alg 𝑨 ι ι) epiFlA = F-ModTh-epi-lift{ℓ = ℓ} (λ {p q} → ModThA{p = p}{q}) + φ : Lift-Alg 𝑨 ι ι IsHomImageOf 𝔽[ 𝕌[ 𝑨 ] ] φ = epi→ontohom 𝔽[ 𝕌[ 𝑨 ] ] (Lift-Alg 𝑨 ι ι) epiFlA + Aim : 𝑨 IsHomImageOf 𝔽[ 𝕌[ 𝑨 ] ] Aim = ∘-hom ∣ φ ∣(from Lift-≅), ∘-IsSurjective _ _ ∥ φ ∥(fromIsSurjective(Lift-≅{𝑨 = 𝑨}))