Library HoTT.Classes.theory.ua_second_isomorphism

Require Import
  Basics.Notations
  HSet
  Colimits.Quotient
  Classes.interfaces.canonical_names
  Classes.theory.ua_isomorphic
  Classes.theory.ua_subalgebra
  Classes.theory.ua_quotient_algebra.

Import
  algebra_notations
  quotient_algebra_notations
  subalgebra_notations
  isomorphic_notations.

Local Notation i := (hom_inc_subalgebra _ _).

Section cong_trace.
  Context
    {σ : Signature} {A : Algebra σ}
    (P : ∀ s, A s → Type) `{!IsSubalgebraPredicate A P}
    (Φ : ∀ s, Relation (A s)) `{!IsCongruence A Φ}.

  Definition cong_trace (s : Sort σ) (x : (A&&P) s) (y : (A&&P) s)
    := Φ s (i s x) (i s y).

  Global Instance equiv_rel_trace_congruence (s : Sort σ)
    : EquivRel (cong_trace s).
  Proof.
    unfold cong_trace.
    constructor.
    - intros [y Y]. reflexivity.
    - intros [y1 Y1] [y2 Y2] S. by symmetry.
    - intros [y1 Y1] [y2 Y2] [y3 Y3] S T. by transitivity y2.
  Qed.

  Lemma for_all_2_family_prod_trace_congruence {w : SymbolType σ}
    (a b : FamilyProd (A&&P) (dom_symboltype w))
    (R : for_all_2_family_prod (A&&P) (A&&P) cong_trace a b)
    : for_all_2_family_prod A A Φ
        (map_family_prod i a) (map_family_prod i b).
  Proof with try assumption.
    induction w...
    destruct a as [x a], b as [y b], R as [C R].
    split...
    apply IHw...
  Qed.

  Global Instance ops_compatible_trace_trace
    : OpsCompatible (A&&P) cong_trace.
  Proof.
    intros u a b R.
    refine (transport (λ X, Φ _ X _)
              (path_homomorphism_ap_operation i u a)^ _).
    refine (transport (λ X, Φ _ _ X)
              (path_homomorphism_ap_operation i u b)^ _).
    apply (ops_compatible_cong A Φ).
    exact (for_all_2_family_prod_trace_congruence a b R).
  Qed.

  Global Instance is_congruence_trace : IsCongruence (A&&P) cong_trace.
  Proof.
    apply (@BuildIsCongruence _ (A&&P) cong_trace);
      [intros; apply (is_mere_relation_cong A Φ) | exact _ ..].
  Qed.
End cong_trace.

Section is_subalgebra_class.
  Context `{Univalence}
    {σ : Signature} {A : Algebra σ}
    (P : ∀ s, A s → Type) `{!IsSubalgebraPredicate A P}
    (Φ : ∀ s, Relation (A s)) `{!IsCongruence A Φ}.

  Definition is_subalgebra_class (s : Sort σ) (x : (A/Φ) s) : HProp
    := hexists (λ (y : (A&&P) s), in_class (Φ s) x (i s y)).

  Lemma op_closed_subalgebra_is_subalgebra_class {w : SymbolType σ}
    (γ : Operation (A/Φ) w)
    (α : Operation A w)
    (Q : ComputeOpQuotient A Φ α γ)
    (C : ClosedUnderOp A P α)
    : ClosedUnderOp (A/Φ) is_subalgebra_class γ.
  Proof.
    induction w.
    - specialize (Q tt). apply tr.
      ∃ (α; C).
      cbn in Q. destruct Q^.
      exact (EquivRel_Reflexive α).
    - refine (Quotient_ind_hprop (Φ t) _ _). intro x.
      refine (Trunc_rec _).
      intros [y R].
      apply (IHw (γ (class_of (Φ t) x)) (α (i t y))).
      + intro a.
        destruct (qglue R)^.
        apply (Q (i t y,a)).
      + apply C. exact y.2.
  Qed.

  Definition is_closed_under_ops_is_subalgebra_class
    : IsClosedUnderOps (A/Φ) is_subalgebra_class.
  Proof.
    intro u.
    eapply op_closed_subalgebra_is_subalgebra_class.
    - apply compute_op_quotient.
    - apply is_closed_under_ops_subalgebra_predicate. exact _.
  Qed.

  Global Instance is_subalgebra_predicate_is_subalgebra_class
    : IsSubalgebraPredicate (A/Φ) is_subalgebra_class.
  Proof.
    apply BuildIsSubalgebraPredicate.
    apply is_closed_under_ops_is_subalgebra_class.
  Qed.
End is_subalgebra_class.

      (A&&P) / (cong_trace P Φ) ≅ (A/Φ) && (is_subalgebra_class P Φ).

(* There is an alternative proof using the first isomorphism theorem,
   but the direct proof below seems simpler in HoTT. *)

Section second_isomorphism.
  Context `{Univalence}
    {σ : Signature} (A : Algebra σ)
    (P : ∀ s, A s → Type) `{!IsSubalgebraPredicate A P}
    (Φ : ∀ s, Relation (A s)) `{!IsCongruence A Φ}.

  Local Notation Ψ := (cong_trace P Φ).

  Local Notation Q := (is_subalgebra_class P Φ).

  Definition def_second_isomorphism (s : Sort σ)
    : ((A&&P) / Ψ) s → ((A/Φ) && Q) s
    := Quotient_rec (Ψ s) _
        (λ (x : (A&&P) s),
         (class_of (Φ s) (i s x); tr (x; EquivRel_Reflexive x)))
        (λ (x y : (A&&P) s) (T : Ψ s x y),
         path_sigma_hprop (class_of (Φ s) (i s x); _)
           (class_of (Φ s) (i s y); _) (@qglue _ (Φ s) _ _ T)).

  Lemma oppreserving_second_isomorphism {w : SymbolType σ}
    (α : Operation A w) (γ : Operation (A/Φ) w)
    (ζ : Operation ((A&&P) / Ψ) w) (CA : ClosedUnderOp (A/Φ) Q γ)
    (CB : ClosedUnderOp A P α) (QA : ComputeOpQuotient A Φ α γ)
    (QB : ComputeOpQuotient (A&&P) Ψ (op_subalgebra A P α CB) ζ)
    : OpPreserving def_second_isomorphism ζ (op_subalgebra (A/Φ) Q γ CA).
  Proof.
    unfold ComputeOpQuotient in ×.
    induction w; cbn in ×.
    - apply path_sigma_hprop.
      cbn. destruct (QB tt)^, (QA tt)^.
      by apply qglue.
    - refine (Quotient_ind_hprop (Ψ t) _ _). intro x.
      apply (IHw (α (i t x)) (γ (class_of (Φ t) (i t x)))
              (ζ (class_of (Ψ t) x))
              (CA (class_of (Φ t) (i t x)) (tr (x; _)))
              (CB (i t x) x.2)).
      + intro a. exact (QA (i t x, a)).
      + intro a. exact (QB (x, a)).
  Defined.

  Global Instance is_homomorphism_second_isomorphism
    : IsHomomorphism def_second_isomorphism.
  Proof.
    intro u.
    eapply oppreserving_second_isomorphism.
    - apply (compute_op_quotient A).
    - apply (compute_op_quotient (A&&P)).
  Defined.

  Definition hom_second_isomorphism
    : Homomorphism ((A&&P) / Ψ) ((A/Φ) && Q)
    := BuildHomomorphism def_second_isomorphism.

  Global Instance embedding_second_isomorphism (s : Sort σ)
    : IsEmbedding (hom_second_isomorphism s).
  Proof.
    apply isembedding_isinj_hset.
    refine (Quotient_ind_hprop (Ψ s) _ _). intro x.
    refine (Quotient_ind_hprop (Ψ s) _ _). intros y p.
    apply qglue.
    exact (related_quotient_paths (Φ s) (i s x) (i s y) (p..1)).
  Qed.

  Global Instance surjection_second_isomorphism (s : Sort σ)
    : IsSurjection (hom_second_isomorphism s).
  Proof.
    apply BuildIsSurjection.
    intros [y S].
    generalize dependent S.
    generalize dependent y.
    refine (Quotient_ind_hprop (Φ s) _ _). intros y S.
    refine (Trunc_rec _ S). intros [y' S']. apply tr.
    ∃ (class_of _ y').
    apply path_sigma_hprop.
    by apply qglue.
  Qed.

  Theorem is_isomorphism_second_isomorphism
    : IsIsomorphism hom_second_isomorphism.
  Proof.
    intro s. apply isequiv_surj_emb; exact _.
  Qed.

  Global Existing Instance is_isomorphism_second_isomorphism.

  Theorem isomorphic_second_isomorphism : (A&&P) / Ψ ≅ (A/Φ) && Q.
  Proof.
    exact (BuildIsomorphic def_second_isomorphism).
  Defined.

  Corollary id_second_isomorphism : (A&&P) / Ψ = (A/Φ) && Q.
  Proof.
    exact (id_isomorphic isomorphic_second_isomorphism).
  Defined.
End second_isomorphism.