{-# 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  ⟦Π⟧
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ᵣ} {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  ⟦∀⟧
syntax ⟦∀⟧ Aᵣ (λ xᵣ → f) = ∀⟨ xᵣ ∶ Aᵣ ⟩⟦→⟧ f

infixr  _⟦→⟧_
_⟦→⟧_ : ∀ {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  _⟦→⟧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  ⟦¬⟧_

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

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ᵣ = λ 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 ℓᵣ) : ⟦Set⟧ (ℓ₁ ⊔ ℓ₂ ⊔ ℓᵣ) (Dec P₁) (Dec P₂) where
  yes : {p₁ : P₁} {p₂ : P₂} (pᵣ : Pᵣ p₁ p₂) → ⟦Dec⟧ Pᵣ (yes p₁) (yes p₂)
  no  : {¬p₁ : ¬ P₁} {¬p₂ : ¬ P₂} (¬pᵣ : (⟦¬⟧ Pᵣ) ¬p₁ ¬p₂) → ⟦Dec⟧ Pᵣ (no ¬p₁) (no ¬p₂)

⟦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ᵣ)