From ab8c9aa7aa77fa82f3aed36fd663f0a6eea94172 Mon Sep 17 00:00:00 2001 From: wadler Date: Tue, 9 Jan 2018 20:08:39 -0200 Subject: [PATCH] trying to prove distribution --- src/Logic.lagda | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Logic.lagda b/src/Logic.lagda index 8e991b37..3e1434a0 100644 --- a/src/Logic.lagda +++ b/src/Logic.lagda @@ -166,14 +166,14 @@ Distribution of `×` over `⊎` is an isomorphism. ×-distributes-+ : ∀ {A B C : Set} → ((A ⊎ B) × C) ≃ ((A × C) ⊎ (B × C)) ×-distributes-+ = record { - to = λ { (inj₁ a , c) → inj₁ (a , c) ; - (inj₂ b , c) → inj₂ (b , c) } ; - fro = {!!} ; -- λ { inj₁ (a , c) → (inj₁ a , c) ; - -- inj₂ (b , c) → (inj₂ b , c) } ; - invˡ = {!!} ; -- λ { (inj₁ a , c) → refl ; - -- (inj₂ b , c) → refl } ; - invʳ = {!!} -- λ { inj₁ (a , c) → refl ; - -- inj₂ (b , c) → refl } + to = λ { (inj₁ a , c) → (inj₁ (a , c)) ; + (inj₂ b , c) → (inj₂ (b , c)) } ; + fro = λ { (inj₁ (a , c)) → (inj₁ a , c) ; + (inj₂ (b , c)) → (inj₂ b , c) } ; + invˡ = λ { (inj₁ a , c) → refl ; + (inj₂ b , c) → refl } ; + invʳ = λ { (inj₁ (a , c)) → refl ; + (inj₂ (b , c)) → refl } } \end{code}