theory.ua_congruence

Require Import
  Morphisms RelationClasses Relation_Definitions List
  universal_algebra ua_homomorphisms canonical_names ua_subalgebraT util.
Require ua_products.

Require theory.categories.

Local Hint Transparent Equiv : typeclass_instances.

Section contents.
  Context σ `{@Algebra v ve vo}.

  Notation op_type := (op_type (sorts )).
  Notation vv := (ua_products.carrier bool (λ _: bool, v)).

  Let hint := @ua_products.product_algebra bool (λ _, v) _ _ _.


  Let hint' (a: sorts ): Equiv (ua_products.carrier bool (fun _: bool => v) a).

  Context (e: s, relation (v s)).

  Section for_nice_e.

  Context
    (e_e: s, Equivalence (e s))
    (e_proper: s, Proper ((=) ==> (=) ==> iff) (e s)).


  Let Q s x := e s (x true) (x false).
  Let lifted_e := @op_type_equiv (sorts ) v e.
  Let lifted_normal := @op_type_equiv (sorts ) v ve.

  Instance lifted_e_proper o: Proper ((=) ==> (=) ==> iff) (lifted_e o).


  Let eAlgebra := @Algebra v e _.

  Let eSub := @ua_subalgebraT.ClosedSubset vv _ _ Q.

  Lemma eAlgebra_eSub: eAlgebra eSub.

  Lemma eSub_eAlgebra: eSub eAlgebra.

  Lemma back_and_forth: iffT eSub eAlgebra.

  End for_nice_e.


  Class Congruence: Prop :=
    { congruence_proper:> s: sorts , Proper ((=) ==> (=) ==> iff) (e s)
    ; congruence_quotient:> Algebra v (e:=e) }.

End contents.


Lemma quotient_variety
  (et: EquationalTheory) `{InVariety et v}
  (e': s, relation (v s)) `{!Congruence et e'}
  (no_premises: s, et_laws et s entailment_premises _ s nil):
    InVariety et v (e:=e').

Section in_domain.

  Context {A B} {R: Equiv B} (f: A B).

  Definition in_domain: Equiv A := λ x y, f x = f y.
  Global Instance in_domain_equivalence: Equivalence R Equivalence in_domain.

End in_domain.

Section first_iso.


  Context `{Algebra σ A} `{Algebra B} `{!HomoMorphism A B f}.

  Notation := (λ s, in_domain (f s)).

  Lemma square o0 x x' y y':
    Preservation A B f x x'
    Preservation A B f y y'
    op_type_equiv (sorts ) B o0 x' y'
    @op_type_equiv (sorts ) A (λ s: sorts , @in_domain (A s) (B s) (e0 s) (f s)) o0 x y.

  Instance co: Congruence .

  Definition image s (b: B s): Type := sigT (λ a, f s a = b).

  Lemma image_proper: s (x0 x' : B s), x0 = x' iffT (image s x0) (image s x').

  Instance: ClosedSubset image.

  Definition quot_obj: algebras.Object := algebras.object A (algebra_equiv:=).   Definition subobject: algebras.Object := algebras.object (ua_subalgebraT.carrier image).

  Program Definition back: subobject quot_obj := λ _ X, projT1 (projT2 X).


  Program Definition forth: quot_obj subobject :=
    λ a X, existT _ (f a X) (existT _ X (reflexivity _)).


  Theorem first_iso: categories.iso_arrows back forth.

End first_iso.