----------------------------------------------------------------------
-- Reproducing code from the Agda standrad library to ensure that
-- we're not secretly using Axiom K
----------------------------------------------------------------------
{-# OPTIONS --without-K #-}

module PropEqWithoutK where

infix 4 _≡_
data _≡_ {a} {A : Set a} (x : A) : A  Set a where
  instance refl : x  x

-- {-# BUILTIN EQUALITY _≡_ #-}
-- {-# BUILTIN REFL refl #-}


sym :  {a} {A : Set a} {x y : A}  x  y  y  x
sym refl = refl

trans :  {a} {A : Set a} {x y z : A}  x  y  y  z  x  z
trans refl eq = eq

subst :  {a p} {A : Set a} (P : A  Set p) {x y : A}  x  y  P x  P y
subst P refl p = p

cong :  {a b} {A : Set a} {B : Set b}
       (f : A  B) {x y}  x  y  f x  f y
cong f refl = refl

cong-app :  {a b} {A : Set a} {B : A  Set b} {f g : (x : A)  B x} 
           f  g  (x : A)  f x  g x
cong-app refl x = refl

module ≡-Reasoning {a} {A : Set a} where

  infix  3 _∎
  infixr 2 _≡⟨⟩_ _≡⟨_⟩_
  infix  1 begin_

  begin_ : ∀{x y : A}  x  y  x  y
  begin_ x≡y = x≡y

  _≡⟨⟩_ :  (x {y} : A)  x  y  x  y
  _ ≡⟨⟩ x≡y = x≡y

  _≡⟨_⟩_ :  (x {y z} : A)  x  y  y  z  x  z
  _ ≡⟨ x≡y  y≡z = trans x≡y y≡z

  _∎ :  (x : A)  x  x
  _∎ _ = refl