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