{-# OPTIONS --universe-polymorphism #-}
-- move this to propeq
module Relation.Binary.PropositionalEquality.NP where

open import Relation.Binary.PropositionalEquality public hiding (module ≡-Reasoning)
open import Relation.Binary.NP
open import Relation.Binary.Bijection
open import Relation.Binary.Logical
open import Relation.Nullary

cong₃ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
          (f : A → B → C → D) {a₁ a₂ b₁ b₂ c₁ c₂}
        → a₁ ≡ a₂ → b₁ ≡ b₂ → c₁ ≡ c₂ → f a₁ b₁ c₁ ≡ f a₂ b₂ c₂
cong₃ f refl refl refl = refl

_≡≡_ : ∀ {a} {A : Set a} {i j : A}
         (i≡j₁ : i ≡ j) (i≡j₂ : i ≡ j) → i≡j₁ ≡ i≡j₂
_≡≡_ refl refl = refl

_≟≡_ : ∀ {a} {A : Set a} {i j : A} → Decidable {A = i ≡ j} _≡_
_≟≡_ refl refl = yes refl

_≗₂_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} (f g : A → B → C) → Set _
f ≗₂ g = ∀ x y → f x y ≡ g x y

injective : ∀ {a} {A : Set a} → InjectiveRel A _≡_
injective refl refl = refl

surjective : ∀ {a} {A : Set a} → SurjectiveRel A _≡_
surjective refl refl = refl

bijective : ∀ {a} {A : Set a} → BijectiveRel A _≡_
bijective = record { injectiveREL = injective; surjectiveREL = surjective }

module ≡-Reasoning {a} {A : Set a} where
  open Setoid-Reasoning (setoid A) public renaming (_≈⟨_⟩_ to _≡⟨_⟩_)

module ≗-Reasoning {a b} {A : Set a} {B : Set b} where
  open Setoid-Reasoning (A →-setoid B) public renaming (_≈⟨_⟩_ to _≗⟨_⟩_)

data ⟦≡⟧ {a₁ a₂ aᵣ}
         {A₁ A₂} (Aᵣ : ⟦Set⟧ {a₁} {a₂} aᵣ A₁ A₂)
         {x₁ x₂} (xᵣ : Aᵣ x₁ x₂)
       : (Aᵣ ⟦→⟧ ⟦Set⟧ aᵣ) (_≡_ x₁) (_≡_ x₂) where
    -- : ∀ {y₁ y₂} (yᵣ : Aᵣ y₁ y₂) → x₁ ≡ y₁ → x₂ ≡ y₂ → Set
  ⟦refl⟧ : ⟦≡⟧ Aᵣ xᵣ xᵣ refl refl

-- Double checking level 0 with a direct ⟦_⟧ encoding
private
  ⟦≡⟧′ : (∀⟨ Aᵣ ∶ ⟦Set₀⟧ ⟩⟦→⟧ Aᵣ ⟦→⟧ Aᵣ ⟦→⟧ ⟦Set₀⟧) _≡_ _≡_
  ⟦≡⟧′ = ⟦≡⟧

  ⟦refl⟧′ : (∀⟨ Aᵣ ∶ ⟦Set₀⟧ ⟩⟦→⟧ ∀⟨ xᵣ ∶ Aᵣ ⟩⟦→⟧ ⟦≡⟧ Aᵣ xᵣ xᵣ) refl refl
  ⟦refl⟧′ _ _ = ⟦refl⟧