From 3e07764efe93e8ce2b478c997ae95ab7c16f27ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Thu, 20 Jun 2019 14:00:41 +0200 Subject: [PATCH] Quantitative: fixes a spelling error --- extra/qtt/Quantitative.lagda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/extra/qtt/Quantitative.lagda b/extra/qtt/Quantitative.lagda index 2edef911..f9cbf3ef 100644 --- a/extra/qtt/Quantitative.lagda +++ b/extra/qtt/Quantitative.lagda @@ -695,7 +695,7 @@ lem-case⊗ {γ} {δ} Γ {A} {B} {Ξ} = (1# *̇ 0s , 1# * 0# ∙ A , 1# * 1# ∙ B) +̇ ((1# *̇ 0s , 1# * 1# ∙ A , 1# * 0# ∙ B) +̇ Γ *⟩ (λ x → Ξ x , 0# ∙ A , 0# ∙ B)) - -- Step 1. Move the three occurences of A and B to the top-level. + -- Step 1. Move the three occurrences of A and B to the top-level. ≡⟨ trans (*⟩-zeroʳ Γ (λ x → Ξ x , 0# ∙ A)) (*⟩-zeroʳ Γ Ξ |> cong (_, 0# ∙ B)) |> cong (((1# *̇ 0s , 1# * 0# ∙ A , 1# * 1# ∙ B) +̇_) ∘ ((1# *̇ 0s , 1# * 1# ∙ A , 1# * 0# ∙ B) +̇_)) ⟩