open import plfa.part1.Isomorphism using (_⇔_)
⇔≃× : ∀ {A B : Set} → A ⇔ B ≃ (A → B) × (B → A)
⇔≃× = record
  { to = λ a → ⟨ _⇔_.to a , _⇔_.from a ⟩
  ; from = λ ab → record { to = proj₁ ab ; from = proj₂ ab }
  ; from∘to = λ _ → refl
  ; to∘from = λ _ → refl
  }

⊎-comm : ∀ {A B : Set} → A ⊎ B ≃ B ⊎ A
⊎-comm = record
  { to = λ a+b → case-⊎ inj₂ inj₁ a+b
  ; from = λ b+a → case-⊎ inj₂ inj₁ b+a
  ; from∘to = λ
    { (inj₁ _) → refl
    ; (inj₂ _) → refl
    }
  ; to∘from = λ
    { (inj₁ _) → refl
    ; (inj₂ _) → refl
    }
  }

⊎-assoc : ∀ {A B C : Set} → (A ⊎ B) ⊎ C ≃ A ⊎ (B ⊎ C)
⊎-assoc = record
  { to = λ
    { (inj₁ (inj₁ x)) → inj₁ x
    ; (inj₁ (inj₂ x)) → inj₂ (inj₁ x)
    ; (inj₂ x)        → inj₂ (inj₂ x)
    }
  ; from = λ
    { (inj₁ x)        → inj₁ (inj₁ x)
    ; (inj₂ (inj₁ x)) → inj₁ (inj₂ x)
    ; (inj₂ (inj₂ x)) → inj₂ x
    }
  ; from∘to = λ
    { (inj₁ (inj₁ x)) → refl
    ; (inj₁ (inj₂ x)) → refl
    ; (inj₂ x)        → refl
    }
  ; to∘from = λ
    { (inj₁ x)        → refl
    ; (inj₂ (inj₁ x)) → refl
    ; (inj₂ (inj₂ x)) → refl
    }
  }

⊥-identityˡ : {A : Set} → ⊥ ⊎ A ≃ A
⊥-identityˡ = record
  { to = λ{ (inj₁ ()); (inj₂ a) → a }
  ; from = inj₂
  ; from∘to = λ
    { (inj₁ ())
    ; (inj₂ a) → refl
    }
  ; to∘from = λ _ → refl
  }

⊥-identityʳ : {A : Set} → A ⊎ ⊥ ≃ A
⊥-identityʳ = record
  { to = λ{ (inj₁ a) → a; (inj₂ ()) }
  ; from = inj₁
  ; from∘to = λ
    { (inj₁ a) → refl
    ; (inj₂ ())
    }
  ; to∘from = λ _ → refl
  }

⊎-weak-×' : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
⊎-weak-×' = λ
  { ⟨ inj₁ a , c ⟩ → inj₁ a
  ; ⟨ inj₂ b , c ⟩ → inj₂ ⟨ b , c ⟩
  }
-- This is similar to ×-distrib-⊎, but it throws away the `C` in inj₁ so it cannot be recovered back from it to form isomorphism

⊎×-implies-×⊎' : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
⊎×-implies-×⊎' = λ
  { (inj₁ ⟨ a , b ⟩) → ⟨ inj₁ a , inj₁ b ⟩
  ; (inj₂ ⟨ c , d ⟩) → ⟨ inj₂ c , inj₂ d ⟩
  }
-- ×⊎-implies-⊎× : ∀ {A B C D : Set} → (A ⊎ C) × (B ⊎ D) → (A × B) ⊎ (C × D)
-- ×⊎-implies-⊎× = λ
--   { ⟨ inj₁ a , inj₁ b ⟩ → inj₁ ⟨ a , b ⟩
--   ; ⟨ inj₁ a , inj₂ d ⟩ → {!!} -- cannot construct
--   ; ⟨ inj₂ c , inj₁ b ⟩ → {!!} -- cannot construct
--   ; ⟨ inj₂ c , inj₂ d ⟩ → inj₂ ⟨ c , d ⟩
--   }