module Notation where
open import Function
open import Data.Product
open import Data.Sum
open import Relation.Nullary as R0
open import Relation.Unary   as R1
open import Relation.Binary  as R2
import Level

infixl 0 _by_
_by_ :  {a} (A : Set a)  A  A
A by x = x

infixl 1 _§′_ _§_ 
_§′_ : {l m : _}{A : Set l}{B : A  Set m}  Fun₁ ( a  B a)
f §′ a = f a
_§_ : {l m : _}{A : Set l}{B : Set m}  Fun₁ (A  B)
_§_ = _§′_

Goal = Set
Proposition = Set

Pred₀ : {a}  Set a  Set _
Pred₀ A = Pred A Level.zero

infix 1 Every_is_
Every_is_ : {l m}(A : Set l)(B : A  Set m)  Set _
Every A is B = (a : A)  B a

infixr 2 _and_
_and_ : {l m}(A : Set l)(B : Set m)  Set _
_and_ = _×_

infixr 7 _And_
_And_ :  {ℓ₀ ℓ₁ ℓ₂}{A : Set ℓ₀}  Pred A ℓ₁  Pred A ℓ₂  Pred A _
_And_ = _∩_

infixr 1 _or_ 
_or_ : {l m}(A : Set l)(B : Set m)  Set _
_or_ = _⊎_

infixr 6 _Or_
_Or_ :  {}{A : Set }{ℓ₁ ℓ₂}  Pred A ℓ₁  Pred A ℓ₂  Pred A _
_Or_ = _∪_

infix 1 _is_
_is_ : { m}{A : Set }(a : A)(P : A  Set m)  Set _
a is P = P a

infix 4 _of_
_of_ : { m}{A : Set }{B : A  Set m}(f : (x : A)  B x)(a : A)  B a
f of a = f a

infix 3 Not_
Not_ :  { m}{A : Set m}  Pred A   Pred A 
Not_ = 

decomposingˍconjunction : {l m}{A : Set l}{B : Set m}  A  B  A and B
decomposingˍconjunction = _,_

instantiation : {l m}{A : Set l}{B : A  Set m}{x : A}  ((a : A)  B a)  B x
instantiation f = f _