{- Use with Andrea Vezzosi's agda-flat -}
{-# OPTIONS --without-K #-}

module agda-flat.prelude where

open import agda.prelude

----------------------------------------------------------------------
-- Congruence property for functions of a crisp variable
----------------------------------------------------------------------

cong♭ :
  {l :{} Level}
  {A :{} Set l}
  {l' : Level}
  {B : Set l'}
  (f : (x :{} A)  B){x y :{} A}
   ------------------------------
  (_ :{} x  y)  f x  f y
cong♭ _ refl = refl

----------------------------------------------------------------------
-- Example that's in the paper
----------------------------------------------------------------------
private 
  right : (A :{} Set) (B : Set) (f : (_ :{} A)  B) (x :{} A)  B
  right A B f x = f x