Idris2Doc : Data.DPair

# Data.DPair

## Definitions

`choice : {0 p : a -> b -> Type} -> ((x : a) -> (b : b ** p x b)) -> (f : a -> b ** (x : a) -> p x (f x))`
`  Constructive choice: a function producing pairs of a value and a proof  can be split into a function producing a value and a family of proofs  for the images of that function.`

Totality: total
Visibility: public export
`choice : {0 b : a -> Type} -> {0 p : (x : a) -> b x -> Type} -> ((x : a) -> (y : b x ** p x y)) -> (f : (x : a) -> b x ** (x : a) -> p x (f x))`
`  Constructive choice: a function producing pairs of a value and a proof  can be split into a function producing a value and a family of proofs  for the images of that function.`

Totality: total
Visibility: public export
`curry : {0 p : a -> Type} -> ((x : a ** p x) -> c) -> (x : a) -> p x -> c`
`  A function taking a pair of a value and a proof as an argument can be turned  into a function taking a value and a proof as two separate arguments.  Use `uncurry` to go in the other direction`

Totality: total
Visibility: public export
`uncurry : {0 p : a -> Type} -> ((x : a) -> p x -> c) -> (x : a ** p x) -> c`
`  A function taking a value and a proof as two separates arguments can be turned  into a function taking a pair of that value and its proof as a single argument.  Use `curry` to go in the other direction.`

Totality: total
Visibility: public export
`bimap : {0 p : a -> Type} -> {0 q : b -> Type} -> (f : (a -> b)) -> (p x -> q (f x)) -> (x : a ** p x) -> (y : b ** q y)`
`  Given a function on values and a family of proofs that this function takes  p-respecting inputs to q-respecting outputs,  we can turn:  a pair of a value and a proof it is p-respecting  into:         a pair of a value and a proof it is q-respecting`

Totality: total
Visibility: public export
`record Exists : (type -> Type) -> Type`
`  A dependent pair in which the first field (witness) should be  erased at runtime.    We can use `Exists` to construct dependent types in which the  type-level value is erased at runtime but used at compile time.  This type-level value could represent, for instance, a value  required for an intrinsic invariant required as part of the  dependent type's representation.    @type The type of the type-level value in the proof.  @this The dependent type that requires an instance of `type`.`

Totality: total
Visibility: public export
Constructor:
`Evidence : (0 fst : type) -> this fst -> Exists this`

Projections:
`0 .fst : Exists this -> type`
`.snd : ({rec:0} : Exists this) -> this (fst {rec:0})`
`0 .fst : Exists this -> type`
Totality: total
Visibility: public export
`0 fst : Exists this -> type`
Totality: total
Visibility: public export
`.snd : ({rec:0} : Exists this) -> this (fst {rec:0})`
Totality: total
Visibility: public export
`snd : ({rec:0} : Exists this) -> this (fst {rec:0})`
Totality: total
Visibility: public export
`curry : (Exists p -> c) -> p x -> c`
Totality: total
Visibility: public export
`uncurry : (p x -> c) -> Exists p -> c`
Totality: total
Visibility: public export
`evidenceInjectiveFst : Evidence x p = Evidence y q -> x = y`
Totality: total
Visibility: export
`evidenceInjectiveSnd : Evidence x p = Evidence x q -> p = q`
Totality: total
Visibility: export
`bimap : (0 f : (a -> b)) -> (p x -> q (f x)) -> Exists p -> Exists q`
Totality: total
Visibility: public export
`record Subset : (type : Type) -> (type -> Type) -> Type`
`  A dependent pair in which the second field (evidence) should not  be required at runtime.    We can use `Subset` to provide extrinsic invariants about a  value and know that these invariants are erased at  runtime but used at compile time.    @type The type-level value's type.  @pred The dependent type that requires an instance of `type`.`

Totality: total
Visibility: public export
Constructor:
`Element : (fst : type) -> (0 _ : pred fst) -> Subset type pred`

Projections:
`.fst : Subset type pred -> type`
`0 .snd : ({rec:0} : Subset type pred) -> pred (fst {rec:0})`

Hints:
`Eq type => Eq (Subset type pred)`
`Ord type => Ord (Subset type pred)`
`Show type => Show (Subset type pred)`
`.fst : Subset type pred -> type`
Totality: total
Visibility: public export
`fst : Subset type pred -> type`
Totality: total
Visibility: public export
`0 .snd : ({rec:0} : Subset type pred) -> pred (fst {rec:0})`
Totality: total
Visibility: public export
`0 snd : ({rec:0} : Subset type pred) -> pred (fst {rec:0})`
Totality: total
Visibility: public export
`curry : (Subset a p -> c) -> (x : a) -> (0 _ : p x) -> c`
Totality: total
Visibility: public export
`uncurry : ((x : a) -> (0 _ : p x) -> c) -> Subset a p -> c`
Totality: total
Visibility: public export
`elementInjectiveFst : Element x p = Element y q -> x = y`
Totality: total
Visibility: export
`elementInjectiveSnd : Element x p = Element x q -> p = q`
Totality: total
Visibility: export
`bimap : (f : (a -> b)) -> (0 _ : (p x -> q (f x))) -> Subset a p -> Subset b q`
Totality: total
Visibility: public export