Frex.Model

Models for a `Frex.Presentation` and associated definitions

Definitions

0 models : (a : SetoidAlgebra sig) -> (eq : Equation sig) -> (Fin (eq .support) -> U (a .algebra)) -> Type

  States: The `sig`-algebra `a` satisfies the equation `eq`: for all
  environments, the interpretations of the lhs and rhs are in the
  setoid equivalence.

Totality: total
Visibility: public export

0 (=|) : (eq : Equation sig) -> (a : SetoidAlgebra sig ** Fin (eq .support) -> U (a .algebra)) -> Type

  Like `models`, but the arguments are reversed and packed slightly
  more compactly, makes nice syntax sometimes

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 1

eqPreservation : (eq : (Term sig x, Term sig x)) -> (env : (x -> U a)) -> (h : a ~> b) -> (a .equivalence) .relation (a .Sem (fst eq) env) (a .Sem (snd eq) env) -> (b .equivalence) .relation (b .Sem (fst eq) ((h .H) .H . env)) (b .Sem (snd eq) ((h .H) .H . env))

  Homomorphisms preserve equations in an environment

Totality: total
Visibility: public export

0 ValidatesEquation : Equation sig -> SetoidAlgebra sig -> Type

  States: `pres.signature`-algebra `a` satisfies the given equation.

Totality: total
Visibility: public export

0 Validates : (pres : Presentation) -> SetoidAlgebra (pres .signature) -> Type

  States: `pres.signature`-algebra `a` satisfies all the axioms of `pres`.

Totality: total
Visibility: public export

semPreservation : (iso : a <~> b) -> (t : Term sig x) -> (env : (x -> U b)) -> (b .equivalence) .relation (bindTerm t env) (((iso .Iso) .Fwd) .H (a .Sem t (((iso .Iso) .Bwd) .H . env)))

  Isomorphisms let us replace the semantics of one algebra with another

Totality: total
Visibility: public export

isoPreservesEq : (iso : a <~> b) -> (eq : Equation sig) -> (env : (Fin (eq .support) -> U b)) -> eq =| (a ** ((iso .Iso) .Bwd) .H . env) -> eq =| (b ** env)

  Isomorphisms preserve all equations

Totality: total
Visibility: public export

isoPreservesModels : (pres : Presentation) -> a <~> b -> Validates pres a -> Validates pres b

  Algebra isomorphisms preserve transport models

Totality: total
Visibility: public export

record Model : Presentation -> Type

  A model for an algebraic theory

Totality: total
Visibility: public export
Constructor: 

MkModel : {0 Pres : Presentation} -> (Algebra : SetoidAlgebra (Pres .signature)) -> Validates Pres Algebra -> Model Pres

Projections:

.Algebra : {0 Pres : Presentation} -> Model Pres -> SetoidAlgebra (Pres .signature)

  Algebra structure for the operations

.Validate : {0 Pres : Presentation} -> ({rec:0} : Model Pres) -> Validates Pres (Algebra {rec:0})

  The algebra validates all the equations

Hints:

Cast (Model pres) Setoid

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)

.Algebra : {0 Pres : Presentation} -> Model Pres -> SetoidAlgebra (Pres .signature)

  Algebra structure for the operations

Totality: total
Visibility: public export

Algebra : {0 Pres : Presentation} -> Model Pres -> SetoidAlgebra (Pres .signature)

  Algebra structure for the operations

Totality: total
Visibility: public export

.Validate : {0 Pres : Presentation} -> ({rec:0} : Model Pres) -> Validates Pres (Algebra {rec:0})

  The algebra validates all the equations

Totality: total
Visibility: public export

Validate : {0 Pres : Presentation} -> ({rec:0} : Model Pres) -> Validates Pres (Algebra {rec:0})

  The algebra validates all the equations

Totality: total
Visibility: public export

cast : (a : Model pres) -> Preorder (((a .Algebra) .algebra) .U) (((a .Algebra) .equivalence) .relation)

Totality: total
Visibility: public export

0 U : Model pres -> Type

  Type carrying the model

Totality: total
Visibility: public export

.equivalence : (a : Model pres) -> Equivalence (U a)

Totality: total
Visibility: public export

0 .rel : (a : Model pres) -> U a -> U a -> Type

  Equivalence relation underlying a model

Totality: total
Visibility: public export

(~>) : Model pres -> Model pres -> Type

  Homomorphism between models

Totality: total
Visibility: public export
Fixity Declarations:
infix operator, level 5
infix operator, level 5
infix operator, level 5

id : (a : Model pres) -> a ~> a

  Identity homomorphism between models

Totality: total
Visibility: public export

.sem : (a : Model pres) -> (pres .signature) .OpWithArity n -> ary n (U a)

  nary interpretation of an operator in a model

Totality: total
Visibility: public export

(~~>) : Model pres -> Model pres -> Setoid

  The setoid of homomorphisms between models with pointwise equivalence.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 5

post : b ~> c -> (a ~~> b) ~> (a ~~> c)

Totality: total
Visibility: public export

pre : a2 ~> a1 -> (a1 ~~> b) ~> (a2 ~~> b)

Totality: total
Visibility: public export

transport : (a : Model pres) -> a .Algebra <~> b -> Model pres

Totality: total
Visibility: public export

.cong : (a : Model pres) -> (0 n : Nat) -> (t : Term (pres .signature) (Either (U a) (Fin n))) -> (lhs : Vect n (U a)) -> (rhs : Vect n (U a)) -> HVect (tabulate (\i => ((cast a) .equivalence) .relation (index i lhs) (index i rhs))) -> ((cast a) .equivalence) .relation (a .Sem t (either (Delay id) (Delay (flip index lhs)))) (a .Sem t (either (Delay id) (Delay (flip index rhs))))

  N-ary congruence in a term with `n` varialbes

Totality: total
Visibility: public export

Dyn : Fin n -> Term sig (Either a (Fin n))

Totality: total
Visibility: public export

Sta : a -> Term sig (Either a (Fin n))

Totality: total
Visibility: public export

.validate : (a : Model pres) -> (ax : Axiom pres) -> (env : Vect (support (pres .axiom ax)) (U a)) -> pres .axiom ax =| (a .Algebra ** \i => index i env)

Totality: total
Visibility: public export