Data.Setoid.Definition

Basic definition and notation for setoids

Reexports

import public Control.Relation
import public Control.Order
import public Data.Fun.Nary

Definitions

record Equivalence : Type -> Type

Totality: total
Visibility: public export
Constructor:

MkEquivalence : {0 A : Type} -> (0 relation : Rel A) -> ((x : A) -> relation x x) -> ((x : A) -> (y : A) -> relation x y -> relation y x) -> ((x : A) -> (y : A) -> (z : A) -> relation x y -> relation y z -> relation x z) -> Equivalence A

Projections:

.reflexive : {0 A : Type} -> ({rec:0} : Equivalence A) -> (x : A) -> relation {rec:0} x x
0 .relation : {0 A : Type} -> Equivalence A -> Rel A
.symmetric : {0 A : Type} -> ({rec:0} : Equivalence A) -> (x : A) -> (y : A) -> relation {rec:0} x y -> relation {rec:0} y x
.transitive : {0 A : Type} -> ({rec:0} : Equivalence A) -> (x : A) -> (y : A) -> (z : A) -> relation {rec:0} x y -> relation {rec:0} y z -> relation {rec:0} x z

0 .relation : {0 A : Type} -> Equivalence A -> Rel A

Totality: total
Visibility: public export

0 relation : {0 A : Type} -> Equivalence A -> Rel A

Totality: total
Visibility: public export

.reflexive : {0 A : Type} -> ({rec:0} : Equivalence A) -> (x : A) -> relation {rec:0} x x

Totality: total
Visibility: public export

reflexive : {0 A : Type} -> ({rec:0} : Equivalence A) -> (x : A) -> relation {rec:0} x x

Totality: total
Visibility: public export

.symmetric : {0 A : Type} -> ({rec:0} : Equivalence A) -> (x : A) -> (y : A) -> relation {rec:0} x y -> relation {rec:0} y x

Totality: total
Visibility: public export

symmetric : {0 A : Type} -> ({rec:0} : Equivalence A) -> (x : A) -> (y : A) -> relation {rec:0} x y -> relation {rec:0} y x

Totality: total
Visibility: public export

.transitive : {0 A : Type} -> ({rec:0} : Equivalence A) -> (x : A) -> (y : A) -> (z : A) -> relation {rec:0} x y -> relation {rec:0} y z -> relation {rec:0} x z

Totality: total
Visibility: public export

transitive : {0 A : Type} -> ({rec:0} : Equivalence A) -> (x : A) -> (y : A) -> (z : A) -> relation {rec:0} x y -> relation {rec:0} y z -> relation {rec:0} x z

Totality: total
Visibility: public export

EqualEquivalence : (0 a : Type) -> Equivalence a

Totality: total
Visibility: public export

record Setoid : Type

Totality: total
Visibility: public export
Constructor:

MkSetoid : (0 U : Type) -> Equivalence U -> Setoid

Projections:

0 .U : Setoid -> Type
.equivalence : ({rec:0} : Setoid) -> Equivalence (U {rec:0})

Hints:

Cast (Model pres) Setoid
Cast (SetoidAlgebra sig) Setoid
Cast Type Setoid
pres .signature = sig => Semantic (Extension a x) (Op sig)
pres .signature = sig => Semantic (Extension a x) (Term sig y)
pres .signature = sig => Semantic (Frex a x) (Op sig)
pres .signature = sig => Semantic (Frex a x) (Term sig y)
pres .signature = sig => Semantic (ModelOver pres x) (Op sig)
pres .signature = sig => Semantic (ModelOver pres x) (Term sig y)
pres .signature = sig => Semantic (Free pres x) (Op sig)
pres .signature = sig => Semantic (Free pres x) (Term sig y)
Show (FreePresetoid sig x u v)

0 .U : Setoid -> Type

Totality: total
Visibility: public export

0 U : Setoid -> Type

Totality: total
Visibility: public export

.equivalence : ({rec:0} : Setoid) -> Equivalence (U {rec:0})

Totality: total
Visibility: public export

equivalence : ({rec:0} : Setoid) -> Equivalence (U {rec:0})

Totality: total
Visibility: public export

record PreorderData : (A : Type) -> Rel A -> Type

Totality: total
Visibility: public export
Constructor:

MkPreorderData : {0 A : Type} -> ((x : A) -> rel x x) -> ((x : A) -> (y : A) -> (z : A) -> rel x y -> rel y z -> rel x z) -> PreorderData A rel

Projections:

.reflexive : {0 A : Type} -> PreorderData A rel -> (x : A) -> rel x x
.transitive : {0 A : Type} -> PreorderData A rel -> (x : A) -> (y : A) -> (z : A) -> rel x y -> rel y z -> rel x z

.reflexive : {0 A : Type} -> PreorderData A rel -> (x : A) -> rel x x

Totality: total
Visibility: public export

reflexive : {0 A : Type} -> PreorderData A rel -> (x : A) -> rel x x

Totality: total
Visibility: public export

.transitive : {0 A : Type} -> PreorderData A rel -> (x : A) -> (y : A) -> (z : A) -> rel x y -> rel y z -> rel x z

Totality: total
Visibility: public export

transitive : {0 A : Type} -> PreorderData A rel -> (x : A) -> (y : A) -> (z : A) -> rel x y -> rel y z -> rel x z

Totality: total
Visibility: public export

MkPreorderWorkaround : Preorder ty rel

Totality: total
Visibility: public export

reflect : (a : Setoid) -> x = y -> (a .equivalence) .relation x y

Totality: total
Visibility: public export

MkPreorder : ((x : a) -> rel x x) -> ((x : a) -> (y : a) -> (z : a) -> rel x y -> rel y z -> rel x z) -> Preorder a rel

Totality: total
Visibility: public export

cast : (a : Setoid) -> Preorder (U a) ((a .equivalence) .relation)

Totality: total
Visibility: public export

irrelevantCast : (0 _ : Type) -> Setoid

Totality: total
Visibility: public export

0 SetoidHomomorphism : (a : Setoid) -> (b : Setoid) -> (U a -> U b) -> Type

Totality: total
Visibility: public export

record (~>) : Setoid -> Setoid -> Type

Totality: total
Visibility: public export
Constructor:

MkSetoidHomomorphism : {0 A : Setoid} -> {0 B : Setoid} -> (H : (U A -> U B)) -> SetoidHomomorphism A B H -> A ~> B

Projections:

.H : {0 A : Setoid} -> {0 B : Setoid} -> A ~> B -> U A -> U B
.homomorphic : {0 A : Setoid} -> {0 B : Setoid} -> ({rec:0} : A ~> B) -> SetoidHomomorphism A B (H {rec:0})

Fixity Declarations:
infix operator, level 5
infix operator, level 5
infix operator, level 5

.H : {0 A : Setoid} -> {0 B : Setoid} -> A ~> B -> U A -> U B

Totality: total
Visibility: public export

H : {0 A : Setoid} -> {0 B : Setoid} -> A ~> B -> U A -> U B

Totality: total
Visibility: public export

.homomorphic : {0 A : Setoid} -> {0 B : Setoid} -> ({rec:0} : A ~> B) -> SetoidHomomorphism A B (H {rec:0})

Totality: total
Visibility: public export

homomorphic : {0 A : Setoid} -> {0 B : Setoid} -> ({rec:0} : A ~> B) -> SetoidHomomorphism A B (H {rec:0})

Totality: total
Visibility: public export

mate : (a -> U b) -> irrelevantCast a ~> b

Totality: total
Visibility: public export

id : (a : Setoid) -> a ~> a

  Identity Setoid homomorphism

Totality: total
Visibility: public export

(.) : b ~> c -> a ~> b -> a ~> c

  Composition of Setoid homomorphisms

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 9

(~~>) : Setoid -> Setoid -> Setoid

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 5

post : b ~> c -> (a ~~> b) ~> (a ~~> c)

Totality: total
Visibility: public export

record Isomorphism : a ~> b -> b ~> a -> Type

  Two setoid homomorphism are each other's inverses

Totality: total
Visibility: public export
Constructor:

IsIsomorphism : {0 Fwd : a ~> b} -> {0 Bwd : b ~> a} -> ((a ~~> a) .equivalence) .relation (Bwd . Fwd) (id a) -> ((b ~~> b) .equivalence) .relation (Fwd . Bwd) (id b) -> Isomorphism Fwd Bwd

Projections:

.BwdFwdId : {0 Fwd : a ~> b} -> {0 Bwd : b ~> a} -> Isomorphism Fwd Bwd -> ((a ~~> a) .equivalence) .relation (Bwd . Fwd) (id a)
.FwdBwdId : {0 Fwd : a ~> b} -> {0 Bwd : b ~> a} -> Isomorphism Fwd Bwd -> ((b ~~> b) .equivalence) .relation (Fwd . Bwd) (id b)

.BwdFwdId : {0 Fwd : a ~> b} -> {0 Bwd : b ~> a} -> Isomorphism Fwd Bwd -> ((a ~~> a) .equivalence) .relation (Bwd . Fwd) (id a)

Totality: total
Visibility: public export

BwdFwdId : {0 Fwd : a ~> b} -> {0 Bwd : b ~> a} -> Isomorphism Fwd Bwd -> ((a ~~> a) .equivalence) .relation (Bwd . Fwd) (id a)

Totality: total
Visibility: public export

.FwdBwdId : {0 Fwd : a ~> b} -> {0 Bwd : b ~> a} -> Isomorphism Fwd Bwd -> ((b ~~> b) .equivalence) .relation (Fwd . Bwd) (id b)

Totality: total
Visibility: public export

FwdBwdId : {0 Fwd : a ~> b} -> {0 Bwd : b ~> a} -> Isomorphism Fwd Bwd -> ((b ~~> b) .equivalence) .relation (Fwd . Bwd) (id b)

Totality: total
Visibility: public export

record (<~>) : Setoid -> Setoid -> Type

  Setoid isomorphism

Totality: total
Visibility: public export
Constructor:

MkIsomorphism : (Fwd : a ~> b) -> (Bwd : b ~> a) -> Isomorphism Fwd Bwd -> a <~> b

Projections:

.Bwd : a <~> b -> b ~> a
.Fwd : a <~> b -> a ~> b
.Iso : ({rec:0} : a <~> b) -> Isomorphism (Fwd {rec:0}) (Bwd {rec:0})

Fixity Declarations:
infix operator, level 5
infix operator, level 5

.Fwd : a <~> b -> a ~> b

Totality: total
Visibility: public export

Fwd : a <~> b -> a ~> b

Totality: total
Visibility: public export

.Bwd : a <~> b -> b ~> a

Totality: total
Visibility: public export

Bwd : a <~> b -> b ~> a

Totality: total
Visibility: public export

.Iso : ({rec:0} : a <~> b) -> Isomorphism (Fwd {rec:0}) (Bwd {rec:0})

Totality: total
Visibility: public export

Iso : ({rec:0} : a <~> b) -> Isomorphism (Fwd {rec:0}) (Bwd {rec:0})

Totality: total
Visibility: public export

refl : a <~> a

  Identity (isomorphism _)

Totality: total
Visibility: public export

sym : a <~> b -> b <~> a

  Reverse an isomorphism

Totality: total
Visibility: public export

trans : a <~> b -> b <~> c -> a <~> c

  Compose isomorphisms

Totality: total
Visibility: public export

IsoEquivalence : Equivalence Setoid

Totality: total
Visibility: public export

Quotient : (b : Setoid) -> (a -> U b) -> Setoid

  Quotient a type by an function into a setoid
  
  Instance of the more general coequaliser of two setoid morphisms.

Totality: total
Visibility: public export