Frex.Frex

Definitions and constructions for free extensions

Definitions

record Extension : {Pres : Presentation} -> Model Pres -> Setoid -> Type

Totality: total
Visibility: public export
Constructor: 

MkExtension : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> (Model : Model Pres) -> A ~> Model -> X ~> cast Model -> Extension A X

Projections:

.Embed : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> ({rec:0} : Extension A X) -> A ~> Model {rec:0}

.Model : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> Extension A X -> Model Pres

.Var : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> ({rec:0} : Extension A X) -> X ~> cast (Model {rec:0})

Hints:

pres .signature = sig => Semantic (Extension a x) (Op sig)

pres .signature = sig => Semantic (Extension a x) (Term sig y)

.Model : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> Extension A X -> Model Pres

Totality: total
Visibility: public export

Model : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> Extension A X -> Model Pres

Totality: total
Visibility: public export

.Embed : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> ({rec:0} : Extension A X) -> A ~> Model {rec:0}

Totality: total
Visibility: public export

Embed : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> ({rec:0} : Extension A X) -> A ~> Model {rec:0}

Totality: total
Visibility: public export

.Var : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> ({rec:0} : Extension A X) -> X ~> cast (Model {rec:0})

Totality: total
Visibility: public export

Var : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> ({rec:0} : Extension A X) -> X ~> cast (Model {rec:0})

Totality: total
Visibility: public export

record (~>) : {Pres : Presentation} -> {A : Model Pres} -> {X : Setoid} -> Extension A X -> Extension A X -> Type

Totality: total
Visibility: public export
Constructor: 

MkExtensionMorphism : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Extension1 : Extension A X} -> {0 Extension2 : Extension A X} -> (H : Extension1 .Model ~> Extension2 .Model) -> ((cast A ~~> Extension2 .Model) .equivalence) .relation (H . Extension1 .Embed) (Extension2 .Embed) -> ((X ~~> cast (Extension2 .Model)) .equivalence) .relation (H .H . Extension1 .Var) (Extension2 .Var) -> Extension1 ~> Extension2

Projections:

.H : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Extension1 : Extension A X} -> {0 Extension2 : Extension A X} -> Extension1 ~> Extension2 -> Extension1 .Model ~> Extension2 .Model

.PreserveEmbed : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Extension1 : Extension A X} -> {0 Extension2 : Extension A X} -> ({rec:0} : Extension1 ~> Extension2) -> ((cast A ~~> Extension2 .Model) .equivalence) .relation (H {rec:0} . Extension1 .Embed) (Extension2 .Embed)

.PreserveVar : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Extension1 : Extension A X} -> {0 Extension2 : Extension A X} -> ({rec:0} : Extension1 ~> Extension2) -> ((X ~~> cast (Extension2 .Model)) .equivalence) .relation ((H {rec:0}) .H . Extension1 .Var) (Extension2 .Var)

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

.H : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Extension1 : Extension A X} -> {0 Extension2 : Extension A X} -> Extension1 ~> Extension2 -> Extension1 .Model ~> Extension2 .Model

Totality: total
Visibility: public export

H : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Extension1 : Extension A X} -> {0 Extension2 : Extension A X} -> Extension1 ~> Extension2 -> Extension1 .Model ~> Extension2 .Model

Totality: total
Visibility: public export

.PreserveEmbed : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Extension1 : Extension A X} -> {0 Extension2 : Extension A X} -> ({rec:0} : Extension1 ~> Extension2) -> ((cast A ~~> Extension2 .Model) .equivalence) .relation (H {rec:0} . Extension1 .Embed) (Extension2 .Embed)

Totality: total
Visibility: public export

PreserveEmbed : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Extension1 : Extension A X} -> {0 Extension2 : Extension A X} -> ({rec:0} : Extension1 ~> Extension2) -> ((cast A ~~> Extension2 .Model) .equivalence) .relation (H {rec:0} . Extension1 .Embed) (Extension2 .Embed)

Totality: total
Visibility: public export

.PreserveVar : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Extension1 : Extension A X} -> {0 Extension2 : Extension A X} -> ({rec:0} : Extension1 ~> Extension2) -> ((X ~~> cast (Extension2 .Model)) .equivalence) .relation ((H {rec:0}) .H . Extension1 .Var) (Extension2 .Var)

Totality: total
Visibility: public export

PreserveVar : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Extension1 : Extension A X} -> {0 Extension2 : Extension A X} -> ({rec:0} : Extension1 ~> Extension2) -> ((X ~~> cast (Extension2 .Model)) .equivalence) .relation ((H {rec:0}) .H . Extension1 .Var) (Extension2 .Var)

Totality: total
Visibility: public export

Extender : Extension a x -> Type

Totality: total
Visibility: public export

0 ExtenderFunction : Extension a x -> Type

Totality: total
Visibility: public export

0 ExtenderIsHomomorphism : (frex : Extension a x) -> ExtenderFunction frex -> Type

Totality: total
Visibility: public export

0 ExtenderIsAlgebraHomomorphism : (frex : Extension a x) -> ExtenderFunction frex -> Type

Totality: total
Visibility: public export

0 ExtenderHomomorphism : Extension a x -> Type

Totality: total
Visibility: public export

0 ExtenderPreservesEmbedding : (frex : Extension a x) -> ExtenderHomomorphism frex -> Type

Totality: total
Visibility: public export

0 ExtenderPreservesVars : (frex : Extension a x) -> ExtenderHomomorphism frex -> Type

Totality: total
Visibility: public export

0 extenderIsUnique : (frex : Extension a x) -> Extender frex -> Type

Totality: total
Visibility: public export

0 Uniqueness : Extension a x -> Type

Totality: total
Visibility: public export

0 SinceExtenderIsUnique : (frex : Extension a x) -> (extender : Extender frex) -> extenderIsUnique frex extender -> Uniqueness frex

Totality: total
Visibility: public export

record Universality : {Pres : Presentation} -> {A : Model Pres} -> {X : Setoid} -> Extension A X -> Type

Totality: total
Visibility: public export
Constructor: 

IsUniversal : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Frex : Extension A X} -> Extender Frex -> Uniqueness Frex -> Universality Frex

Projections:

.Exists : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Frex : Extension A X} -> Universality Frex -> Extender Frex

.Unique : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Frex : Extension A X} -> Universality Frex -> Uniqueness Frex

.Exists : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Frex : Extension A X} -> Universality Frex -> Extender Frex

Totality: total
Visibility: public export

Exists : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Frex : Extension A X} -> Universality Frex -> Extender Frex

Totality: total
Visibility: public export

.Unique : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Frex : Extension A X} -> Universality Frex -> Uniqueness Frex

Totality: total
Visibility: public export

Unique : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> {0 Frex : Extension A X} -> Universality Frex -> Uniqueness Frex

Totality: total
Visibility: public export

record Frex : {Pres : Presentation} -> Model Pres -> Setoid -> Type

Totality: total
Visibility: public export
Constructor: 

MkFrex : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> (Data : Extension A X) -> Universality Data -> Frex A X

Projections:

.Data : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> Frex A X -> Extension A X

.UP : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> ({rec:0} : Frex A X) -> Universality (Data {rec:0})

Hints:

pres .signature = sig => Semantic (Frex a x) (Op sig)

pres .signature = sig => Semantic (Frex a x) (Term sig y)

.Data : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> Frex A X -> Extension A X

Totality: total
Visibility: public export

Data : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> Frex A X -> Extension A X

Totality: total
Visibility: public export

.UP : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> ({rec:0} : Frex A X) -> Universality (Data {rec:0})

Totality: total
Visibility: public export

UP : {0 Pres : Presentation} -> {0 A : Model Pres} -> {0 X : Setoid} -> ({rec:0} : Frex A X) -> Universality (Data {rec:0})

Totality: total
Visibility: public export

CoproductAlgebraWithFree : (free : Free pres x) -> Coproduct a ((free .Data) .Model) -> Frex a x

Totality: total
Visibility: public export

CoproductsAndFreeFrex : ((a : Model pres) -> (b : Model pres) -> Coproduct a b) -> Free pres x -> (a : Model pres) -> Frex a x

Totality: total
Visibility: public export

Frexlet : Type

Totality: total
Visibility: public export