\import Logic
\import Order.Biordered
\import Paths

{- |
  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 => _ (transport, transportInv, *>, inv, Empty, BiorderedSet.<-transitive-left)

{- |
  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 ∃ => _ TruncP

{- |
  {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