@[reducible, inline]

abbrev Iris.Std.Relation (α : Type u_1) : Type u_1

Represents a binary relation with two arguments of the same type α.

Equations

• Iris.Std.Relation α = (α → α → Prop)

class Iris.Std.Reflexive {α : Type u_1} (R : Relation α) : Prop

Require that a relation R on a is reflexive.

• refl {x : α} : R x x

class Iris.Std.Transitive {α : Type u_1} (R : Relation α) : Prop

Require that a relation R on α is transitive.

• trans {x y z : α} : R x y → R y z → R x z

class Iris.Std.Preorder {α : Type u_1} (R : Relation α) extends Iris.Std.Reflexive R, Iris.Std.Transitive R : Prop

Require that a relation R on α is a preorder, i.e. that it is reflexive and transitive.

• refl {x : α} : R x x
• trans {x y z : α} : R x y → R y z → R x z

class Iris.Std.Idempotent {α : Type u_1} (R : Relation α) (f : α → α → α) : Prop

Require that a binary function f on α is idempotent in a relation R on α.

• idem {x : α} : R (f x x) x

class Iris.Std.Commutative {α : Type u_1} {β : Sort u_2} (R : Relation α) (f : β → β → α) : Prop

Require that a binary function f from β to α is commutative in a relation R on α.

• comm {x y : β} : R (f x y) (f y x)

class Iris.Std.LeftId {α : Type u_1} (R : Relation α) (i : α) (f : α → α → α) : Prop

Require that an element i of α is the left unit of a binary function f on α in a relation R on α.

• left_id {x : α} : R (f i x) x

class Iris.Std.RightId {α : Type u_1} (R : Relation α) (i : α) (f : α → α → α) : Prop

Require that an element i of α is the right unit of a binary function f on α in a relation R on α.

• right_id {x : α} : R (f x i) x

class Iris.Std.Associative {α : Type u_1} (R : Relation α) (f : α → α → α) : Prop

Require that a binary function f on α is associative in a relation R on α.

• assoc {x y z : α} : R (f (f x y) z) (f x (f y z))

class Iris.Std.Antisymmetric {α : Type u_1} (R : Relation α) (S : outParam (Relation α)) : Prop

Require that a relation S on α is antisymmetrical with R as its equivalence relation.

• antisymm {x y : α} (left : S x y) (right : S y x) : R x y