Frexlet.Monoid.Commutative.Coproduct

The coproduct of two commutative monoids is their cartesian product

Reexports

import public Frexlet.Monoid.Commutative.Nat
import public Data.Vect.Extra

Definitions

CoprodAlgebraStructure : CommutativeMonoid -> CommutativeMonoid -> Algebra Signature: Totality: total
Visibility: public export
CoprodSetoidEquivalence : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> Equivalence (U a, U b): Totality: total
Visibility: public export
CoprodSetoid : CommutativeMonoid -> CommutativeMonoid -> Setoid: Totality: total
Visibility: public export
CoprodAlgebraCongruence : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> (op : Op Signature) -> CongruenceWRT (CoprodSetoid a b) ((CoprodAlgebraStructure a b) .Sem op): Totality: total
Visibility: public export
CoprodAlgebra : CommutativeMonoid -> CommutativeMonoid -> MonoidStructure: Totality: total
Visibility: public export
CoprodValidate : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> Validates CommutativeMonoidTheory (CoprodAlgebra a b): Totality: total
Visibility: public export
Coprod : CommutativeMonoid -> CommutativeMonoid -> CommutativeMonoid: Totality: total
Visibility: public export
CoprodLftFunction : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> U a -> U (Coprod a b): Totality: total
Visibility: public export
CoprodLftSetoidHomomorphism : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> SetoidHomomorphism (cast a) (cast (Coprod a b)) (CoprodLftFunction a b): Totality: total
Visibility: public export
CoprodLftHomomorphism : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> Homomorphism (a .Algebra) ((Coprod a b) .Algebra) (CoprodLftFunction a b): Totality: total
Visibility: public export
CoprodRgtFunction : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> U b -> U (Coprod a b): Totality: total
Visibility: public export
CoprodRgtSetoidHomomorphism : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> SetoidHomomorphism (cast b) (cast (Coprod a b)) (CoprodRgtFunction a b): Totality: total
Visibility: public export
CoprodRgtHomomorphism : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> Homomorphism (b .Algebra) ((Coprod a b) .Algebra) (CoprodRgtFunction a b): Totality: total
Visibility: public export
Coproduct : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> a <~.~> b: Totality: total
Visibility: public export
ExtenderFunction : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> ExtenderFunction: Totality: total
Visibility: public export
ExtenderSetoidHomomorphism : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> ExtenderSetoidHomomorphism: Totality: total
Visibility: public export
ExtenderIsHomomorphism : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> (other : a <~.~> b) -> Homomorphism ((Coprod a b) .Algebra) ((other .Sink) .Algebra) (ExtenderFunction a b other): Totality: total
Visibility: public export
Extender : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> Extender: Totality: total
Visibility: public export
normalForm : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> (xy : U (Coprod a b)) -> (Coprod a b) .rel ((fst xy, O1) .+. (O1, snd xy)) xy: Totality: total
Visibility: public export
extenderUniqueness : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> (other : a <~.~> b) -> (extend : Coproduct a b ~> other) -> (xy : U (Coprod a b)) -> (other .Sink) .rel (((extend .H) .H) .H xy) ((((Extender a b other) .H) .H) .H xy): Totality: total
Visibility: public export
Uniqueness : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> Uniqueness: Totality: total
Visibility: public export
CoproductCospan : (a : CommutativeMonoid) -> (b : CommutativeMonoid) -> Coproduct a b: Totality: total
Visibility: public export