Frex.Free.Construction.Combinators

Definitions

congruence' : (t : Term (pres .signature) (Either (U a) (Fin n))) -> (cast (QuotientModel pres a)) .VectEquality lhs rhs -> (|-) a (bindTerm t (fromLeft (\i => index i lhs))) (bindTerm t (fromLeft (\i => index i rhs)))

Totality: total
Visibility: export

WithEqualities : (pres : Presentation) -> (a : PresetoidAlgebra (pres .signature)) -> Vect n (U a) -> Vect n (U a) -> Type -> Type

Totality: total
Visibility: public export

withEqualities : (lhs : Vect n (U a)) -> (rhs : Vect n (U a)) -> ((cast (QuotientModel pres a)) .VectEquality lhs rhs -> b) -> WithEqualities pres a lhs rhs b

Totality: total
Visibility: export

congruence : (n : Nat) -> (t : Term (pres .signature) (Either (U a) (Fin n))) -> PI n Hidden (U a) (\lhs => PI n Hidden (U a) (\rhs => WithEqualities pres a lhs rhs ((|-) a (bindTerm t (fromLeft (\i => index i lhs))) (bindTerm t (fromLeft (\i => index i rhs))))))

  A congruence that's much more convenient to use

Totality: total
Visibility: export

byAxiom' : (pres : Presentation) -> (eq : Axiom pres) -> PI ((pres .axiom eq) .support) Visible (U a) (\env => (|-) a (bindTerm ((pres .axiom eq) .lhs) (\i => index i env)) (bindTerm ((pres .axiom eq) .rhs) (\i => index i env)))

  A ByAxiom that's much more convenient to use

Totality: total
Visibility: export

byAxiom : (pres : Presentation) -> (eq : Axiom pres) -> PI ((pres .axiom eq) .support) Hidden (U a) (\env => (|-) a (bindTerm ((pres .axiom eq) .lhs) (\i => index i env)) (bindTerm ((pres .axiom eq) .rhs) (\i => index i env)))

  A ByAxiom that's much more convenient to use

Totality: total
Visibility: export

byLemma' : (lemma : Lemma pres) -> PI ((lemma .equation) .support) Visible (U a) (\env => (|-) a (bindTerm ((lemma .equation) .lhs) (\i => index i env)) (bindTerm ((lemma .equation) .rhs) (\i => index i env)))

  A ByAxiom-like combinator that's much more convenient to use

Totality: total
Visibility: export

byLemma : (lemma : Lemma pres) -> PI ((lemma .equation) .support) Hidden (U a) (\env => (|-) a (bindTerm ((lemma .equation) .lhs) (\i => index i env)) (bindTerm ((lemma .equation) .rhs) (\i => index i env)))

  A ByAxiom-like combinator that's much more convenient to use

Totality: total
Visibility: export