From d70739091ed165d89670ef69cefd2a7d7bbc9f02 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Tue, 1 Aug 2023 18:17:18 +0200 Subject: [PATCH] Continued report about Transport Hell --- FFOLInitial.lagda | 142 ++------------------------------------------ Makefile | 2 +- report/M1Report.tex | 34 +++++++++++ report/header.tex | 27 +++++---- 4 files changed, 55 insertions(+), 150 deletions(-) diff --git a/FFOLInitial.lagda b/FFOLInitial.lagda index d2c60f3..d737eae 100644 --- a/FFOLInitial.lagda +++ b/FFOLInitial.lagda @@ -314,11 +314,6 @@ module FFOLInitial where wkₜσₚ : Subp {Δₜ} Δₚ' Δₚ → Subp {Δₜ ▹t⁰} (Δₚ' ▹tp) (Δₚ ▹tp) wkₜσₚ εₚ = εₚ wkₜσₚ {Δₜ = Δₜ} (_,ₚ_ {A = A} σₚ pf) = (wkₜσₚ σₚ) ,ₚ substP (λ Ξₚ → Pf (Δₜ ▹t⁰) Ξₚ (A [ wkₜσₜ idₜ ]f)) refl (_[_]pₜ {Γₜ = Δₜ ▹t⁰} pf (wkₜσₜ idₜ)) - {- - wkₚ[] : {σₜ : Subt Γₜ Δₜ} {σₚ : Subp Δₚ Δₚ'} {A : For Δₜ} → (wkₚσₚ {A = A} σₚ) [ σₜ ]σₚ ≡ wkₚσₚ (σₚ [ σₜ ]σₚ) - wkₚ[] {σₚ = εₚ} = refl - wkₚ[] {σₚ = σₚ ,ₚ x} = cong (λ ξ → ξ ,ₚ _) (wkₚ[] {σₚ = σₚ}) - -} _[_]p : {A : For Δₜ} → Pf Δₜ Δₚ A → (σ : Subp {Δₜ} Δₚ' Δₚ) → Pf Δₜ Δₚ' A var pvzero [ σ ,ₚ pf ]p = pf @@ -342,124 +337,6 @@ module FFOLInitial where εₚ ∘ₚ β = εₚ (α ,ₚ pf) ∘ₚ β = (α ∘ₚ β) ,ₚ (pf [ β ]p) - -- And now we have to show all their equalities - {- - idₚ[] : {σₜ : Subt Γₜ Δₜ} → ((idₚ {Δₜ} {Δₚ}) [ σₜ ]σₚ) ≡ idₚ {Γₜ} {Δₚ [ σₜ ]c} - idₚ[] {Δₚ = ◇p} = refl - idₚ[] {Δₚ = Δₚ ▹p⁰ A} = cong (λ ξ → ξ ,ₚ var pvzero) (≡tran wkₚ[] (cong wkₚσₚ idₚ[])) - -} - - -- Cancelling a wkₚσₚ with a ,ₚ - {- - wkₚ∘, : {Δₜ : Cont}{Γₚ Δₚ Ξₚ : Conp Δₜ}{α : Subp {Δₜ} Γₚ Δₚ}{β : Subp {Δₜ} Ξₚ Γₚ}{A : For Δₜ}{pf : Pf Δₜ Ξₚ A} → (wkₚσₚ α) ∘ₚ (β ,ₚ pf) ≡ (α ∘ₚ β) - wkₚ∘, {α = εₚ} = refl - wkₚ∘, {α = α ,ₚ pf} {β = β} {pf = pf'} = cong (λ ξ → ξ ,ₚ (pf [ β ]p)) wkₚ∘, - -} - - -- Categorical rules - {- - idlₚ : {Γₚ Δₚ : Conp Γₜ} {σₚ : Subp Γₚ Δₚ} → (idₚ {Δₚ = Δₚ}) ∘ₚ σₚ ≡ σₚ - idlₚ {Δₚ = ◇p} {εₚ} = refl - idlₚ {Δₚ = Δₚ ▹p⁰ pf} {σₚ ,ₚ pf'} = cong (λ ξ → ξ ,ₚ pf') (≡tran wkₚ∘, (idlₚ {σₚ = σₚ})) - idrₚ : {Γₚ Δₚ : Conp Γₜ} {σₚ : Subp Γₚ Δₚ} → σₚ ∘ₚ (idₚ {Δₚ = Γₚ}) ≡ σₚ - idrₚ {σₚ = εₚ} = refl - idrₚ {σₚ = σₚ ,ₚ prf} = cong (λ X → X ,ₚ prf) (idrₚ {σₚ = σₚ}) - ∘ₚ-ass : {Γₚ Δₚ Ξₚ Ψₚ : Conp Γₜ}{αₚ : Subp Γₚ Δₚ}{βₚ : Subp Δₚ Ξₚ}{γₚ : Subp Ξₚ Ψₚ} → (γₚ ∘ₚ βₚ) ∘ₚ αₚ ≡ γₚ ∘ₚ (βₚ ∘ₚ αₚ) - ∘ₚ-ass {γₚ = εₚ} = refl - ∘ₚ-ass {αₚ = αₚ} {βₚ} {γₚ ,ₚ x} = cong (λ ξ → ξ ,ₚ (x [ βₚ ∘ₚ αₚ ]p)) ∘ₚ-ass - - -- Unicity of the terminal morphism - εₚ-u : {Γₚ : Conp Γₜ} → {σ : Subp Γₚ ◇p} → σ ≡ εₚ {Δₚ = Γₚ} - εₚ-u {σ = εₚ} = refl - - -- Term substitution for proof substitutions - []σₚ-id : {σₚ : Subp {Δₜ} Δₚ Δₚ'} → coe (cong₂ Subp []c-id []c-id) (σₚ [ idₜ ]σₚ) ≡ σₚ - []σₚ-id {σₚ = εₚ} = εₚ-u - []σₚ-id {Δₜ}{Δₚ}{Δₚ' ▹p⁰ A} {σₚ = σₚ ,ₚ x} = - substP (λ ξ → coe (cong₂ Subp []c-id []c-id) (ξ ,ₚ (x [ idₜ ]pₜ)) ≡ (σₚ ,ₚ x)) - (≡sym (coeshift []σₚ-id)) - (≡sym (coeshift {eq = cong₂ Subp (≡sym []c-id) (≡sym []c-id)} - (substfpoly⁴ - {A = ((Conp Δₜ) × (Conp Δₜ)) × (For Δₜ)} - {P = λ W → Subp (proj×₁ (proj×₁ W)) ((proj×₂ (proj×₁ W)) ▹p⁰ (proj×₂ W))} - {R = λ W → Subp (proj×₁ (proj×₁ W)) (proj×₂ (proj×₁ W))} - {Q = λ W → Pf Δₜ (proj×₁ (proj×₁ W)) (proj×₂ W)} - {α = (Δₚ ,× Δₚ') ,× A} - {eq = ×≡ (×≡ (≡sym []c-id) (≡sym []c-id)) (≡sym []f-id)} - {f = λ {W} ξ pf → _,ₚ_ ξ pf}{x = σₚ}{y = x} - ))) - - []σₚ-∘ : {Ξₚ Ξₚ' : Conp Ξₜ}{α : Subt Δₜ Ξₜ} {β : Subt Γₜ Δₜ} {σₚ : Subp {Ξₜ} Ξₚ Ξₚ'} - → coe (cong₂ Subp (≡sym []c-∘) (≡sym []c-∘)) ((σₚ [ α ]σₚ) [ β ]σₚ) ≡ σₚ [ α ∘ₜ β ]σₚ - []σₚ-∘ {σₚ = εₚ} = εₚ-u - []σₚ-∘ {Ξₜ}{Δₜ}{Γₜ}{Ξₚ}{Δₚ' ▹p⁰ A}{α}{β}{σₚ = σₚ ,ₚ pf} = - substP (λ ξ → coe (cong₂ Subp (≡sym []c-∘) (≡sym []c-∘)) (ξ ,ₚ ((pf [ α ]pₜ) [ β ]pₜ)) ≡ ((σₚ [ α ∘ₜ β ]σₚ) ,ₚ (pf [ α ∘ₜ β ]pₜ))) (≡sym (coeshift []σₚ-∘)) - (≡sym (coeshift {eq = cong₂ Subp []c-∘ []c-∘} - (substfpoly⁴ - {A = ((Conp Γₜ) × (Conp Γₜ)) × (For Γₜ)} - {P = λ W → Subp (proj×₁ (proj×₁ W)) ((proj×₂ (proj×₁ W)) ▹p⁰ (proj×₂ W))} - {R = λ W → Subp (proj×₁ (proj×₁ W)) (proj×₂ (proj×₁ W))} - {Q = λ W → Pf Γₜ (proj×₁ (proj×₁ W)) (proj×₂ W)} - {eq = ×≡ (×≡ []c-∘ []c-∘) []f-∘} - {f = λ {W} ξ pf → _,ₚ_ ξ pf}{x = σₚ [ α ∘ₜ β ]σₚ}{y = pf [ α ∘ₜ β ]pₜ}) - )) - - -- How ∘ₚ and ∘ₜ interact to make associativity (to be proven later for Sub) - - ∘ₚₜ-ass⁰ : - {Γₜ Δₜ : Cont}{Γₚ : Conp Γₜ}{Δₚ : Conp Δₜ}{Ξₚ : Conp Δₜ}{Ψₚ : Conp Δₜ} - {αₜ : Subt Γₜ Δₜ}{γₚ : Subp Ξₚ Ψₚ}{βₚ : Subp Δₚ Ξₚ}{αₚ : Subp Γₚ (Δₚ [ αₜ ]c)} - → ((γₚ ∘ₚ βₚ) [ αₜ ]σₚ) ∘ₚ αₚ ≡ (γₚ [ αₜ ]σₚ) ∘ₚ ((βₚ [ αₜ ]σₚ) ∘ₚ αₚ) - ∘ₚₜ-ass⁰ {γₚ = εₚ} = refl - ∘ₚₜ-ass⁰ {αₜ = αₜ}{γₚ ,ₚ x}{βₚ}{αₚ} = cong (λ ξ → ξ ,ₚ (((x [ βₚ ]p) [ αₜ ]pₜ) [ αₚ ]p)) (∘ₚₜ-ass⁰ {γₚ = γₚ}) - - ∘ₚₜ-ass : - {Γₜ Δₜ Ξₜ Ψₜ : Cont}{Γₚ : Conp Γₜ}{Δₚ : Conp Δₜ}{Ξₚ : Conp Ξₜ}{Ψₚ : Conp Ψₜ} - {αₜ : Subt Γₜ Δₜ}{βₜ : Subt Δₜ Ξₜ}{γₜ : Subt Ξₜ Ψₜ}{γₚ : Subp Ξₚ (Ψₚ [ γₜ ]c)}{βₚ : Subp Δₚ (Ξₚ [ βₜ ]c)}{αₚ : Subp Γₚ (Δₚ [ αₜ ]c)} - {eq₁ : Subp Γₚ (Ψₚ [ (γₜ ∘ₜ βₜ) ∘ₜ αₜ ]c) ≡ Subp Γₚ (Ψₚ [ γₜ ∘ₜ (βₜ ∘ₜ αₜ) ]c)} - {eq₂ : Subp (Δₚ [ αₜ ]c) ((Ψₚ [ γₜ ∘ₜ βₜ ]c) [ αₜ ]c) ≡ Subp (Δₚ [ αₜ ]c) (Ψₚ [ (γₜ ∘ₜ βₜ) ∘ₜ αₜ ]c)} - {eq₃ : Subp (Ξₚ [ βₜ ∘ₜ αₜ ]c) ((Ψₚ [ γₜ ]c) [ βₜ ∘ₜ αₜ ]c) ≡ Subp (Ξₚ [ βₜ ∘ₜ αₜ ]c) (Ψₚ [ γₜ ∘ₜ (βₜ ∘ₜ αₜ) ]c)} - {eq₄ : Subp (Δₚ [ αₜ ]c) ((Ξₚ [ βₜ ]c) [ αₜ ]c) ≡ Subp (Δₚ [ αₜ ]c) (Ξₚ [ βₜ ∘ₜ αₜ ]c)} - {eq₅ : Subp (Ξₚ [ βₜ ]c) ((Ψₚ [ γₜ ]c) [ βₜ ]c) ≡ Subp (Ξₚ [ βₜ ]c) (Ψₚ [ γₜ ∘ₜ βₜ ]c)} - → coe eq₁ ((coe eq₂ (((coe eq₅ (γₚ [ βₜ ]σₚ)) ∘ₚ βₚ) [ αₜ ]σₚ)) ∘ₚ αₚ) ≡ (coe eq₃ (γₚ [ βₜ ∘ₜ αₜ ]σₚ)) ∘ₚ ((coe eq₄ (βₚ [ αₜ ]σₚ)) ∘ₚ αₚ) - ∘ₚₜ-ass {Γₜ}{Δₜ}{Ξₜ}{Ψₜ}{Γₚ}{Δₚ}{Ξₚ}{Ψₚ}{αₜ = αₜ}{βₜ}{γₜ}{γₚ}{βₚ}{αₚ}{eq₁}{eq₂}{eq₃}{eq₄}{eq₅} = - substP (λ X → coe eq₁ ((coe eq₂ (((coe eq₅ (γₚ [ βₜ ]σₚ)) ∘ₚ βₚ) [ αₜ ]σₚ)) ∘ₚ αₚ) ≡ (coe eq₃ X) ∘ₚ ((coe eq₄ (βₚ [ αₜ ]σₚ)) ∘ₚ αₚ)) []σₚ-∘ ( - ≡tran⁵ - (cong (coe eq₁) (≡tran ( - ≡sym (substfpoly - {R = λ X → Subp (Δₚ [ αₜ ]c) X} - {eq = ≡sym []c-∘} - {f = λ ξ → ξ ∘ₚ αₚ} - {x = ((coe eq₅ (γₚ [ βₜ ]σₚ)) ∘ₚ βₚ) [ αₜ ]σₚ})) - (cong (coe (cong (λ z → Subp Γₚ z) (≡sym []c-∘))) - (≡sym (substfpoly - {R = λ X → Subp (Ξₚ [ βₜ ]c) X} - {eq = ≡sym []c-∘} - {f = λ ξ → ((ξ ∘ₚ βₚ) [ αₜ ]σₚ) ∘ₚ αₚ} - {x = γₚ [ βₜ ]σₚ} - ))) - )) - (≡tran coecoe-coe coecoe-coe) - (cong (coe (≡tran (cong (λ z → Subp Γₚ (z [ αₜ ]c)) (≡sym []c-∘)) (≡tran (cong (λ z → Subp Γₚ z) (≡sym []c-∘)) eq₁))) ∘ₚₜ-ass⁰) - (≡sym coecoe-coe) - (cong (coe (cong (λ z → Subp Γₚ z) (≡sym []c-∘))) (substppoly - {A = (Conp Γₜ) × (Conp Γₜ)} - {R = λ W → Subp (proj×₁ W) (proj×₂ W)} - {Q = λ W → Subp (Δₚ [ αₜ ]c) (proj×₁ W)} - {eq = ×≡ (≡sym []c-∘) (≡sym []c-∘)} - {f = λ x y → x ∘ₚ (y ∘ₚ αₚ)} - {x = (γₚ [ βₜ ]σₚ) [ αₜ ]σₚ} - {y = βₚ [ αₜ ]σₚ} - ))(substfpoly - {R = λ X → Subp (Ξₚ [ βₜ ∘ₜ αₜ ]c) X} - {eq = ≡sym []c-∘} - {f = λ {τ} ξ → (ξ ∘ₚ ((coe eq₄ (βₚ [ αₜ ]σₚ)) ∘ₚ αₚ))} - {x = (coe (cong₂ Subp (≡sym []c-∘) (≡sym []c-∘)) ((γₚ [ βₜ ]σₚ) [ αₜ ]σₚ))} - )) - -} - - - @@ -483,6 +360,8 @@ module FFOLInitial where field t : Subt (Con.t Γ) (Con.t Δ) p : Subp {Con.t Γ} (Con.p Γ) ((Con.p Δ) [ t ]c) + + -- We need this to apply term-substitution theorems to global substitutions sub= : {Γ Δ : Con}{σₜ σₜ' : Subt (Con.t Γ) (Con.t Δ)} → σₜ ≡ σₜ' → {σₚ : Subp {Con.t Γ} (Con.p Γ) ((Con.p Δ) [ σₜ ]c)} @@ -495,16 +374,7 @@ module FFOLInitial where id {Γ} = sub idₜ (substP (Subp _) (≡sym []c-id) idₚ) _∘_ : Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ sub αₜ αₚ ∘ sub βₜ βₚ = sub (αₜ ∘ₜ βₜ) (substP (Subp _) (≡sym []c-∘) (αₚ [ βₜ ]σₚ) ∘ₚ βₚ) - idl : {Γ Δ : Con} {σ : Sub Γ Δ} → (id {Δ}) ∘ σ ≡ σ - idl = sub= idlₜ - idr : {Γ Δ : Con} {σ : Sub Γ Δ} → σ ∘ (id {Γ}) ≡ σ - idr = sub= idrₜ - ∘-ass : {Γ Δ Ξ Ψ : Con}{α : Sub Γ Δ}{β : Sub Δ Ξ}{γ : Sub Ξ Ψ} → (γ ∘ β) ∘ α ≡ γ ∘ (β ∘ α) - ∘-ass = sub= ∘ₜ-ass - ◇ : Con - ◇ = con ◇t ◇p - -- We have our two context extension operators _▹t : Con → Con @@ -554,11 +424,11 @@ module FFOLInitial where { Con = Con ; Sub = Sub ; _∘_ = _∘_ - ; ∘-ass = λ {Γ}{Δ}{Ξ}{Ψ}{α}{β}{γ} → ∘-ass {Γ}{Δ}{Ξ}{Ψ}{α}{β}{γ} + ; ∘-ass = sub= ∘ₜ-ass ; id = id - ; idl = idl - ; idr = idr - ; ◇ = ◇ + ; idl = sub= idlₜ + ; idr = sub= idrₜ + ; ◇ = con ◇t ◇p ; ε = sub εₜ εₚ ; ε-u = sub= εₜ-u ; Tm = λ Γ → Tm (Con.t Γ) diff --git a/Makefile b/Makefile index 2206ba0..3e632c7 100644 --- a/Makefile +++ b/Makefile @@ -35,7 +35,7 @@ agda-tex-FIni: latex/FFOLInitial.tex @$(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\]\\AgdaFunction{idl}\\AgdaSpace{}') + @$(call extract,latex/FFOLInitial.tex,report/agda/IIdComp.tex,'(Con,Sub)\\ is\\ a\\ category\\ with\\ an\\ initial\\ object','\\AgdaEmptyExtraSkip') @$(call extract,latex/FFOLInitial.tex,report/agda/ICExt.tex,'We\\ have\\ our\\ two\\ context\\ extension\\ operators','\\AgdaEmptyExtraSkip') agda-tex-FFOL: latex/FFOL.tex diff --git a/report/M1Report.tex b/report/M1Report.tex index cef44ec..8f2d1af 100644 --- a/report/M1Report.tex +++ b/report/M1Report.tex @@ -293,6 +293,7 @@ \begin{tcolorbox} \vspace{-2ex} \agda{agda/IIdComp.tex} + \vspace{-3ex} \agdasep \agda{agda/ICExt.tex} \vspace{-7.5ex} @@ -301,6 +302,39 @@ \subsection{Transport Hell} \label{sec:transport-hell} + + In order for you to understand the code, i have to explain what are transport. I'll do this with the example of the definition of \AgdaFunction{id}. + To construct it, we will use \AgdaFunction{idₜ} and \AgdaFunction{id${}ₚ$}, merged together with the constructor \AgdaInductiveConstructor{sub}. Here are the types of the different elements in an array. + + \begin{center} + \renewcommand{\arraystretch}{1.2} + \begin{tabular}{l|l} + \AgdaFunction{id} & \AgdaRecord{Sub} (\AgdaInductiveConstructor{con} Γₜ Γₚ) (\AgdaInductiveConstructor{con} Γₜ Γₚ) \\\hline + \AgdaFunction{idₜ} & \AgdaDatatype{Subt} Γₜ Γₜ \\ + \AgdaFunction{idₚ} & \AgdaDatatype{Subp} Γₚ Γₚ \\ + \AgdaInductiveConstructor{sub} & (σ : \AgdaDatatype{Subt} Γₜ Δₜ) \\ + & \AgdaSymbol{$\rightarrow$} \AgdaDatatype{Subp} Γₚ (Δₚ[σ]c) \\ + & \AgdaSymbol{$\rightarrow$} \AgdaRecord{Sub} (\AgdaInductiveConstructor{con} Γₜ Γₚ) (\AgdaInductiveConstructor{con} Δₜ Δₚ) \\ + \end{tabular} + \end{center} + + But if we try to construct \AgdaFunction{id}, then we will eventually end up with the following goal: + + \begin{center} + \AgdaFunction{id} = \AgdaInductiveConstructor{sub} \AgdaFunction{idₜ} \textbf{?} $\implies$ \textbf{?} : \AgdaDatatype{Subp} Γₚ (Γₚ[\AgdaFunction{idₜ}]c) + \end{center} + + But then agda will complain if we give it as a goal the expression \enquote{\AgdaFunction{idₚ}}. Indeed, it is not trivial for them that \AgdaDatatype{Subp} Γₚ (Γₚ[\AgdaFunction{idₜ}]c) is the same as \AgdaDatatype{Subp} Γₚ Γₚ. Even if we can easily prove the equality between those two elements of \AgdaPrimitive{Prop} (the proof of the equality is derived from the fact that Conp is a functor from $\textbf{Cont}$ to $\bSet$, and therefore it has to respect the identity of $\textbf{Conp}$). + + That's where transports comes in. Its definition is as follows: + + \begin{center} + \AgdaFunction{substP} : \{A : \AgdaPrimitive{Set}\}(P : A → \AgdaPrimitive{Prop})\{a a' : A\} → a ≡ a' → P a → P a' + \end{center} + + This is exactly the thing that will solve our problem. With the equality between the two elements of \AgdaPrimitive{Prop}, we can now convert \AgdaFunction{idₚ} to something that will correctly match the goal required by Agda. + + This section is called \enquote{Transport Hell} because those transports between equal sets can get really annoying. In former version of the syntax, the \AgdaDatatype{Subp} were \AgdaPrimitive{Set}s instead of \AgdaPrimitive{Prop}s. And that created a lot of equalities related to polymorphic functions (quite all \AgdaDatatype{Subp}'s related functions were then polymorphic, as they would depend on proof contexts). And to solve those equalities, you have to extract what are precisely the polymorphic functions you are working with. You can see those proofs on \href{https://github.com/MysaaJava/m1-internship/commit/2728c60633a80631ed7b61bbfae5c81a1e0e193a#diff-99bc55bebd36ad0afbae3c6448793992086091c5b6b25973f73dd779690d7dd2}{former versions of the syntax}, they are really long and not interesting (as it is basically trying to tweak our equation so that Agda understands that two types are equal). \section{Summary} diff --git a/report/header.tex b/report/header.tex index 29153b9..87c97a1 100644 --- a/report/header.tex +++ b/report/header.tex @@ -33,6 +33,7 @@ \usepackage[page,header]{appendix} \usepackage{minitoc} \usepackage{mathtools} +\usepackage{textgreek} \usepackage{geometry} @@ -111,24 +112,24 @@ \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}}} -\newunicodechar{δ}{\ensuremath{\mathnormal{\delta}}} -\newunicodechar{ε}{\ensuremath{\mathnormal{\varepsilon}}} -\newunicodechar{σ}{\ensuremath{\mathnormal{\sigma}}} -\newunicodechar{π}{\ensuremath{\mathnormal{\pi}}} -\newunicodechar{λ}{\ensuremath{\mathnormal{\lambda}}} +\newunicodechar{Γ}{\textGamma} +\newunicodechar{Δ}{\textDelta} +\newunicodechar{Ξ}{\textXi} +\newunicodechar{α}{\textalpha} +\newunicodechar{β}{\textbeta} +\newunicodechar{γ}{\textgamma} +\newunicodechar{δ}{\textdelta} +\newunicodechar{ε}{\textvarepsilon} +\newunicodechar{σ}{\textsigma} +\newunicodechar{π}{\textpi} +\newunicodechar{λ}{\textlambda} \newunicodechar{▹}{\ensuremath{\mathnormal{\triangleright}}} \newunicodechar{⊢}{\ensuremath{\mathnormal{\vdash}}} \newunicodechar{⇒}{\ensuremath{\mathnormal{\Rightarrow}}} \newunicodechar{∀}{\ensuremath{\mathnormal{\forall}}} \newunicodechar{≈}{\ensuremath{\mathnormal{\approx}}} -\newunicodechar{ₜ}{\ensuremath{{}_t}} -\newunicodechar{ₚ}{\ensuremath{{}_p}} +\newunicodechar{ₜ}{\ensuremath{{}_\text{t}}} +\newunicodechar{ₚ}{\ensuremath{{}_\text{p}}} \newunicodechar{⁰}{\ensuremath{{}^0}}