Frex.Coproduct

Definitions and constructions for coproducts in the category of models

Definitions

record (<~.~>) : {Pres : Presentation} -> Model Pres -> Model Pres -> Type

  A cospan between models of a presentation. Looks a bit like this: \o/

Totality: total
Visibility: public export
Constructor: 

MkCospan : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> (Sink : Model Pres) -> L ~> Sink -> R ~> Sink -> L <~.~> R

Projections:

.Lft : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> ({rec:0} : L <~.~> R) -> L ~> Sink {rec:0}

  Left 'arm' of the cospan (\o/)

.Rgt : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> ({rec:0} : L <~.~> R) -> R ~> Sink {rec:0}

  Right 'arm' of the cospan (\o/)

.Sink : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> L <~.~> R -> Model Pres

  'Head' of the cospan (\o/)

Hints:

pres .signature = sig => Semantic (a <~.~> b) (Op sig)

pres .signature = sig => Semantic (a <~.~> b) (Term sig y)

Fixity Declaration: infixr operator, level 3

.Sink : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> L <~.~> R -> Model Pres

  'Head' of the cospan (\o/)

Totality: total
Visibility: public export

Sink : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> L <~.~> R -> Model Pres

  'Head' of the cospan (\o/)

Totality: total
Visibility: public export

.Lft : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> ({rec:0} : L <~.~> R) -> L ~> Sink {rec:0}

  Left 'arm' of the cospan (\o/)

Totality: total
Visibility: public export

Lft : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> ({rec:0} : L <~.~> R) -> L ~> Sink {rec:0}

  Left 'arm' of the cospan (\o/)

Totality: total
Visibility: public export

.Rgt : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> ({rec:0} : L <~.~> R) -> R ~> Sink {rec:0}

  Right 'arm' of the cospan (\o/)

Totality: total
Visibility: public export

Rgt : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> ({rec:0} : L <~.~> R) -> R ~> Sink {rec:0}

  Right 'arm' of the cospan (\o/)

Totality: total
Visibility: public export

0 PreservesLft : {Pres : Presentation} -> {L : Model Pres} -> {R : Model Pres} -> (C : L <~.~> R) -> (D : L <~.~> R) -> C .Sink ~> D .Sink -> Type

  `Pres`-homomorphism preserving the Lft-arm of a cospan

Totality: total
Visibility: public export

0 PreservesRgt : {Pres : Presentation} -> {L : Model Pres} -> {R : Model Pres} -> (C : L <~.~> R) -> (D : L <~.~> R) -> C .Sink ~> D .Sink -> Type

  `Pres`-homomorphism preserving the Rgt-arm of a cospan

Totality: total
Visibility: public export

record Preserves : {Pres : Presentation} -> {L : Model Pres} -> {R : Model Pres} -> (C : L <~.~> R) -> (D : L <~.~> R) -> C .Sink ~> D .Sink -> Type

  A morphism preserving both arms of a cospan

Totality: total
Visibility: public export
Constructor: 

IsPreserving : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 C : L <~.~> R} -> {0 D : L <~.~> R} -> {0 H : C .Sink ~> D .Sink} -> PreservesLft H -> PreservesRgt H -> Preserves C D H

Projections:

.Lft : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 C : L <~.~> R} -> {0 D : L <~.~> R} -> {0 H : C .Sink ~> D .Sink} -> Preserves C D H -> PreservesLft H

.Rgt : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 C : L <~.~> R} -> {0 D : L <~.~> R} -> {0 H : C .Sink ~> D .Sink} -> Preserves C D H -> PreservesRgt H

.Lft : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 C : L <~.~> R} -> {0 D : L <~.~> R} -> {0 H : C .Sink ~> D .Sink} -> Preserves C D H -> PreservesLft H

Totality: total
Visibility: public export

Lft : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 C : L <~.~> R} -> {0 D : L <~.~> R} -> {0 H : C .Sink ~> D .Sink} -> Preserves C D H -> PreservesLft H

Totality: total
Visibility: public export

.Rgt : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 C : L <~.~> R} -> {0 D : L <~.~> R} -> {0 H : C .Sink ~> D .Sink} -> Preserves C D H -> PreservesRgt H

Totality: total
Visibility: public export

Rgt : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 C : L <~.~> R} -> {0 D : L <~.~> R} -> {0 H : C .Sink ~> D .Sink} -> Preserves C D H -> PreservesRgt H

Totality: total
Visibility: public export

record (~>) : {Pres : Presentation} -> {L : Model Pres} -> {R : Model Pres} -> L <~.~> R -> L <~.~> R -> Type

  A morphism between cospans

Totality: total
Visibility: public export
Constructor: 

MkCospanMorphism : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 C : L <~.~> R} -> {0 D : L <~.~> R} -> (H : C .Sink ~> D .Sink) -> Preserves C D H -> C ~> D

Projections:

.H : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 C : L <~.~> R} -> {0 D : L <~.~> R} -> C ~> D -> C .Sink ~> D .Sink

  A morphism between the sinks

.preserve : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 C : L <~.~> R} -> {0 D : L <~.~> R} -> ({rec:0} : C ~> D) -> Preserves C D (H {rec:0})

  Preserving both arms

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

.H : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 C : L <~.~> R} -> {0 D : L <~.~> R} -> C ~> D -> C .Sink ~> D .Sink

  A morphism between the sinks

Totality: total
Visibility: public export

H : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 C : L <~.~> R} -> {0 D : L <~.~> R} -> C ~> D -> C .Sink ~> D .Sink

  A morphism between the sinks

Totality: total
Visibility: public export

.preserve : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 C : L <~.~> R} -> {0 D : L <~.~> R} -> ({rec:0} : C ~> D) -> Preserves C D (H {rec:0})

  Preserving both arms

Totality: total
Visibility: public export

preserve : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 C : L <~.~> R} -> {0 D : L <~.~> R} -> ({rec:0} : C ~> D) -> Preserves C D (H {rec:0})

  Preserving both arms

Totality: total
Visibility: public export

Extender : {Pres : Presentation} -> {L : Model Pres} -> {R : Model Pres} -> L <~.~> R -> Type

  Weak initiality: for any other cospan there is a cospan morphism from Coprod into it

Totality: total
Visibility: public export

0 ExtenderFunction : {Pres : Presentation} -> {L : Model Pres} -> {R : Model Pres} -> L <~.~> R -> Type

  Data for function underlying an Extender

Totality: total
Visibility: public export

0 ExtenderSetoidHomomorphism : {Pres : Presentation} -> {L : Model Pres} -> {R : Model Pres} -> L <~.~> R -> Type

  Data for SetoidHomomorphism underlying an Extender

Totality: total
Visibility: public export

0 ExtenderHomomorphism : {Pres : Presentation} -> {L : Model Pres} -> {R : Model Pres} -> L <~.~> R -> Type

  Data for AlgebraHomomorphism underlying an Extender

Totality: total
Visibility: public export

0 Uniqueness : {Pres : Presentation} -> {L : Model Pres} -> {R : Model Pres} -> L <~.~> R -> Type

  There's at most one cospan morphism out of `Coprod` into any other cospan

Totality: total
Visibility: public export

record Universality : {Pres : Presentation} -> {L : Model Pres} -> {R : Model Pres} -> L <~.~> R -> Type

  A cospan is (co)universal when it is initial

Totality: total
Visibility: public export
Constructor: 

IsUniversal : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 Coprod : L <~.~> R} -> Extender -> Uniqueness -> Universality Coprod

Projections:

.Exists : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 Coprod : L <~.~> R} -> Universality Coprod -> Extender

.Unique : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 Coprod : L <~.~> R} -> Universality Coprod -> Uniqueness

.Exists : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 Coprod : L <~.~> R} -> Universality Coprod -> Extender

Totality: total
Visibility: public export

Exists : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 Coprod : L <~.~> R} -> Universality Coprod -> Extender

Totality: total
Visibility: public export

.Unique : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 Coprod : L <~.~> R} -> Universality Coprod -> Uniqueness

Totality: total
Visibility: public export

Unique : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> {0 Coprod : L <~.~> R} -> Universality Coprod -> Uniqueness

Totality: total
Visibility: public export

record Coproduct : {Pres : Presentation} -> Model Pres -> Model Pres -> Type

  A coproduct of two models is a universal cospan between them

Totality: total
Visibility: public export
Constructor: 

MkCoproduct : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> (Data : L <~.~> R) -> Universality Data -> Coproduct L R

Projections:

.Data : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> Coproduct L R -> L <~.~> R

.UP : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> ({rec:0} : Coproduct L R) -> Universality (Data {rec:0})

Hints:

pres .signature = sig => Semantic (Coproduct a b) (Op sig)

pres .signature = sig => Semantic (Coproduct a b) (Term sig y)

.Data : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> Coproduct L R -> L <~.~> R

Totality: total
Visibility: public export

Data : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> Coproduct L R -> L <~.~> R

Totality: total
Visibility: public export

.UP : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> ({rec:0} : Coproduct L R) -> Universality (Data {rec:0})

Totality: total
Visibility: public export

UP : {0 Pres : Presentation} -> {0 L : Model Pres} -> {0 R : Model Pres} -> ({rec:0} : Coproduct L R) -> Universality (Data {rec:0})

Totality: total
Visibility: public export