From 08a5c303d6f9c9bcf33536d338cdffedfe369a6a Mon Sep 17 00:00:00 2001 From: Ayberk Tosun Date: Fri, 18 Aug 2023 16:05:40 +0100 Subject: [PATCH] Align --- source/EffectfulForcing/Internal/InternalModCont.lagda | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/source/EffectfulForcing/Internal/InternalModCont.lagda b/source/EffectfulForcing/Internal/InternalModCont.lagda index 8fd98ea68..2ef483ad2 100644 --- a/source/EffectfulForcing/Internal/InternalModCont.lagda +++ b/source/EffectfulForcing/Internal/InternalModCont.lagda @@ -160,7 +160,7 @@ max-question₀ : D ℕ ℕ ℕ → (ℕ → ℕ) → ℕ max-question₀ d α = maximum (pr₁ (dialogue-continuity d α)) max-question₀-agreement : (d : D ℕ ℕ ℕ) (α : ℕ → ℕ) - → max-question d α = max-question₀ d α + → max-question d α = max-question₀ d α max-question₀-agreement (D.η n) α = refl max-question₀-agreement (D.β φ n) α = ap (max n) (max-question₀-agreement (φ (α n)) α) @@ -172,7 +172,7 @@ max-questionᵀ : {Γ : Cxt} → Γ ⊢ (⌜B⌝ ι ι) ⇒ baire ⇒ ι max-questionᵀ = ƛ (ƛ (ν₁ · ƛ Zero · ƛ (ƛ (maxᵀ · ν₀ · (ν₁ · (ν₂ · ν₀)))))) max-question⋆-agreement : (d : D ℕ ℕ ℕ) (α : ℕ → ℕ) - → max-question d α = max-question⋆ (church-encode d) α + → max-question d α = max-question⋆ (church-encode d) α max-question⋆-agreement (D.η n) α = refl max-question⋆-agreement (D.β φ n) α = † where @@ -185,7 +185,8 @@ max-question⋆-agreement (D.β φ n) α = † † = ap (max n) IH max-questionᵀ-agreement-with-max-question⋆ : (d : 〈〉 ⊢ ⌜D⋆⌝ ι ι ι ι) (α : ℕ → ℕ) - → ⟦ max-questionᵀ · d ⟧₀ α = max-question⋆ ⟦ d ⟧₀ α + → ⟦ max-questionᵀ · d ⟧₀ α + = max-question⋆ ⟦ d ⟧₀ α max-questionᵀ-agreement-with-max-question⋆ d α = ap (⟦ d ⟧₀ (λ _ → 0))