module MiniLibrary.Base where

data Bool : Set where
  true : Bool
  false : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

{-# COMPILED_DATA Bool Bool True False #-}


data  : Set  where
  triv :  

data  : Set where

data _∨_ (A B : Set) : Set where
  inl : A  A  B
  inr : B  A  B

infixr 3 _∨_


in0 : {A B C : Set}  A  A  B  C
in0 a = inl a

in1 : {A B C : Set}  B  A  B  C
in1 b = inr (inl b)

in2 : {A B C : Set}  C  A  B  C
in2 c = inr (inr c)


True : Bool  Set
True true  = 
True false =