theory.forget_variety


Require Import
  canonical_names universal_algebra interfaces.functors
  theory.categories categories.varieties categories.algebras.

Section contents.

  Variable et: EquationalTheory.

  Definition forget (v: varieties.Object et) := algebras.object et v.

  Global Instance: Fmap forget := λ _ _, id.

  Global Instance: Functor forget _.

End contents.