module Test where
open import Level
open import Relation.Nullary
open import Relation.Binary -- hiding (_⇔_ )
open import Data.Empty
open import Data.Nat hiding ( _⊔_ )

id : ( A : Set ) → A → A
id A x =  x

id1 : { A : Set } → A → A
id1 x = x


test1 = id ℕ 1
test2 = id1  1



data Bool : Set where
    true  : Bool
    false : Bool

record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
   constructor ⟪_,_⟫
   field
      proj1 : A
      proj2 : B

data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
   case1 : A → A ∨ B
   case2 : B → A ∨ B