{-# OPTIONS --universe-polymorphism #-}
module Relation.Binary.Logical where

open import Level

⟦Set⟧ : ∀ {a₁ a₂} aᵣ (A₁ : Set a₁) (A₂ : Set a₂) → Set _
⟦Set⟧ aᵣ A₁ A₂ = A₁ → A₂ → Set aᵣ

⟦Set₀⟧ : ∀ (A₁ A₂ : Set) → Set₁
⟦Set₀⟧ = ⟦Set⟧ zero

⟦Set₁⟧ : ∀ (A₁ A₂ : Set₁) → Set₂
⟦Set₁⟧ = ⟦Set⟧ (suc zero)

⟦Π⟧ : ∀ {a₁ a₂ aᵣ} {A₁ : Set a₁} {A₂ : Set a₂} (Aᵣ : A₁ → A₂ → Set aᵣ)
         {b₁ b₂ bᵣ} {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂} (Bᵣ : ∀ {x₁ x₂} (xᵣ : Aᵣ x₁ x₂) → B₁ x₁ → B₂ x₂ → Set bᵣ)
         (f₁ : (x : A₁) → B₁ x) (f₂ : (x : A₂) → B₂ x) → Set _
⟦Π⟧ Aᵣ Bᵣ = λ f₁ f₂ → ∀ {x₁ x₂} (xᵣ : Aᵣ x₁ x₂) → Bᵣ xᵣ (f₁ x₁) (f₂ x₂)

infixr 0 ⟦Π⟧
syntax ⟦Π⟧ Aᵣ (λ xᵣ → f) = ⟨ xᵣ ∶ Aᵣ ⟩⟦→⟧ f

⟦Π⟧e : ∀ {a₁ a₂ aᵣ} {A₁ : Set a₁} {A₂ : Set a₂} (Aᵣ : A₁ → A₂ → Set aᵣ)
         {b₁ b₂ bᵣ} {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂} (Bᵣ : ∀ {x₁ x₂} (xᵣ : Aᵣ x₁ x₂) → B₁ x₁ → B₂ x₂ → Set bᵣ)
         (f₁ : (x : A₁) → B₁ x) (f₂ : (x : A₂) → B₂ x) → Set _
⟦Π⟧e Aᵣ Bᵣ = λ f₁ f₂ → ∀ x₁ x₂ (xᵣ : Aᵣ x₁ x₂) → Bᵣ xᵣ (f₁ x₁) (f₂ x₂)

{-
⟦∀⟧ : ∀ {a₁ a₂ aᵣ}
         {b₁ b₂ bᵣ} {B₁ : (A₁ : Set a₁) → Set b₁} {B₂ : (A₂ : Set a₂) → Set b₂}
                   (Bᵣ : ∀ {A₁ A₂} (Aᵣ : A₁ → A₂ → Set aᵣ) → B₁ A₁ → B₂ A₂ → Set bᵣ)
         (f₁ : {A₁ : Set a₁} → B₁ A₁) (f₂ : {A₂ : Set a₂} → B₂ A₂) → Set _
⟦∀⟧ Bᵣ = λ f₁ f₂ → ∀ {A₁ A₂} (Aᵣ : A₁ → A₂ → Set _) → Bᵣ Aᵣ (f₁ {A₁}) (f₂ {A₂})
-}

⟦∀⟧ : ∀ {a₁ a₂ aᵣ} {A₁ : Set a₁} {A₂ : Set a₂} (Aᵣ : A₁ → A₂ → Set aᵣ)
         {b₁ b₂ bᵣ} {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂} (Bᵣ : ∀ {x₁ x₂} (xᵣ : Aᵣ x₁ x₂) → B₁ x₁ → B₂ x₂ → Set bᵣ)
         (f₁ : {x : A₁} → B₁ x) (f₂ : {x : A₂} → B₂ x) → Set _
⟦∀⟧ Aᵣ Bᵣ = λ f₁ f₂ → ∀ {x₁ x₂} (xᵣ : Aᵣ x₁ x₂) → Bᵣ xᵣ (f₁ {x₁}) (f₂ {x₂})

infixr 0 ⟦∀⟧
syntax ⟦∀⟧ Aᵣ (λ xᵣ → f) = ∀⟨ xᵣ ∶ Aᵣ ⟩⟦→⟧ f

infixr 1 _⟦→⟧_
_⟦→⟧_ : ∀ {a₁ a₂ aᵣ} {A₁ : Set a₁} {A₂ : Set a₂} (Aᵣ : A₁ → A₂ → Set aᵣ)
          {b₁ b₂ bᵣ} {B₁ : Set b₁} {B₂ : Set b₂} (Bᵣ : B₁ → B₂ → Set bᵣ)
          (f₁ : A₁ → B₁) (f₂ : A₂ → B₂) → Set _
Aᵣ ⟦→⟧ Bᵣ = ⟦Π⟧ Aᵣ (λ _ → Bᵣ)

infixr 0 _⟦→⟧e_
_⟦→⟧e_ : ∀ {a₁ a₂ aᵣ} {A₁ : Set a₁} {A₂ : Set a₂} (Aᵣ : A₁ → A₂ → Set aᵣ)
          {b₁ b₂ bᵣ} {B₁ : Set b₁} {B₂ : Set b₂} (Bᵣ : B₁ → B₂ → Set bᵣ)
          (f₁ : A₁ → B₁) (f₂ : A₂ → B₂) → Set _
_⟦→⟧e_ Aᵣ Bᵣ = ⟦Π⟧e Aᵣ (λ _ → Bᵣ)

open import Data.Product


open import Data.Unit

record ⟦⊤⟧ (x₁ x₂ : ⊤) : Set where
  constructor ⟦tt⟧

open import Data.Empty

data ⟦⊥⟧ (x₁ x₂ : ⊥) : Set where

open import Relation.Nullary

infix 3 ⟦¬⟧_

--⟦¬⟧_ : (⟦Set⟧ ⟦→⟧ ⟦Set⟧) ¬_ ¬_
⟦¬⟧_ : ∀ {a₁ a₂ aᵣ} {A₁ : Set a₁} {A₂ : Set a₂} (Aᵣ : A₁ → A₂ → Set aᵣ) → ¬ A₁ → ¬ A₂ → Set _
⟦¬⟧ Aᵣ = Aᵣ ⟦→⟧ ⟦⊥⟧

{-
⟦∃⟧ : {A₁ A₂ : World → Set} (Aᵣ : ∀ {α₁ α₂} → ⟦World⟧ α₁ α₂ → A₁ α₁ → A₂ α₂ → Set)
       (p₁ : ∃ A₁) (f₂ : ∃ A₂) → Set
⟦∃⟧ Aᵣ = λ p₁ p₂ → Σ[ αᵣ ∶ ⟦World⟧ (proj₁ p₁) (proj₁ p₂) ]
                       (Aᵣ αᵣ (proj₂ p₁) (proj₂ p₂))

syntax ⟦∃⟧ (λ αᵣ → f) = ⟦∃⟧[ αᵣ ] f
-}

Pred : ∀ ℓ {a} (A : Set a) → Set (a ⊔ suc ℓ)
Pred ℓ A = A → Set ℓ

⟦Pred⟧ : ∀ {p₁ p₂} pᵣ {a₁ a₂ aᵣ} → (⟦Set⟧ {a₁} {a₂} aᵣ ⟦→⟧ ⟦Set⟧ _) (Pred p₁) (Pred p₂)
--⟦Pred⟧ {p₁} {p₂} pᵣ Aᵣ = Aᵣ ⟦→⟧ ⟦Set⟧ (p₁ ⊔ p₂ ⊔ pᵣ)
⟦Pred⟧ {p₁} {p₂} pᵣ Aᵣ = λ f₁ f₂ → ∀ {x₁} {x₂} (xᵣ : Aᵣ x₁ x₂) → f₁ x₁ → f₂ x₂ → Set (p₁ ⊔ p₂ ⊔ pᵣ)

open import Relation.Binary

private
  REL′ : ∀ ℓ {a b} → Set a → Set b → Set (a ⊔ b ⊔ suc ℓ)
  REL′ ℓ A B = A → B → Set ℓ

  ⟦REL⟧′ : ∀ {a₁ a₂ aᵣ b₁ b₂ bᵣ ℓ₁ ℓ₂} ℓᵣ →
          (⟦Set⟧ {a₁} {a₂} aᵣ ⟦→⟧ ⟦Set⟧ {b₁} {b₂} bᵣ ⟦→⟧ ⟦Set⟧ _) (REL′ ℓ₁) (REL′ ℓ₂)
  ⟦REL⟧′ ℓᵣ Aᵣ Bᵣ = Aᵣ ⟦→⟧ Bᵣ ⟦→⟧ (⟦Set⟧ ℓᵣ)

⟦REL⟧ : ∀ {a₁ a₂ aᵣ} {A₁ : Set a₁} {A₂ : Set a₂} (Aᵣ : A₁ → A₂ → Set aᵣ)
          {b₁ b₂ bᵣ} {B₁ : Set b₁} {B₂ : Set b₂} (Bᵣ : B₁ → B₂ → Set bᵣ)
          {ℓ₁ ℓ₂} ℓᵣ (∼₁ : REL A₁ B₁ ℓ₁) (∼₂ : REL A₂ B₂ ℓ₂) → Set _
⟦REL⟧ Aᵣ Bᵣ ℓᵣ = Aᵣ ⟦→⟧ Bᵣ ⟦→⟧ (⟦Set⟧ ℓᵣ)

⟦Rel⟧ : ∀ {a₁ a₂ aᵣ} {A₁ : Set a₁} {A₂ : Set a₂} (Aᵣ : A₁ → A₂ → Set aᵣ)
          {ℓ₁ ℓ₂} ℓᵣ (∼₁ : Rel A₁ ℓ₁) (∼₂ : Rel A₂ ℓ₂) → Set _
⟦Rel⟧ Aᵣ ℓᵣ = ⟦REL⟧ Aᵣ Aᵣ ℓᵣ

-- data ⟦Dec⟧ {ℓ₁ ℓ₂ ℓᵣ} {P₁ : Set ℓ₁} {P₂ : Set ℓ₂} (Pᵣ : P₁ → P₂ → Set ℓᵣ) : Dec P₁ → Dec P₂ → Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓᵣ) where
-- data ⟦Dec⟧ {ℓᵣ} : ⟦Pred⟧ (⟦Set⟧ ℓᵣ) ℓᵣ Dec Dec where
data ⟦Dec⟧ {ℓ₁ ℓ₂ ℓᵣ} {P₁ : Set ℓ₁} {P₂ : Set ℓ₂} (Pᵣ : P₁ → P₂ → Set ℓᵣ) : ⟦Set⟧ (ℓ₁ ⊔ ℓ₂ ⊔ ℓᵣ) (Dec P₁) (Dec P₂) where
  yes : {-∀ {P₁ P₂ Pᵣ}-} {p₁ : P₁} {p₂ : P₂} (pᵣ : Pᵣ p₁ p₂) → ⟦Dec⟧ Pᵣ (yes p₁) (yes p₂)
  no  : {-∀ {P₁ P₂ Pᵣ}-} {¬p₁ : ¬ P₁} {¬p₂ : ¬ P₂} (¬pᵣ : (⟦¬⟧ Pᵣ) ¬p₁ ¬p₂) → ⟦Dec⟧ Pᵣ (no ¬p₁) (no ¬p₂)

--⟦Decidable⟧ : ∀ {a₁ a₂ aᵣ b₁ b₂ bᵣ ℓ₁ ℓ₂ ℓᵣ} → (∀⟨ Aᵣ ∶ ⟦Set⟧ {a₁} {a₂} aᵣ ⟩⟦→⟧ ∀⟨ Bᵣ ∶ ⟦Set⟧ {b₁ b₂} bᵣ ⟩⟦→⟧ ⟦REL⟧ Aᵣ Bᵣ {ℓ₁} {ℓ₂} ℓᵣ ⟦→⟧ ⟦Set⟧ _) Decidable Decidable
⟦Decidable⟧ : ∀ {a₁ a₂ aᵣ} {A₁ : Set a₁} {A₂ : Set a₂} (Aᵣ : A₁ → A₂ → Set aᵣ)
                 {b₁ b₂ bᵣ} {B₁ : Set b₁} {B₂ : Set b₂} (Bᵣ : B₁ → B₂ → Set bᵣ)
                 {ℓ₁ ℓ₂ ℓᵣ} {∼₁ : REL A₁ B₁ ℓ₁} {∼₂ : REL A₂ B₂ ℓ₂} (∼ᵣ : ⟦REL⟧ Aᵣ Bᵣ ℓᵣ ∼₁ ∼₂)
              → Decidable ∼₁ → Decidable ∼₂ → Set _
⟦Decidable⟧ Aᵣ Bᵣ _∼ᵣ_ = ⟨ xᵣ ∶ Aᵣ ⟩⟦→⟧ ⟨ yᵣ ∶ Bᵣ ⟩⟦→⟧ ⟦Dec⟧ (xᵣ ∼ᵣ yᵣ)