varieties.setoids

Require
  theory.rings categories.varieties.
Require Import
  abstract_algebra universal_algebra ua_homomorphisms.

Definition op := False.

Definition sig: Signature := Build_Signature unit op (False_rect _).

Definition Laws: EqEntailment sig Prop := λ _, False.

Definition theory: EquationalTheory := Build_EquationalTheory sig Laws.


Section from_instance.
  Context A `{Setoid A}.

  Notation carriers := (λ _, A).

  Instance: AlgebraOps sig carriers := λ o, False_rect _ o.

  Instance: Algebra sig carriers.

  Instance: InVariety theory carriers.

  Definition object: varieties.Object theory := varieties.object theory (λ _, A).

End from_instance.


Section from_variety.

  Context `{InVariety theory A}.

  Instance: Setoid (A tt) := {}.

End from_variety.

Lemma mor_from_sr_to_alg `{InVariety theory A} `{InVariety theory B}
  (f: u, A u B u) `{!Setoid_Morphism (f tt)}: HomoMorphism sig A B f.

Instance decode_variety_and_ops `{InVariety theory A}: Setoid (A tt) := {}.