Frex.Free.Construction

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

Definitions

record PresetoidAlgebra : Signature -> Type

  Auxiliary abstraction: an algebra with a relation over it

Totality: total
Visibility: public export
Constructor: 

MkPresetoidAlgebra : {0 Sig : Signature} -> (algebra : Algebra Sig) -> (0 _ : (U algebra -> U algebra -> Type)) -> PresetoidAlgebra Sig

Projections:

.algebra : {0 Sig : Signature} -> PresetoidAlgebra Sig -> Algebra Sig

0 .relation : {0 Sig : Signature} -> ({rec:0} : PresetoidAlgebra Sig) -> U (algebra {rec:0}) -> U (algebra {rec:0}) -> Type

Hint: 

Cast (SetoidAlgebra sig) (PresetoidAlgebra sig)

.algebra : {0 Sig : Signature} -> PresetoidAlgebra Sig -> Algebra Sig

Totality: total
Visibility: public export

algebra : {0 Sig : Signature} -> PresetoidAlgebra Sig -> Algebra Sig

Totality: total
Visibility: public export

0 .relation : {0 Sig : Signature} -> ({rec:0} : PresetoidAlgebra Sig) -> U (algebra {rec:0}) -> U (algebra {rec:0}) -> Type

Totality: total
Visibility: public export

0 relation : {0 Sig : Signature} -> ({rec:0} : PresetoidAlgebra Sig) -> U (algebra {rec:0}) -> U (algebra {rec:0}) -> Type

Totality: total
Visibility: public export

0 U : PresetoidAlgebra sig -> Type

  Carrier of underlying algebra

Totality: total
Visibility: public export

data (|-) : (a : PresetoidAlgebra (pres .signature)) -> Rel (U a)

  The provability relation of equational logic: given an algebra
  with a binary relation over it, thought of as a collection of
  equality assumptions, `a |- x y` are the proofs that x = y follows
  from these assumptions, the axioms of `pres`, and the deduction
  rules of equational logic.

Totality: total
Visibility: public export
Constructors:

Include : a .relation x y -> (|-) a x y

  Include assumptions in `a` as thereoms.

Refl : (x : U a) -> (|-) a x x

  Reflexivity

Sym : (|-) a x y -> (|-) a y x

Transitive : (|-) a x y -> (|-) a y z -> (|-) a x z

ByAxiom : (eq : Axiom pres) -> (env : (Fin ((pres .axiom eq) .support) -> U a)) -> (|-) a (bindTerm ((pres .axiom eq) .lhs) env) (bindTerm ((pres .axiom eq) .rhs) env)

  Instances of axioms are theorems

Congruence : (t : Term (pres .signature) (Fin n)) -> ((x : Fin n) -> (|-) a (lhs x) (rhs x)) -> (|-) a (bindTerm t lhs) (bindTerm t rhs)

  Theorems are congruences w.r.t. algebraic terms

Fixity Declaration: infix operator, level 4

quotientSetoid : (pres : Presentation) -> PresetoidAlgebra (pres .signature) -> Setoid

Totality: total
Visibility: public export

quotientSetoidAlgebra : (pres : Presentation) -> PresetoidAlgebra (pres .signature) -> SetoidAlgebra (pres .signature)

Totality: total
Visibility: public export

QuotientModel : (pres : Presentation) -> PresetoidAlgebra (pres .signature) -> Model pres

  Quotient an algebra and a set of assumptions by the equational theory generated by it

Totality: total
Visibility: public export

data FreePresetoid : (sig : Signature) -> (x : Setoid) -> Term sig (U x) -> Term sig (U x) -> Type

  Auxiliary data structure: promote the equivalence relation of a
  setoid to a relation (PER, in fact) over the variable terms.

Totality: total
Visibility: public export
Constructor: 

Assume : (x .equivalence) .relation i j -> FreePresetoid sig x (Done i) (Done j)

Hint: 

Show (FreePresetoid sig x u v)

QuotientData : (pres : Presentation) -> Setoid -> PresetoidAlgebra (pres .signature)

  The algebra and relation over it to generate the equational
  theorems of the theory

Totality: total
Visibility: public export

F : (pres : Presentation) -> Setoid -> Model pres

  The free model over a setoid

Totality: total
Visibility: public export

FreeDataEnv : (pres : Presentation) -> (x : Setoid) -> x ~> cast (F pres x)

  The environment data for the universal property of the free model

Totality: total
Visibility: public export

FreeData : (pres : Presentation) -> (x : Setoid) -> ModelOver pres x

  Data for the universal property of the free model

Totality: total
Visibility: public export

freeSem : (pres : Presentation) -> (x : Setoid) -> (t : Term (pres .signature) (U x)) -> bindTerm t (((FreeData pres x) .Env) .H) = t

  Semantics in the free algebra is the identity

Totality: total
Visibility: export

FreeUPExistsHHH : (pres : Presentation) -> (x : Setoid) -> ExtenderFunction

  The function underlying the mediating homomorphism in the
  universal property of the free model

Totality: total
Visibility: public export

FreeUPExistsHHHomomorphic : (pres : Presentation) -> (x : Setoid) -> (other : ModelOver pres x) -> SetoidHomomorphism (cast (F pres x)) (cast (other .Model)) (FreeUPExistsHHH pres x other)

  States: The mediating homomorphism in the universal property of
  the free model is a setoid homomorphism.

Totality: total
Visibility: public export

FreeUPExistsHH : (pres : Presentation) -> (x : Setoid) -> ExtenderSetoidHomomorphism

  States: The mediating setoid homomorphism in the universal
  property of the free model.

Totality: total
Visibility: public export

FreeUPExists : (pres : Presentation) -> (x : Setoid) -> Extender

  States: The mediating homomorphism in the universal property of
  the free model.

Totality: total
Visibility: public export

FreeUPUnique : (pres : Presentation) -> (x : Setoid) -> Uniqueness

  Uniqueness of the mediating homomorphism in the universal property
  of the free model.

Totality: total
Visibility: public export

FreeIsFree : (pres : Presentation) -> (x : Setoid) -> Freeness (FreeData pres x)

  The free model is indeed free.

Totality: total
Visibility: public export

Free : (pres : Presentation) -> (x : Setoid) -> Free pres x

  Constructs the free model of a presentation over a given setoid.
  The equivalence relation in the resulting setoid might be
  undecidable, even if the original setoid was a decidable setoid
  (or even a decidable set).

Totality: total
Visibility: public export