{-# 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
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

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
  infix   finally
  infixr  _≡⟨_⟩_

  _≡⟨_⟩_ : ∀ x {y z : A} → x ≡ y → y ≡ z → x ≡ z
  _ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z

  finally : ∀ (x y : A) → x ≡ y → x ≡ y
  finally _ _ x≡y = x≡y

  syntax finally x y x≡y = x ≡⟨ x≡y ⟩∎ y ∎

module ≗-Reasoning {a b} {A : Set a} {B : Set b} where
  infix   finally
  infixr  _≗⟨_⟩_

  _≗⟨_⟩_ : ∀ x {y z : A → B} → x ≗ y → y ≗ z → x ≗ z
  _ ≗⟨ x≗y ⟩ y≗z = Setoid.trans (A →-setoid B) x≗y y≗z

  finally : ∀ (x y : A → B) → x ≗ y → x ≗ y
  finally _ _ x≗y = x≗y

  syntax finally x y x≗y = x ≗⟨ x≗y ⟩∎ y ∎

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⟧