michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

trying to prove distribution

Browse source
This commit is contained in:
wadler 2018-01-09 20:08:39 -02:00
parent bc9cd1934a
commit ab8c9aa7aa
1 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Logic.lagda
View file

@ -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}