Notation.Semantic

A type is semantic w.r.t. two other types if it can interpret one type as another

Definitions

interface Semantic : Type -> Type -> Type

Parameters: a, b
Methods:

0 .SemType : a -> b -> Type

.Sem : (x : a) -> (y : b) -> x .SemType y

Implementations:

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

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

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

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

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

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

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

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

pres .signature = sig => Semantic (Model pres) (Op sig)

pres .signature = sig => Semantic (Model pres) (Term sig x)

pres .signature = sig => Semantic (ModelOver pres x) (Op sig)

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

pres .signature = sig => Semantic (Free pres x) (Op sig)

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

Semantic (Algebra sig) (Op sig)

Semantic (Algebra sig) (Term sig x)

Semantic (SetoidAlgebra sig) (Op sig)

Semantic (SetoidAlgebra sig) (Term sig x)

0 .SemType : Semantic a b => a -> b -> Type

Totality: total
Visibility: public export

.Sem : {auto __con : Semantic a b} -> (x : a) -> (y : b) -> x .SemType y

Totality: total
Visibility: public export