Frex.Frex.Construction

Construct the free extension of a model over a setoid
Small print: the setoid's equivalence relation may not be decidable

The frex `a[s]` of a `pres`-model `a` over a setoid `s` is given
by the free model `F s` of the following presentation over the
setoid `s`. First, we add all the elements `x : U a` as constants
`Constant x : 0`. Then, we add the following evaluation equations
to the `pres` axioms:

  f (Constant x1, ..., Constant xn)
  = Constant $ a.Sem f (x1,..., xn)

Reexports

Definitions

data EvaluationSigOperation : Signature -> (0 _ : Type) -> Nat -> Type

Totality: total
Visibility: public export
Constructors:

Op : sig .OpWithArity n -> EvaluationSigOperation sig a n

Constant : a -> EvaluationSigOperation sig a 0

EvaluationSig : Signature -> (0 _ : Type) -> Signature

Visibility: public export

withEvaluation : Show c => Printer sig a -> Printer (EvaluationSig sig c) a

Visibility: export

EvalEmbed : (sig : Signature) -> sig ~> EvaluationSig sig a

Visibility: public export

data EvaluationAxiom : Signature -> Type -> Setoid -> Type

Totality: total
Visibility: public export
Constructors:

Axiom : axioms -> EvaluationAxiom sig axioms a

Evaluation : sig .OpWithArity n -> Vect n (U a) -> EvaluationAxiom sig axioms a

Assumption : (a .equivalence) .relation x y -> EvaluationAxiom sig axioms a

EvaluationTheory : (pres : Presentation) -> (a : SetoidAlgebra (pres .signature)) -> EvaluationAxiom (pres .signature) (pres .Axiom) (cast a) -> Equation (EvaluationSig (pres .signature) (U a))

Visibility: public export

EvaluationPresentation : (pres : Presentation) -> SetoidAlgebra (pres .signature) -> Presentation

Visibility: public export

castEval : SetoidAlgebra (EvaluationSig sig a) -> SetoidAlgebra sig

Visibility: public export

lemma : {auto a : Algebra sig} -> (n : Nat) -> (f : (Fin n -> x)) -> (env : (x -> U a)) -> bindTerms (map Done (tabulate f)) env = tabulate (env . f)

Visibility: export

lemma2 : {auto a : Algebra sig} -> (i : Fin n) -> (ts : Vect n (Term sig x)) -> (env : (x -> U a)) -> index i (bindTerms ts env) = bindTerm (index i ts) env

Visibility: export

coherence : (a : SetoidAlgebra (EvaluationSig sig s)) -> (t : Term sig x) -> (env : (x -> U a)) -> a .Sem (cast t) env = (castEval a) .Sem t env

Visibility: export

coherenceTerms : (a : SetoidAlgebra (EvaluationSig sig s)) -> (ts : Vect n (Term sig x)) -> (env : (x -> U a)) -> bindTerms (castTerms (EvalEmbed sig) ts) env = bindTerms ts env

Visibility: export

castEval : Model (EvaluationPresentation pres a) -> Model pres

Visibility: public export

castEval : b ~> c -> castEval b ~> castEval c

Visibility: public export

freeAsExtension : Free (EvaluationPresentation pres (a .Algebra)) s -> Extension a s

Visibility: public export

.OverAlgebra : Extension a s -> SetoidAlgebra ((EvaluationPresentation pres (a .Algebra)) .signature)

Visibility: public export

.OverAlgebraCoherence : (other : Extension a s) -> (env : (x -> U (other .Model))) -> (t : Term (pres .signature) x) -> (castEval (other .OverAlgebra)) .Sem t env = (other .Model) .Sem t env

Visibility: export

OverAlgebraCoherenceAux : (other : Extension a s) -> (env : (x -> U (other .Model))) -> (ts : Vect n (Term (pres .signature) x)) -> bindTerms ts env = bindTerms ts env

Visibility: export

OverAlgebraNop : (other : Extension a s) -> (xs : Vect n (U a)) -> (env : (x -> U (other .Model))) -> bindTerms (map (\x => Call (MkOp (Constant x)) []) xs) env = map (((other .Embed) .H) .H) xs

Visibility: export

.Over : Extension a s -> ModelOver (EvaluationPresentation pres (a .Algebra)) s

Visibility: public export

Extender : (fs : Free (EvaluationPresentation pres (a .Algebra)) s) -> Extender (freeAsExtension fs)

Visibility: public export

Uniqueness : (fs : Free (EvaluationPresentation pres (a .Algebra)) s) -> Uniqueness (freeAsExtension fs)

Visibility: public export

FrexByFree : Free (EvaluationPresentation pres (a .Algebra)) s -> Frex a s

Visibility: public export

Frex : (a : Model pres) -> (s : Setoid) -> Frex a s

Visibility: public export