Library HoTT.Classes.theory.ua_third_isomorphism

Require Import
  Basics.Notations
  Colimits.Quotient
  Classes.interfaces.canonical_names
  Classes.theory.ua_quotient_algebra
  Classes.theory.ua_isomorphic
  Classes.theory.ua_first_isomorphism
  Spaces.List.Core.

Import algebra_notations quotient_algebra_notations isomorphic_notations.

Section cong_quotient.
  Context
    `{Univalence}
    {σ : Signature} {A : Algebra σ}
    (Φ : ∀ s, Relation (A s)) `{!IsCongruence A Φ}
    (Ψ : ∀ s, Relation (A s)) `{!IsCongruence A Ψ}
    (subrel : ∀ (s : Sort σ) (x y : A s), Ψ s x y → Φ s x y).

  Definition cong_quotient (_ : ∀ s x y, Ψ s x y → Φ s x y)
    (s : Sort σ) (a b : (A/Ψ) s)
    := ∀ (x y : A s), in_class (Ψ s) a x → in_class (Ψ s) b y → Φ s x y.

  Global Instance equivalence_relation_quotient (s : Sort σ)
    : EquivRel (cong_quotient subrel s).
  Proof.
    constructor.
    - refine (Quotient_ind_hprop (Ψ s) _ _). intros x y z P Q.
      apply subrel.
      by transitivity x.
    - refine (Quotient_ind_hprop (Ψ s) _ _). intro x1.
      refine (Quotient_ind_hprop (Ψ s) _ _). intros x2 C y1 y2 P Q.
      symmetry.
      by apply C.
    - refine (Quotient_ind_hprop (Ψ s) _ _). intro x1.
      refine (Quotient_ind_hprop (Ψ s) _ _). intro x2.
      refine (Quotient_ind_hprop (Ψ s) _ _). intros x3 C D y1 y2 P Q.
      transitivity x2.
      + exact (C y1 x2 P (EquivRel_Reflexive x2)).
      + exact (D x2 y2 (EquivRel_Reflexive x2) Q).
  Defined.

  Lemma for_all_relation_quotient {w : list (Sort σ)} (a b : FamilyProd A w)
    : for_all_2_family_prod (A/Ψ) (A/Ψ) (cong_quotient subrel)
        (map_family_prod (λ s, class_of (Ψ s)) a)
        (map_family_prod (λ s, class_of (Ψ s)) b) →
      for_all_2_family_prod A A Φ a b.
  Proof.
    intro F. induction w; cbn in ×.
    - constructor.
    - destruct a as [x a], b as [y b], F as [Q F].
      split.
      + apply Q; simpl; reflexivity.
      + by apply IHw.
  Qed.

  Global Instance ops_compatible_quotient
    : OpsCompatible (A/Ψ) (cong_quotient subrel).
  Proof.
    intros u.
    refine (quotient_ind_prop_family_prod A Ψ _ _). intro a.
    refine (quotient_ind_prop_family_prod A Ψ _ _). intro b.
    (* It should not be necessary to provide the explicit types: *)
    destruct (compute_op_quotient A Ψ u a
              : ap_operation (u.#(A / Ψ))
                 (map_family_prod (λ s, class_of (Ψ s)) _) = _)^.
    destruct (compute_op_quotient A Ψ u b
              : ap_operation (u.#(A / Ψ))
                 (map_family_prod (λ s, class_of (Ψ s)) _) = _)^.
    intros R x y P Q.
    apply subrel in P.
    apply subrel in Q.
    transitivity (ap_operation u.#A a).
    - by symmetry.
    - transitivity (ap_operation u.#A b); try assumption.
      apply (ops_compatible A Φ u).
      by apply for_all_relation_quotient.
  Defined.

  Global Instance is_congruence_quotient
    : IsCongruence (A/Ψ) (cong_quotient subrel)
    := BuildIsCongruence (A/Ψ) (cong_quotient subrel).

End cong_quotient.

Section third_isomorphism.
  Context
    `{Univalence}
    {σ : Signature} {A : Algebra σ}
    (Φ : ∀ s, Relation (A s)) `{!IsCongruence A Φ}
    (Ψ : ∀ s, Relation (A s)) `{!IsCongruence A Ψ}
    (subrel : ∀ (s : Sort σ) (x y : A s), Ψ s x y → Φ s x y).

  Lemma third_surjecton_well_def (s : Sort σ)
    (x y : A s) (P : Ψ s x y)
    : class_of (Φ s) x = class_of (Φ s) y.
  Proof.
    apply qglue. exact (subrel s x y P).
  Defined.

  Definition def_third_surjection (s : Sort σ) : (A/Ψ) s → (A/Φ) s
    := Quotient_rec (Ψ s) _ (class_of (Φ s)) (third_surjecton_well_def s).

  Lemma oppreserving_third_surjection {w : SymbolType σ} (f : Operation A w)
    : ∀ (α : Operation (A/Φ) w) (Qα : ComputeOpQuotient A Φ f α)
        (β : Operation (A/Ψ) w) (Qβ : ComputeOpQuotient A Ψ f β),
      OpPreserving def_third_surjection β α.
  Proof.
    induction w.
    - refine (Quotient_ind_hprop (Φ t) _ _). intros α Qα.
      refine (Quotient_ind_hprop (Ψ t) _ _). intros β Qβ.
      apply qglue.
      transitivity f.
      + apply subrel. apply (related_quotient_paths (Ψ t)). exact (Qβ tt).
      + apply (related_quotient_paths (Φ t)). symmetry. exact (Qα tt).
    - intros α Qα β Qβ.
      refine (Quotient_ind_hprop (Ψ t) _ _).
      intro x.
      exact (IHw (f x) (α (class_of (Φ t) x)) (λ a, Qα (x,a))
               (β (class_of (Ψ t) x)) (λ a, Qβ (x,a))).
  Defined.

 Global Instance is_homomorphism_third_surjection
    : IsHomomorphism def_third_surjection.
  Proof.
    intro u.
    eapply oppreserving_third_surjection; apply compute_op_quotient.
  Defined.

  Definition hom_third_surjection : Homomorphism (A/Ψ) (A/Φ)
    := BuildHomomorphism def_third_surjection.

  Global Instance surjection_third_surjection (s : Sort σ)
    : IsSurjection (hom_third_surjection s).
  Proof.
    apply BuildIsSurjection.
    refine (Quotient_ind_hprop (Φ s) _ _).
    intro x.
    apply tr.
    by ∃ (class_of (Ψ s) x).
  Qed.

  Local Notation Θ := (cong_quotient Φ Ψ subrel).

  Lemma path_quotient_algebras_third_surjection
    : A/Ψ / cong_ker hom_third_surjection = A/Ψ / Θ.
  Proof.
    apply path_quotient_algebra_iff. intros s x y.
    split; generalize dependent y; generalize dependent x;
           refine (Quotient_ind_hprop (Ψ s) _ _); intro x;
           refine (Quotient_ind_hprop (Ψ s) _ _); intro y.
    - intros K x' y' Cx Cy.
      apply subrel in Cx. apply subrel in Cy.
      apply (related_quotient_paths (Φ s)) in K.
      transitivity x.
      + by symmetry.
      + by transitivity y.
    - intro T.
      apply qglue.
      exact (T x y (EquivRel_Reflexive x) (EquivRel_Reflexive y)).
  Defined.

  Definition hom_third_isomorphism : Homomorphism (A/Ψ/Θ) (A/Φ)
    := transport (λ X, Homomorphism X (A/Φ))
          path_quotient_algebras_third_surjection
          (hom_first_isomorphism_surjection hom_third_surjection).

  Theorem is_isomorphism_third_isomorphism
    : IsIsomorphism hom_third_isomorphism.
  Proof.
    unfold hom_third_isomorphism.
    destruct path_quotient_algebras_third_surjection.
    exact _.
  Qed.

  Global Existing Instance is_isomorphism_third_isomorphism.

  Corollary isomorphic_third_isomorphism : A/Ψ/Θ ≅ A/Φ.
  Proof.
    exact (BuildIsomorphic hom_third_isomorphism).
  Defined.

  Corollary id_third_isomorphism : A/Ψ/Θ = A/Φ.
  Proof.
    exact (id_isomorphic isomorphic_third_isomorphism).
  Defined.
End third_isomorphism.