open import Agda.Primitive

infixr 1 _∨_
data _∨_ {ℓa ℓb} (A : Set ℓa) (B : Set ℓb) : Set (ℓa ⊔ ℓb) where
  inj₁ : A → A ∨ B
  inj₂ : B → A ∨ B

infixr 2 _∧_
data _∧_ {ℓa ℓb} (A : Set ℓa) (B : Set ℓb) : Set (ℓa ⊔ ℓb) where
  _,_ : A → B → A ∧ B

data ⊥ : Set where

⊥-elim : ∀ {ℓ} {A : Set ℓ} → ⊥ → A
⊥-elim ()

infix 3 ¬_
¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ A = A → ⊥

infixr 1 _∨ᶜ_
_∨ᶜ_ : ∀ {ℓa ℓb} → Set ℓa → Set ℓb → Set (ℓa ⊔ ℓb)
A ∨ᶜ B = ¬ (¬ A ∧ ¬ B)

lem : ∀ {ℓ} → (op : ∀ {ℓ ℓ'} → Set ℓ → Set ℓ' → Set (ℓ ⊔ ℓ')) → Set (lsuc ℓ)
lem {ℓ} op = ∀ {A : Set ℓ} → op A (¬ A)

lemᶜ : ∀ {ℓ} → lem {ℓ} _∨ᶜ_
lemᶜ (¬p , ¬¬p) = ¬¬p ¬p

∨-stronger-∨ᶜ : ∀ {ℓa ℓb} {A : Set ℓa} {B : Set ℓb} → A ∨ B → A ∨ᶜ B
∨-stronger-∨ᶜ (inj₁ x) (p , _) = p x
∨-stronger-∨ᶜ (inj₂ x) (_ , p) = p x

infixr 1 _∨ᵈ_
_∨ᵈ_ : ∀ {ℓa ℓb} → Set ℓa → Set ℓb → Set (ℓa ⊔ ℓb)
A ∨ᵈ B = ((A → B) → B) ∧ ((B → A) → A)

∨ᵈ-stronger-∨ᶜ : ∀ {ℓa ℓb} {A : Set ℓa} {B : Set ℓb} → A ∨ᵈ B → A ∨ᶜ B
∨ᵈ-stronger-∨ᶜ (p , q) (¬A , ¬B) = ¬A (q (λ b → ⊥-elim (¬B b)))

∨-stronger-∨ᵈ : ∀ {ℓa ℓb} {A : Set ℓa} {B : Set ℓb} → A ∨ B → A ∨ᵈ B
∨-stronger-∨ᵈ (inj₁ x) = (λ p → p x) , λ _ → x
∨-stronger-∨ᵈ (inj₂ x) = (λ _ → x) , λ q → q x

linearity : ∀ {ℓa ℓb} → (op : ∀ {ℓ ℓ'} → Set ℓ → Set ℓ' → Set (ℓ ⊔ ℓ')) → Set (lsuc (ℓa ⊔ ℓb))
linearity {ℓa} {ℓb} op = ∀ {A : Set ℓa} {B : Set ℓb} → op (A → B) (B → A)

linearity-∨ᵈ : ∀ {ℓa ℓb} → linearity {ℓa} {ℓb} _∨ᵈ_
linearity-∨ᵈ = (λ p b → p (λ _ → b) b) , (λ p a → p (λ _ → a) a)

∨ᵈ-stronger-∨-linearity : ∀ {ℓa ℓb} {A : Set ℓa} {B : Set ℓb} → linearity {ℓa} {ℓb} _∨_ → A ∨ᵈ B → A ∨ B
∨ᵈ-stronger-∨-linearity {A = A} {B = B} l (p , q) with l {A} {B}
... | inj₁ x = inj₂ (p x)
... | inj₂ x = inj₁ (q x)