Data.Setoid.Pair

Product of setoids

Definitions

record And : {A : Type} -> {B : Type} -> Rel A -> Rel B -> (A, B) -> (A, B) -> Type

  Binary relation conjunction

Totality: total
Visibility: public export
Constructor: 

MkAnd : {0 A : Type} -> {0 B : Type} -> p (fst xy1) (fst xy2) -> q (snd xy1) (snd xy2) -> And p q xy1 xy2

Projections:

.fst : {0 A : Type} -> {0 B : Type} -> And p q xy1 xy2 -> p (fst xy1) (fst xy2)

.snd : {0 A : Type} -> {0 B : Type} -> And p q xy1 xy2 -> q (snd xy1) (snd xy2)

.fst : {0 A : Type} -> {0 B : Type} -> And p q xy1 xy2 -> p (fst xy1) (fst xy2)

Totality: total
Visibility: public export

fst : {0 A : Type} -> {0 B : Type} -> And p q xy1 xy2 -> p (fst xy1) (fst xy2)

Totality: total
Visibility: public export

.snd : {0 A : Type} -> {0 B : Type} -> And p q xy1 xy2 -> q (snd xy1) (snd xy2)

Totality: total
Visibility: public export

snd : {0 A : Type} -> {0 B : Type} -> And p q xy1 xy2 -> q (snd xy1) (snd xy2)

Totality: total
Visibility: public export

Pair : Setoid -> Setoid -> Setoid

  Product of setoids

Totality: total
Visibility: public export

.fst : Pair a b ~> a

  Left projection setoid homomorphism

Totality: total
Visibility: public export

.snd : Pair a b ~> b

  Right projection setoid homomorphism

Totality: total
Visibility: public export

tuple : c ~> a -> c ~> b -> c ~> Pair a b

  Setoid homomorphism constructor

Totality: total
Visibility: public export

unitVal : (x : ()) -> (y : ()) -> x = y

  Unique value of type unit

Totality: total
Visibility: public export

unit : a ~> cast ()

  The unique setoid map into the terminal type

Totality: total
Visibility: public export

const : U b -> a ~> b

  The constant function as a setoid morphism

Totality: total
Visibility: public export

bimap : c ~> a -> d ~> b -> Pair c d ~> Pair a b

  Setoid homomorphism constructor

Totality: total
Visibility: public export

distributeFunction : (Bool, U s) -> Either (U s) (U s)

  Function underlying the bijection 2 x s <~> s + s

Totality: total
Visibility: public export

distributeHomomorphism : SetoidHomomorphism (Pair (cast Bool) s) (Either s s) distributeFunction

  States: the function underlying the bijection 2 x s <~> s + s is a setoid homomorphism

Totality: total
Visibility: public export

distribute : Pair (cast Bool) s ~> Either s s

  Setoid homomorphism involved in the bijection 2 x s <~> s + s

Totality: total
Visibility: public export

pairIso : a <~> c -> b <~> d -> Pair a b <~> Pair c d

Totality: total
Visibility: public export