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:05:52 -02:00
parent 3d919975fa
commit bc9cd1934a
1 changed files with 11 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/Logic.lagda
View file

@ -163,31 +163,18 @@ and `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`.
Distribution of `×` over `⊎` is an isomorphism.
\begin{code}
{-
data _≃_ : Set → Set → Set where
mk-≃ : ∀ {A B : Set} → (f : A → B) → (g : B → A) →
(∀ (x : A) → g (f x) ≡ x) → (∀ (y : B) → f (g y) ≡ y) → A ≃ B
×-distributes-+ : ∀ {A B C : Set} → ((A ⊎ B) × C) ≃ ((A × C) ⊎ (B × C))
×-distributes-+ = mk-≃ f g gf fg
where
f : ∀ {A B C : Set} → (A ⊎ B) × C → (A × C) ⊎ (B × C)
f (inj₁ a , c) = inj₁ (a , c)
f (inj₂ b , c) = inj₂ (b , c)
g : ∀ {A B C : Set} → (A × C) ⊎ (B × C) → (A ⊎ B) × C
g (inj₁ (a , c)) = (inj₁ a , c)
g (inj₂ (b , c)) = (inj₂ b , c)
gf : ∀ {A B C : Set} → (x : (A ⊎ B) × C) → g (f x) ≡ x
gf (inj₁ a , c) = refl
gf (inj₂ b , c) = refl
fg : ∀ {A B C : Set} → (y : (A × C) ⊎ (B × C)) → f (g y) ≡ y
fg (inj₁ (a , c)) = refl
fg (inj₂ (b , c)) = refl
-}
×-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 }
}
\end{code}
Distribution of `⊎` over `×` is half an isomorphism.