{-# OPTIONS --cubical-compatible #-}
module Terra.Data.Negation.Instances where
open import Terra.Classes.Contravariant
open import Terra.Classes.Contractible
open import Terra.Data.Negation
open import Terra.Data.Level

private
  variable
    ℓ : Level

instance
  neg-contra : Contravariant {ℓ} ¬_
  neg-contra = record {
    contramap = λ t n f → n (t f)
    }


  -- ¬-contractible : {A : Set ℓ} -> Contractible A
  -- ¬-contractible = record {
  --   contract = λ a b → {!!}
  --   }