Idris2Doc : Control.Category.Instances.Thin

Control.Category.Instances.Thin

(source)
This module defines thin categories, which are categorifications
of certain relations. Explicitly, any reflexive and transitive
relation on a particular type also forms a category on that type
where there is at most one morphism between any two objects.

It can be demonstrated that thin *monoidal* categories correspond
to preordered monoids. This makes it possible to use string diagram
notation to prove inequalities on monoids.

It can be further demonstrated that thin *bimonoidal* categories
correspond to preordered semirings. This makes it possible to use
bimonoidal sheet diagram notation to prove inequalities on
semirings (represented here by the interface `Num`).

Reexports

import public Control.Relation
import public Control.Order

Definitions

record RelMonoid : (ty : Type) -> Rel ty -> Type
Totality: total
Visibility: public export
Constructor: 
MkRelMonoid : {auto impl : Monoid ty} -> (rel x y -> rel x' y' -> rel (x <+> x') (y <+> y')) -> rel ((x <+> y) <+> z) (x <+> (y <+> z)) -> rel (x <+> (y <+> z)) ((x <+> y) <+> z) -> rel (neutral <+> x) x -> rel x (neutral <+> x) -> rel (x <+> neutral) x -> rel x (x <+> neutral) -> RelMonoid ty rel

Projections:
.assoc : ({rec:0} : RelMonoid ty rel) -> rel ((x <+> y) <+> z) (x <+> (y <+> z))
.assoc' : ({rec:0} : RelMonoid ty rel) -> rel (x <+> (y <+> z)) ((x <+> y) <+> z)
.cong : ({rec:0} : RelMonoid ty rel) -> rel x y -> rel x' y' -> rel (x <+> x') (y <+> y')
.impl : RelMonoid ty rel -> Monoid ty
.unitl : ({rec:0} : RelMonoid ty rel) -> rel (neutral <+> x) x
.unitl' : ({rec:0} : RelMonoid ty rel) -> rel x (neutral <+> x)
.unitr : ({rec:0} : RelMonoid ty rel) -> rel (x <+> neutral) x
.unitr' : ({rec:0} : RelMonoid ty rel) -> rel x (x <+> neutral)
.impl : RelMonoid ty rel -> Monoid ty
Totality: total
Visibility: public export
impl : RelMonoid ty rel -> Monoid ty
Totality: total
Visibility: public export
.cong : ({rec:0} : RelMonoid ty rel) -> rel x y -> rel x' y' -> rel (x <+> x') (y <+> y')
Totality: total
Visibility: public export
cong : ({rec:0} : RelMonoid ty rel) -> rel x y -> rel x' y' -> rel (x <+> x') (y <+> y')
Totality: total
Visibility: public export
.assoc : ({rec:0} : RelMonoid ty rel) -> rel ((x <+> y) <+> z) (x <+> (y <+> z))
Totality: total
Visibility: public export
assoc : ({rec:0} : RelMonoid ty rel) -> rel ((x <+> y) <+> z) (x <+> (y <+> z))
Totality: total
Visibility: public export
.assoc' : ({rec:0} : RelMonoid ty rel) -> rel (x <+> (y <+> z)) ((x <+> y) <+> z)
Totality: total
Visibility: public export
assoc' : ({rec:0} : RelMonoid ty rel) -> rel (x <+> (y <+> z)) ((x <+> y) <+> z)
Totality: total
Visibility: public export
.unitl : ({rec:0} : RelMonoid ty rel) -> rel (neutral <+> x) x
Totality: total
Visibility: public export
unitl : ({rec:0} : RelMonoid ty rel) -> rel (neutral <+> x) x
Totality: total
Visibility: public export
.unitl' : ({rec:0} : RelMonoid ty rel) -> rel x (neutral <+> x)
Totality: total
Visibility: public export
unitl' : ({rec:0} : RelMonoid ty rel) -> rel x (neutral <+> x)
Totality: total
Visibility: public export
.unitr : ({rec:0} : RelMonoid ty rel) -> rel (x <+> neutral) x
Totality: total
Visibility: public export
unitr : ({rec:0} : RelMonoid ty rel) -> rel (x <+> neutral) x
Totality: total
Visibility: public export
.unitr' : ({rec:0} : RelMonoid ty rel) -> rel x (x <+> neutral)
Totality: total
Visibility: public export
unitr' : ({rec:0} : RelMonoid ty rel) -> rel x (x <+> neutral)
Totality: total
Visibility: public export
mkRelMonoid : Reflexive ty rel => {auto impl : Monoid ty} -> (rel x y -> rel x' y' -> rel (x <+> x') (y <+> y')) -> (0 _ : (x <+> y) <+> z = x <+> (y <+> z)) -> (0 _ : neutral <+> x = x) -> (0 _ : x <+> neutral = x) -> RelMonoid ty rel
Totality: total
Visibility: public export
record RelCommMonoid : (ty : Type) -> Rel ty -> Type
Totality: total
Visibility: public export
Constructor: 
MkRelCommMonoid : {auto impl : Monoid ty} -> (rel x y -> rel x' y' -> rel (x <+> x') (y <+> y')) -> rel ((x <+> y) <+> z) (x <+> (y <+> z)) -> rel (neutral <+> x) x -> rel x (neutral <+> x) -> rel (x <+> y) (y <+> x) -> RelCommMonoid ty rel

Projections:
.assoc : ({rec:0} : RelCommMonoid ty rel) -> rel ((x <+> y) <+> z) (x <+> (y <+> z))
.comm : ({rec:0} : RelCommMonoid ty rel) -> rel (x <+> y) (y <+> x)
.cong : ({rec:0} : RelCommMonoid ty rel) -> rel x y -> rel x' y' -> rel (x <+> x') (y <+> y')
.impl : RelCommMonoid ty rel -> Monoid ty
.relMonoid : Preorder ty rel => RelCommMonoid ty rel -> RelMonoid ty rel
.unit : ({rec:0} : RelCommMonoid ty rel) -> rel (neutral <+> x) x
.unit' : ({rec:0} : RelCommMonoid ty rel) -> rel x (neutral <+> x)
.impl : RelCommMonoid ty rel -> Monoid ty
Totality: total
Visibility: public export
impl : RelCommMonoid ty rel -> Monoid ty
Totality: total
Visibility: public export
.cong : ({rec:0} : RelCommMonoid ty rel) -> rel x y -> rel x' y' -> rel (x <+> x') (y <+> y')
Totality: total
Visibility: public export
cong : ({rec:0} : RelCommMonoid ty rel) -> rel x y -> rel x' y' -> rel (x <+> x') (y <+> y')
Totality: total
Visibility: public export
.assoc : ({rec:0} : RelCommMonoid ty rel) -> rel ((x <+> y) <+> z) (x <+> (y <+> z))
Totality: total
Visibility: public export
assoc : ({rec:0} : RelCommMonoid ty rel) -> rel ((x <+> y) <+> z) (x <+> (y <+> z))
Totality: total
Visibility: public export
.unit : ({rec:0} : RelCommMonoid ty rel) -> rel (neutral <+> x) x
Totality: total
Visibility: public export
unit : ({rec:0} : RelCommMonoid ty rel) -> rel (neutral <+> x) x
Totality: total
Visibility: public export
.unit' : ({rec:0} : RelCommMonoid ty rel) -> rel x (neutral <+> x)
Totality: total
Visibility: public export
unit' : ({rec:0} : RelCommMonoid ty rel) -> rel x (neutral <+> x)
Totality: total
Visibility: public export
.comm : ({rec:0} : RelCommMonoid ty rel) -> rel (x <+> y) (y <+> x)
Totality: total
Visibility: public export
comm : ({rec:0} : RelCommMonoid ty rel) -> rel (x <+> y) (y <+> x)
Totality: total
Visibility: public export
relMonoid : Preorder ty rel => RelCommMonoid ty rel -> RelMonoid ty rel
Totality: total
Visibility: public export
.relMonoid : Preorder ty rel => RelCommMonoid ty rel -> RelMonoid ty rel
Totality: total
Visibility: public export
mkRelCommMonoid : Reflexive ty rel => {auto impl : Monoid ty} -> (rel x y -> rel x' y' -> rel (x <+> x') (y <+> y')) -> (0 _ : (x <+> y) <+> z = x <+> (y <+> z)) -> (0 _ : neutral <+> x = x) -> (0 _ : x <+> y = y <+> x) -> RelCommMonoid ty rel
Totality: total
Visibility: public export
record RelNearRing : (ty : Type) -> Rel ty -> Type
Totality: total
Visibility: public export
Constructor: 
MkRelNearRing : {auto impl : Num ty} -> (rel x y -> rel x' y' -> rel (x + x') (y + y')) -> (rel x y -> rel x' y' -> rel (x * x') (y * y')) -> rel ((x + y) + z) (x + (y + z)) -> rel (x + (y + z)) ((x + y) + z) -> rel ((x * y) * z) (x * (y * z)) -> rel (x * (y * z)) ((x * y) * z) -> rel (0 + x) x -> rel x (0 + x) -> rel (1 * x) x -> rel x (1 * x) -> rel (x + 0) x -> rel x (x + 0) -> rel (x * 1) x -> rel x (x * 1) -> rel (x * (y + z)) ((x * y) + (x * z)) -> rel ((x * y) + (x * z)) (x * (y + z)) -> rel ((x + y) * z) ((x * z) + (y * z)) -> rel ((x * z) + (y * z)) ((x + y) * z) -> rel (x * 0) 0 -> rel 0 (x * 0) -> rel (0 * x) 0 -> rel 0 (0 * x) -> RelNearRing ty rel

Projections:
.absorbl : ({rec:0} : RelNearRing ty rel) -> rel (x * 0) 0
.absorbl' : ({rec:0} : RelNearRing ty rel) -> rel 0 (x * 0)
.absorbr : ({rec:0} : RelNearRing ty rel) -> rel (0 * x) 0
.absorbr' : ({rec:0} : RelNearRing ty rel) -> rel 0 (0 * x)
.distribl : ({rec:0} : RelNearRing ty rel) -> rel (x * (y + z)) ((x * y) + (x * z))
.distribl' : ({rec:0} : RelNearRing ty rel) -> rel ((x * y) + (x * z)) (x * (y + z))
.distribr : ({rec:0} : RelNearRing ty rel) -> rel ((x + y) * z) ((x * z) + (y * z))
.distribr' : ({rec:0} : RelNearRing ty rel) -> rel ((x * z) + (y * z)) ((x + y) * z)
.impl : RelNearRing ty rel -> Num ty
.multAssoc : ({rec:0} : RelNearRing ty rel) -> rel ((x * y) * z) (x * (y * z))
.multAssoc' : ({rec:0} : RelNearRing ty rel) -> rel (x * (y * z)) ((x * y) * z)
.multCong : ({rec:0} : RelNearRing ty rel) -> rel x y -> rel x' y' -> rel (x * x') (y * y')
.multMonoid : RelNearRing ty rel -> RelMonoid ty rel
.multUnitl : ({rec:0} : RelNearRing ty rel) -> rel (1 * x) x
.multUnitl' : ({rec:0} : RelNearRing ty rel) -> rel x (1 * x)
.multUnitr : ({rec:0} : RelNearRing ty rel) -> rel (x * 1) x
.multUnitr' : ({rec:0} : RelNearRing ty rel) -> rel x (x * 1)
.plusAssoc : ({rec:0} : RelNearRing ty rel) -> rel ((x + y) + z) (x + (y + z))
.plusAssoc' : ({rec:0} : RelNearRing ty rel) -> rel (x + (y + z)) ((x + y) + z)
.plusCong : ({rec:0} : RelNearRing ty rel) -> rel x y -> rel x' y' -> rel (x + x') (y + y')
.plusMonoid : RelNearRing ty rel -> RelMonoid ty rel
.plusUnitl : ({rec:0} : RelNearRing ty rel) -> rel (0 + x) x
.plusUnitl' : ({rec:0} : RelNearRing ty rel) -> rel x (0 + x)
.plusUnitr : ({rec:0} : RelNearRing ty rel) -> rel (x + 0) x
.plusUnitr' : ({rec:0} : RelNearRing ty rel) -> rel x (x + 0)
.impl : RelNearRing ty rel -> Num ty
Totality: total
Visibility: public export
impl : RelNearRing ty rel -> Num ty
Totality: total
Visibility: public export
.plusCong : ({rec:0} : RelNearRing ty rel) -> rel x y -> rel x' y' -> rel (x + x') (y + y')
Totality: total
Visibility: public export
plusCong : ({rec:0} : RelNearRing ty rel) -> rel x y -> rel x' y' -> rel (x + x') (y + y')
Totality: total
Visibility: public export
.multCong : ({rec:0} : RelNearRing ty rel) -> rel x y -> rel x' y' -> rel (x * x') (y * y')
Totality: total
Visibility: public export
multCong : ({rec:0} : RelNearRing ty rel) -> rel x y -> rel x' y' -> rel (x * x') (y * y')
Totality: total
Visibility: public export
.plusAssoc : ({rec:0} : RelNearRing ty rel) -> rel ((x + y) + z) (x + (y + z))
Totality: total
Visibility: public export
plusAssoc : ({rec:0} : RelNearRing ty rel) -> rel ((x + y) + z) (x + (y + z))
Totality: total
Visibility: public export
.plusAssoc' : ({rec:0} : RelNearRing ty rel) -> rel (x + (y + z)) ((x + y) + z)
Totality: total
Visibility: public export
plusAssoc' : ({rec:0} : RelNearRing ty rel) -> rel (x + (y + z)) ((x + y) + z)
Totality: total
Visibility: public export
.multAssoc : ({rec:0} : RelNearRing ty rel) -> rel ((x * y) * z) (x * (y * z))
Totality: total
Visibility: public export
multAssoc : ({rec:0} : RelNearRing ty rel) -> rel ((x * y) * z) (x * (y * z))
Totality: total
Visibility: public export
.multAssoc' : ({rec:0} : RelNearRing ty rel) -> rel (x * (y * z)) ((x * y) * z)
Totality: total
Visibility: public export
multAssoc' : ({rec:0} : RelNearRing ty rel) -> rel (x * (y * z)) ((x * y) * z)
Totality: total
Visibility: public export
.plusUnitl : ({rec:0} : RelNearRing ty rel) -> rel (0 + x) x
Totality: total
Visibility: public export
plusUnitl : ({rec:0} : RelNearRing ty rel) -> rel (0 + x) x
Totality: total
Visibility: public export
.plusUnitl' : ({rec:0} : RelNearRing ty rel) -> rel x (0 + x)
Totality: total
Visibility: public export
plusUnitl' : ({rec:0} : RelNearRing ty rel) -> rel x (0 + x)
Totality: total
Visibility: public export
.multUnitl : ({rec:0} : RelNearRing ty rel) -> rel (1 * x) x
Totality: total
Visibility: public export
multUnitl : ({rec:0} : RelNearRing ty rel) -> rel (1 * x) x
Totality: total
Visibility: public export
.multUnitl' : ({rec:0} : RelNearRing ty rel) -> rel x (1 * x)
Totality: total
Visibility: public export
multUnitl' : ({rec:0} : RelNearRing ty rel) -> rel x (1 * x)
Totality: total
Visibility: public export
.plusUnitr : ({rec:0} : RelNearRing ty rel) -> rel (x + 0) x
Totality: total
Visibility: public export
plusUnitr : ({rec:0} : RelNearRing ty rel) -> rel (x + 0) x
Totality: total
Visibility: public export
.plusUnitr' : ({rec:0} : RelNearRing ty rel) -> rel x (x + 0)
Totality: total
Visibility: public export
plusUnitr' : ({rec:0} : RelNearRing ty rel) -> rel x (x + 0)
Totality: total
Visibility: public export
.multUnitr : ({rec:0} : RelNearRing ty rel) -> rel (x * 1) x
Totality: total
Visibility: public export
multUnitr : ({rec:0} : RelNearRing ty rel) -> rel (x * 1) x
Totality: total
Visibility: public export
.multUnitr' : ({rec:0} : RelNearRing ty rel) -> rel x (x * 1)
Totality: total
Visibility: public export
multUnitr' : ({rec:0} : RelNearRing ty rel) -> rel x (x * 1)
Totality: total
Visibility: public export
.distribl : ({rec:0} : RelNearRing ty rel) -> rel (x * (y + z)) ((x * y) + (x * z))
Totality: total
Visibility: public export
distribl : ({rec:0} : RelNearRing ty rel) -> rel (x * (y + z)) ((x * y) + (x * z))
Totality: total
Visibility: public export
.distribl' : ({rec:0} : RelNearRing ty rel) -> rel ((x * y) + (x * z)) (x * (y + z))
Totality: total
Visibility: public export
distribl' : ({rec:0} : RelNearRing ty rel) -> rel ((x * y) + (x * z)) (x * (y + z))
Totality: total
Visibility: public export
.distribr : ({rec:0} : RelNearRing ty rel) -> rel ((x + y) * z) ((x * z) + (y * z))
Totality: total
Visibility: public export
distribr : ({rec:0} : RelNearRing ty rel) -> rel ((x + y) * z) ((x * z) + (y * z))
Totality: total
Visibility: public export
.distribr' : ({rec:0} : RelNearRing ty rel) -> rel ((x * z) + (y * z)) ((x + y) * z)
Totality: total
Visibility: public export
distribr' : ({rec:0} : RelNearRing ty rel) -> rel ((x * z) + (y * z)) ((x + y) * z)
Totality: total
Visibility: public export
.absorbl : ({rec:0} : RelNearRing ty rel) -> rel (x * 0) 0
Totality: total
Visibility: public export
absorbl : ({rec:0} : RelNearRing ty rel) -> rel (x * 0) 0
Totality: total
Visibility: public export
.absorbl' : ({rec:0} : RelNearRing ty rel) -> rel 0 (x * 0)
Totality: total
Visibility: public export
absorbl' : ({rec:0} : RelNearRing ty rel) -> rel 0 (x * 0)
Totality: total
Visibility: public export
.absorbr : ({rec:0} : RelNearRing ty rel) -> rel (0 * x) 0
Totality: total
Visibility: public export
absorbr : ({rec:0} : RelNearRing ty rel) -> rel (0 * x) 0
Totality: total
Visibility: public export
.absorbr' : ({rec:0} : RelNearRing ty rel) -> rel 0 (0 * x)
Totality: total
Visibility: public export
absorbr' : ({rec:0} : RelNearRing ty rel) -> rel 0 (0 * x)
Totality: total
Visibility: public export
mkRelNearRing : Reflexive ty rel => {auto impl : Num ty} -> (rel x y -> rel x' y' -> rel (x + x') (y + y')) -> (rel x y -> rel x' y' -> rel (x * x') (y * y')) -> (0 _ : (x + y) + z = x + (y + z)) -> (0 _ : (x * y) * z = x * (y * z)) -> (0 _ : 0 + x = x) -> (0 _ : 1 * x = x) -> (0 _ : x + 0 = x) -> (0 _ : x * 1 = x) -> (0 _ : x * (y + z) = (x * y) + (x * z)) -> (0 _ : (x + y) * z = (x * z) + (y * z)) -> (0 _ : x * 0 = 0) -> (0 _ : 0 * x = 0) -> RelNearRing ty rel
Totality: total
Visibility: public export
plusMonoid : RelNearRing ty rel -> RelMonoid ty rel
Totality: total
Visibility: public export
.plusMonoid : RelNearRing ty rel -> RelMonoid ty rel
Totality: total
Visibility: public export
multMonoid : RelNearRing ty rel -> RelMonoid ty rel
Totality: total
Visibility: public export
.multMonoid : RelNearRing ty rel -> RelMonoid ty rel
Totality: total
Visibility: public export
record RelSemiring : (ty : Type) -> Rel ty -> Type
Totality: total
Visibility: public export
Constructor: 
MkRelSemiring : {auto impl : Num ty} -> (rel x y -> rel x' y' -> rel (x + x') (y + y')) -> (rel x y -> rel x' y' -> rel (x * x') (y * y')) -> rel ((x + y) + z) (x + (y + z)) -> rel ((x * y) * z) (x * (y * z)) -> rel (x * (y * z)) ((x * y) * z) -> rel (0 + x) x -> rel x (0 + x) -> rel (1 * x) x -> rel x (1 * x) -> rel (x * 1) x -> rel x (x * 1) -> rel (x * (y + z)) ((x * y) + (x * z)) -> rel ((x * y) + (x * z)) (x * (y + z)) -> rel ((x + y) * z) ((x * z) + (y * z)) -> rel ((x * z) + (y * z)) ((x + y) * z) -> rel (x * 0) 0 -> rel 0 (x * 0) -> rel (0 * x) 0 -> rel 0 (0 * x) -> rel (x + y) (y + x) -> RelSemiring ty rel

Projections:
.absorbl : ({rec:0} : RelSemiring ty rel) -> rel (x * 0) 0
.absorbl' : ({rec:0} : RelSemiring ty rel) -> rel 0 (x * 0)
.absorbr : ({rec:0} : RelSemiring ty rel) -> rel (0 * x) 0
.absorbr' : ({rec:0} : RelSemiring ty rel) -> rel 0 (0 * x)
.distribl : ({rec:0} : RelSemiring ty rel) -> rel (x * (y + z)) ((x * y) + (x * z))
.distribl' : ({rec:0} : RelSemiring ty rel) -> rel ((x * y) + (x * z)) (x * (y + z))
.distribr : ({rec:0} : RelSemiring ty rel) -> rel ((x + y) * z) ((x * z) + (y * z))
.distribr' : ({rec:0} : RelSemiring ty rel) -> rel ((x * z) + (y * z)) ((x + y) * z)
.impl : RelSemiring ty rel -> Num ty
.multAssoc : ({rec:0} : RelSemiring ty rel) -> rel ((x * y) * z) (x * (y * z))
.multAssoc' : ({rec:0} : RelSemiring ty rel) -> rel (x * (y * z)) ((x * y) * z)
.multCong : ({rec:0} : RelSemiring ty rel) -> rel x y -> rel x' y' -> rel (x * x') (y * y')
.multMonoid : RelSemiring ty rel -> RelMonoid ty rel
.multUnitl : ({rec:0} : RelSemiring ty rel) -> rel (1 * x) x
.multUnitl' : ({rec:0} : RelSemiring ty rel) -> rel x (1 * x)
.multUnitr : ({rec:0} : RelSemiring ty rel) -> rel (x * 1) x
.multUnitr' : ({rec:0} : RelSemiring ty rel) -> rel x (x * 1)
.plusAssoc : ({rec:0} : RelSemiring ty rel) -> rel ((x + y) + z) (x + (y + z))
.plusComm : ({rec:0} : RelSemiring ty rel) -> rel (x + y) (y + x)
.plusCong : ({rec:0} : RelSemiring ty rel) -> rel x y -> rel x' y' -> rel (x + x') (y + y')
.plusMonoid : RelSemiring ty rel -> RelCommMonoid ty rel
.plusUnit : ({rec:0} : RelSemiring ty rel) -> rel (0 + x) x
.plusUnit' : ({rec:0} : RelSemiring ty rel) -> rel x (0 + x)
.relNearRing : Preorder ty rel => RelSemiring ty rel -> RelNearRing ty rel
.impl : RelSemiring ty rel -> Num ty
Totality: total
Visibility: public export
impl : RelSemiring ty rel -> Num ty
Totality: total
Visibility: public export
.plusCong : ({rec:0} : RelSemiring ty rel) -> rel x y -> rel x' y' -> rel (x + x') (y + y')
Totality: total
Visibility: public export
plusCong : ({rec:0} : RelSemiring ty rel) -> rel x y -> rel x' y' -> rel (x + x') (y + y')
Totality: total
Visibility: public export
.multCong : ({rec:0} : RelSemiring ty rel) -> rel x y -> rel x' y' -> rel (x * x') (y * y')
Totality: total
Visibility: public export
multCong : ({rec:0} : RelSemiring ty rel) -> rel x y -> rel x' y' -> rel (x * x') (y * y')
Totality: total
Visibility: public export
.plusAssoc : ({rec:0} : RelSemiring ty rel) -> rel ((x + y) + z) (x + (y + z))
Totality: total
Visibility: public export
plusAssoc : ({rec:0} : RelSemiring ty rel) -> rel ((x + y) + z) (x + (y + z))
Totality: total
Visibility: public export
.multAssoc : ({rec:0} : RelSemiring ty rel) -> rel ((x * y) * z) (x * (y * z))
Totality: total
Visibility: public export
multAssoc : ({rec:0} : RelSemiring ty rel) -> rel ((x * y) * z) (x * (y * z))
Totality: total
Visibility: public export
.multAssoc' : ({rec:0} : RelSemiring ty rel) -> rel (x * (y * z)) ((x * y) * z)
Totality: total
Visibility: public export
multAssoc' : ({rec:0} : RelSemiring ty rel) -> rel (x * (y * z)) ((x * y) * z)
Totality: total
Visibility: public export
.plusUnit : ({rec:0} : RelSemiring ty rel) -> rel (0 + x) x
Totality: total
Visibility: public export
plusUnit : ({rec:0} : RelSemiring ty rel) -> rel (0 + x) x
Totality: total
Visibility: public export
.plusUnit' : ({rec:0} : RelSemiring ty rel) -> rel x (0 + x)
Totality: total
Visibility: public export
plusUnit' : ({rec:0} : RelSemiring ty rel) -> rel x (0 + x)
Totality: total
Visibility: public export
.multUnitl : ({rec:0} : RelSemiring ty rel) -> rel (1 * x) x
Totality: total
Visibility: public export
multUnitl : ({rec:0} : RelSemiring ty rel) -> rel (1 * x) x
Totality: total
Visibility: public export
.multUnitl' : ({rec:0} : RelSemiring ty rel) -> rel x (1 * x)
Totality: total
Visibility: public export
multUnitl' : ({rec:0} : RelSemiring ty rel) -> rel x (1 * x)
Totality: total
Visibility: public export
.multUnitr : ({rec:0} : RelSemiring ty rel) -> rel (x * 1) x
Totality: total
Visibility: public export
multUnitr : ({rec:0} : RelSemiring ty rel) -> rel (x * 1) x
Totality: total
Visibility: public export
.multUnitr' : ({rec:0} : RelSemiring ty rel) -> rel x (x * 1)
Totality: total
Visibility: public export
multUnitr' : ({rec:0} : RelSemiring ty rel) -> rel x (x * 1)
Totality: total
Visibility: public export
.distribl : ({rec:0} : RelSemiring ty rel) -> rel (x * (y + z)) ((x * y) + (x * z))
Totality: total
Visibility: public export
distribl : ({rec:0} : RelSemiring ty rel) -> rel (x * (y + z)) ((x * y) + (x * z))
Totality: total
Visibility: public export
.distribl' : ({rec:0} : RelSemiring ty rel) -> rel ((x * y) + (x * z)) (x * (y + z))
Totality: total
Visibility: public export
distribl' : ({rec:0} : RelSemiring ty rel) -> rel ((x * y) + (x * z)) (x * (y + z))
Totality: total
Visibility: public export
.distribr : ({rec:0} : RelSemiring ty rel) -> rel ((x + y) * z) ((x * z) + (y * z))
Totality: total
Visibility: public export
distribr : ({rec:0} : RelSemiring ty rel) -> rel ((x + y) * z) ((x * z) + (y * z))
Totality: total
Visibility: public export
.distribr' : ({rec:0} : RelSemiring ty rel) -> rel ((x * z) + (y * z)) ((x + y) * z)
Totality: total
Visibility: public export
distribr' : ({rec:0} : RelSemiring ty rel) -> rel ((x * z) + (y * z)) ((x + y) * z)
Totality: total
Visibility: public export
.absorbl : ({rec:0} : RelSemiring ty rel) -> rel (x * 0) 0
Totality: total
Visibility: public export
absorbl : ({rec:0} : RelSemiring ty rel) -> rel (x * 0) 0
Totality: total
Visibility: public export
.absorbl' : ({rec:0} : RelSemiring ty rel) -> rel 0 (x * 0)
Totality: total
Visibility: public export
absorbl' : ({rec:0} : RelSemiring ty rel) -> rel 0 (x * 0)
Totality: total
Visibility: public export
.absorbr : ({rec:0} : RelSemiring ty rel) -> rel (0 * x) 0
Totality: total
Visibility: public export
absorbr : ({rec:0} : RelSemiring ty rel) -> rel (0 * x) 0
Totality: total
Visibility: public export
.absorbr' : ({rec:0} : RelSemiring ty rel) -> rel 0 (0 * x)
Totality: total
Visibility: public export
absorbr' : ({rec:0} : RelSemiring ty rel) -> rel 0 (0 * x)
Totality: total
Visibility: public export
.plusComm : ({rec:0} : RelSemiring ty rel) -> rel (x + y) (y + x)
Totality: total
Visibility: public export
plusComm : ({rec:0} : RelSemiring ty rel) -> rel (x + y) (y + x)
Totality: total
Visibility: public export
mkRelSemiring : Reflexive ty rel => {auto impl : Num ty} -> (rel x y -> rel x' y' -> rel (x + x') (y + y')) -> (rel x y -> rel x' y' -> rel (x * x') (y * y')) -> (0 _ : (x + y) + z = x + (y + z)) -> (0 _ : (x * y) * z = x * (y * z)) -> (0 _ : 0 + x = x) -> (0 _ : 1 * x = x) -> (0 _ : x * 1 = x) -> (0 _ : x * (y + z) = (x * y) + (x * z)) -> (0 _ : (x + y) * z = (x * z) + (y * z)) -> (0 _ : x * 0 = 0) -> (0 _ : 0 * x = 0) -> (0 _ : x + y = y + x) -> RelSemiring ty rel
Totality: total
Visibility: public export
relNearRing : Preorder ty rel => RelSemiring ty rel -> RelNearRing ty rel
Totality: total
Visibility: public export
.relNearRing : Preorder ty rel => RelSemiring ty rel -> RelNearRing ty rel
Totality: total
Visibility: public export
plusMonoid : RelSemiring ty rel -> RelCommMonoid ty rel
Totality: total
Visibility: public export
.plusMonoid : RelSemiring ty rel -> RelCommMonoid ty rel
Totality: total
Visibility: public export
multMonoid : RelSemiring ty rel -> RelMonoid ty rel
Totality: total
Visibility: public export
.multMonoid : RelSemiring ty rel -> RelMonoid ty rel
Totality: total
Visibility: public export
record RelCommSemiring : (ty : Type) -> Rel ty -> Type
Totality: total
Visibility: public export
Constructor: 
MkRelCommSemiring : {auto impl : Num ty} -> (rel x y -> rel x' y' -> rel (x + x') (y + y')) -> (rel x y -> rel x' y' -> rel (x * x') (y * y')) -> rel ((x + y) + z) (x + (y + z)) -> rel ((x * y) * z) (x * (y * z)) -> rel (0 + x) x -> rel x (0 + x) -> rel (1 * x) x -> rel x (1 * x) -> rel (x * (y + z)) ((x * y) + (x * z)) -> rel ((x * y) + (x * z)) (x * (y + z)) -> rel (x * 0) 0 -> rel 0 (x * 0) -> rel (x + y) (y + x) -> rel (x * y) (y * x) -> RelCommSemiring ty rel

Projections:
.absorb : ({rec:0} : RelCommSemiring ty rel) -> rel (x * 0) 0
.absorb' : ({rec:0} : RelCommSemiring ty rel) -> rel 0 (x * 0)
.distrib : ({rec:0} : RelCommSemiring ty rel) -> rel (x * (y + z)) ((x * y) + (x * z))
.distrib' : ({rec:0} : RelCommSemiring ty rel) -> rel ((x * y) + (x * z)) (x * (y + z))
.impl : RelCommSemiring ty rel -> Num ty
.multAssoc : ({rec:0} : RelCommSemiring ty rel) -> rel ((x * y) * z) (x * (y * z))
.multComm : ({rec:0} : RelCommSemiring ty rel) -> rel (x * y) (y * x)
.multCong : ({rec:0} : RelCommSemiring ty rel) -> rel x y -> rel x' y' -> rel (x * x') (y * y')
.multMonoid : RelCommSemiring ty rel -> RelCommMonoid ty rel
.multUnit : ({rec:0} : RelCommSemiring ty rel) -> rel (1 * x) x
.multUnit' : ({rec:0} : RelCommSemiring ty rel) -> rel x (1 * x)
.plusAssoc : ({rec:0} : RelCommSemiring ty rel) -> rel ((x + y) + z) (x + (y + z))
.plusComm : ({rec:0} : RelCommSemiring ty rel) -> rel (x + y) (y + x)
.plusCong : ({rec:0} : RelCommSemiring ty rel) -> rel x y -> rel x' y' -> rel (x + x') (y + y')
.plusMonoid : RelCommSemiring ty rel -> RelCommMonoid ty rel
.plusUnit : ({rec:0} : RelCommSemiring ty rel) -> rel (0 + x) x
.plusUnit' : ({rec:0} : RelCommSemiring ty rel) -> rel x (0 + x)
.relSemiring : Preorder ty rel => RelCommSemiring ty rel -> RelSemiring ty rel
.impl : RelCommSemiring ty rel -> Num ty
Totality: total
Visibility: public export
impl : RelCommSemiring ty rel -> Num ty
Totality: total
Visibility: public export
.plusCong : ({rec:0} : RelCommSemiring ty rel) -> rel x y -> rel x' y' -> rel (x + x') (y + y')
Totality: total
Visibility: public export
plusCong : ({rec:0} : RelCommSemiring ty rel) -> rel x y -> rel x' y' -> rel (x + x') (y + y')
Totality: total
Visibility: public export
.multCong : ({rec:0} : RelCommSemiring ty rel) -> rel x y -> rel x' y' -> rel (x * x') (y * y')
Totality: total
Visibility: public export
multCong : ({rec:0} : RelCommSemiring ty rel) -> rel x y -> rel x' y' -> rel (x * x') (y * y')
Totality: total
Visibility: public export
.plusAssoc : ({rec:0} : RelCommSemiring ty rel) -> rel ((x + y) + z) (x + (y + z))
Totality: total
Visibility: public export
plusAssoc : ({rec:0} : RelCommSemiring ty rel) -> rel ((x + y) + z) (x + (y + z))
Totality: total
Visibility: public export
.multAssoc : ({rec:0} : RelCommSemiring ty rel) -> rel ((x * y) * z) (x * (y * z))
Totality: total
Visibility: public export
multAssoc : ({rec:0} : RelCommSemiring ty rel) -> rel ((x * y) * z) (x * (y * z))
Totality: total
Visibility: public export
.plusUnit : ({rec:0} : RelCommSemiring ty rel) -> rel (0 + x) x
Totality: total
Visibility: public export
plusUnit : ({rec:0} : RelCommSemiring ty rel) -> rel (0 + x) x
Totality: total
Visibility: public export
.plusUnit' : ({rec:0} : RelCommSemiring ty rel) -> rel x (0 + x)
Totality: total
Visibility: public export
plusUnit' : ({rec:0} : RelCommSemiring ty rel) -> rel x (0 + x)
Totality: total
Visibility: public export
.multUnit : ({rec:0} : RelCommSemiring ty rel) -> rel (1 * x) x
Totality: total
Visibility: public export
multUnit : ({rec:0} : RelCommSemiring ty rel) -> rel (1 * x) x
Totality: total
Visibility: public export
.multUnit' : ({rec:0} : RelCommSemiring ty rel) -> rel x (1 * x)
Totality: total
Visibility: public export
multUnit' : ({rec:0} : RelCommSemiring ty rel) -> rel x (1 * x)
Totality: total
Visibility: public export
.distrib : ({rec:0} : RelCommSemiring ty rel) -> rel (x * (y + z)) ((x * y) + (x * z))
Totality: total
Visibility: public export
distrib : ({rec:0} : RelCommSemiring ty rel) -> rel (x * (y + z)) ((x * y) + (x * z))
Totality: total
Visibility: public export
.distrib' : ({rec:0} : RelCommSemiring ty rel) -> rel ((x * y) + (x * z)) (x * (y + z))
Totality: total
Visibility: public export
distrib' : ({rec:0} : RelCommSemiring ty rel) -> rel ((x * y) + (x * z)) (x * (y + z))
Totality: total
Visibility: public export
.absorb : ({rec:0} : RelCommSemiring ty rel) -> rel (x * 0) 0
Totality: total
Visibility: public export
absorb : ({rec:0} : RelCommSemiring ty rel) -> rel (x * 0) 0
Totality: total
Visibility: public export
.absorb' : ({rec:0} : RelCommSemiring ty rel) -> rel 0 (x * 0)
Totality: total
Visibility: public export
absorb' : ({rec:0} : RelCommSemiring ty rel) -> rel 0 (x * 0)
Totality: total
Visibility: public export
.plusComm : ({rec:0} : RelCommSemiring ty rel) -> rel (x + y) (y + x)
Totality: total
Visibility: public export
plusComm : ({rec:0} : RelCommSemiring ty rel) -> rel (x + y) (y + x)
Totality: total
Visibility: public export
.multComm : ({rec:0} : RelCommSemiring ty rel) -> rel (x * y) (y * x)
Totality: total
Visibility: public export
multComm : ({rec:0} : RelCommSemiring ty rel) -> rel (x * y) (y * x)
Totality: total
Visibility: public export
mkRelCommSemiring : Reflexive ty rel => {auto impl : Num ty} -> (rel x y -> rel x' y' -> rel (x + x') (y + y')) -> (rel x y -> rel x' y' -> rel (x * x') (y * y')) -> (0 _ : (x + y) + z = x + (y + z)) -> (0 _ : (x * y) * z = x * (y * z)) -> (0 _ : 0 + x = x) -> (0 _ : 1 * x = x) -> (0 _ : x * (y + z) = (x * y) + (x * z)) -> (0 _ : x * 0 = 0) -> (0 _ : x + y = y + x) -> (0 _ : x * y = y * x) -> RelCommSemiring ty rel
Totality: total
Visibility: public export
relSemiring : Preorder ty rel => RelCommSemiring ty rel -> RelSemiring ty rel
Totality: total
Visibility: public export
.relSemiring : Preorder ty rel => RelCommSemiring ty rel -> RelSemiring ty rel
Totality: total
Visibility: public export
plusMonoid : RelCommSemiring ty rel -> RelCommMonoid ty rel
Totality: total
Visibility: public export
.plusMonoid : RelCommSemiring ty rel -> RelCommMonoid ty rel
Totality: total
Visibility: public export
multMonoid : RelCommSemiring ty rel -> RelCommMonoid ty rel
Totality: total
Visibility: public export
.multMonoid : RelCommSemiring ty rel -> RelCommMonoid ty rel
Totality: total
Visibility: public export
Thin : (rel : Rel ty) -> Preorder ty rel => CategoryR
Totality: total
Visibility: public export
Thin : (rel : Rel ty) -> Preorder ty rel => RelMonoid ty rel -> MonoidalR
Totality: total
Visibility: public export
Thin : (rel : Rel ty) -> Preorder ty rel => RelCommMonoid ty rel -> BraidedR
Totality: total
Visibility: public export
Thin : (rel : Rel ty) -> Preorder ty rel => RelCommMonoid ty rel -> SymmetricR
Totality: total
Visibility: public export
Thin : (rel : Rel ty) -> Preorder ty rel => RelNearRing ty rel -> BimonoidalR
Totality: total
Visibility: public export
Thin : (rel : Rel ty) -> Preorder ty rel => RelSemiring ty rel -> RigCategoryR
Totality: total
Visibility: public export
Thin : (rel : Rel ty) -> Preorder ty rel => RelCommSemiring ty rel -> SymRigCategoryR
Totality: total
Visibility: public export