{- | Derives a contradiction from assumptions in the context

 - A proof of a contradiction can be explicitly specified as an implicit argument
 - `using`, `usingOnly`, and `hiding` with a single argument can be used instead of a proof to control the context

 -}
\meta contradiction

{- | Given constructs a \Sigma-type:
 - * `Given (x y z : A) B` is equivalent to `\Sigma (x y z : A) B`.
 - * `Given {x y z} B` is equivalent to `\Sigma (x y z : _) B`
 - * If `P : A -> B -> C -> \Type`, then `Given ((x,y,z) (a,b,c) : P) (Q x y z a b c)` is equivalent to `\Sigma (x a : A) (y b : B) (z c : C) (P x y z) (P a b c) (Q x y z a b c)`
 - * If `l : Array A`, then `Given (x y : l) (P x y)` is equivalent to `\Sigma (j j' : Fin l.len) (P (l j) (l j'))`

 -}
\meta Given

-- | {Exists} is a truncated version of {Given}. That is, `Exists a b c` is equivalent to `TruncP (Given a b c)`
\meta Exists \alias ∃

{- | {Forall} works like {Given}, but returns a \Pi-type instead of a \Sigma-type.
 - The last argument should be a type and will be used as the codomain.
 - Other arguments work like arguments of {Given} with the exception that curly braces mean implicit arguments:
 - * `Forall (x y : A) B` is equivalent to `\Pi (x y : A) -> B`
 - * `Forall {x y : A} B` is equivalent to `\Pi {x y : A} -> B`
 - * `Forall x y B` is equivalent to `\Pi (x : _) (y : _) -> B
 - `* `Forall x (B 0) (B 1)` is equivalent to `\Pi (x : _) -> B 0 -> B 1
 - `* `Forall {x y} {z} B` is equivalent to `\Pi {x y : _} {z : _} -> B`
 - * If `P : A -> \Type`, then `Forall {x y : P} (Q x) (Q y)` is equivalent to `\Pi {x y : A} -> P x -> P y -> Q x -> Q y`

 -}
\meta Forall \alias ∀

-- | Returns either a tuple, a \new expression, or a single constructor of a data type depending on the expected type
\meta constructor