Displayed algebra (UniMath#2008)

This PR introduces enhancements to the module on universal algebra.
Along with several minor improvements, we introduce the concept of
_displayed algebra_. This work will be presented at [HOTT-UF
2025](https://hott-uf.github.io/2025/).

---------

Co-authored-by: Calosci Matteo <calomat@libero.it>
Co-authored-by: CalosciMatteo <116155090+CalosciMatteo@users.noreply.github.com>

Author: amato-gianluca

UniMath/Algebra/.package/files

@@ -25,9 +25,14 @@ Modules/Quotient.v
 Modules.v
 Matrix.v
 Universal/HVectors.v
+Universal/HVecRel.v
 Universal/SortedTypes.v
 Universal/Signatures.v
 Universal/Algebras.v
+Universal/Algebras_eq.v
+Universal/SubAlgebras.v
+Universal/DisplayedAlgebras.v
+Universal/Congruences.v
 Universal/Terms.v
 Universal/TermAlgebras.v
 Universal/VTerms.v

UniMath/Algebra/Universal/Algebras.v

@@ -2,6 +2,7 @@
 (** Gianluca Amato,  Marco Maggesi, Cosimo Perini Brogi 2019-2023 *)
 
 Require Import UniMath.Foundations.All.
+Require Import UniMath.MoreFoundations.All.
 
 Require Export UniMath.Algebra.Universal.SortedTypes.
 Require Export UniMath.Algebra.Universal.Signatures.
@@ -103,9 +104,10 @@ Bind Scope hom_scope with hom.
 
 Local Open Scope hom.
 
-Definition hom2fun {σ: signature} {A1 A2: algebra σ} (f: A1 ↷ A2): ∏ s: sorts σ, support A1 s → support A2 s:= pr1 f.
+Definition hom2fun {σ: signature} {A1 A2: algebra σ} (f: A1 ↷ A2)
+  : sfun (support A1) (support A2) := pr1 f.
 
-Coercion hom2fun: hom >-> Funclass.
+Coercion hom2fun: hom >-> sfun.
 
 Definition hom2axiom {σ: signature} {A1 A2: algebra σ} (f: A1 ↷ A2) := pr2 f.
 
@@ -234,5 +236,121 @@ Definition make_hSetalgebra {σ : signature} {A: algebra σ} (setproperty: has_s
 Definition hSetalgebra_to_algebra {σ : signature} (A: hSetalgebra σ): algebra σ
 := ((λ s : sorts σ, pr1 (pr1 A s)),, pr2 A).
 
+Coercion hSetalgebra_to_algebra : hSetalgebra >-> algebra.
+
 Definition has_supportsets_hSetalgebra {σ : signature} (A: hSetalgebra σ): has_supportsets (hSetalgebra_to_algebra A)
 := λ s: sorts σ, setproperty (pr1 A s).
+
+Lemma transportf_fun_op {σ : signature} {A B : sUU (sorts σ)}
+  (p : A = B)
+  (nm : names σ) (f : (A⋆ (arity nm) → A (sort nm)))
+  : transportf (λ x : sUU (sorts σ), x⋆ (arity nm) → x (sort nm)) p f
+  = (transportf (λ x : sUU (sorts σ), x (sort nm)) p) ∘ f ∘ (transportb (λ x : sUU (sorts σ), x⋆ (arity nm)) p).
+Proof.
+  induction p.
+  apply idpath.
+Defined.
+
+Lemma transportf_fun_op2 {σ : signature} {A : sUU (sorts σ)}
+  (D D' : ∏ s : sorts σ, A s → UU)
+  (p : D = D')
+  (nm : names σ)
+  (base_xs : hvec (vec_map A (arity nm)))
+  (opsAnm : (A⋆ (arity nm) → A (sort nm)))
+  (f : hvec (h1lower (h1map D base_xs)) → D (sort nm) (opsAnm base_xs))
+  : transportf
+    (λ x : ∏ s : sorts σ, A s → UU,
+      hvec (h1lower (h1map x base_xs)) → x (sort nm) (opsAnm base_xs))
+    p f
+  = (transportf
+    (λ D0 : ∏ s : sorts σ, A s → UU , D0 (sort nm) (opsAnm base_xs)) p) ∘ f ∘
+    (transportb (λ D0, hvec (h1lower (h1map D0 base_xs))) p).
+  Proof.
+    induction p.
+    apply idpath.
+  Defined.
+
+(*The proof is the same of [transportf_funextsec], but this statement is not captured by it*)
+  Lemma transportf_funextsec_op
+    {S : UU} {A : sUU S}
+    {l : list S}
+    (D D' : ∏ s : S, A s → UU)
+    (H : ∏ (s: S), D s = D' s)
+    (s : S)
+    (a : A s)
+    (d : D s a)
+
+  : transportf (λ D0 : ∏ s : S, A s → UU, D0 s a) (funextsec _ _ _ H) d =
+  transportf (λ Ds0 : A s -> UU, Ds0 a) (H s) d.
+  Proof.
+    use (toforallpaths_induction' S (λ s, A s → UU) D D'
+      (λ H',  transportf
+        (λ D0 : ∏ s : S, A s → UU, D0 s a)
+        (funextsec (λ s : S, A s → UU) D D' H') d
+        = transportf
+        (λ Ds0 : A s → UU, Ds0 a)
+        (H' s) d ) _ H).
+    intro e.
+    clear H.
+    simpl.
+
+    set (XR := homotinvweqweq (weqtoforallpaths _ D D') e).
+    set (H := funextsec (λ s, A s → UU) D D' (toforallpaths _ D D' e)).
+    set (P' := (λ D0 : ∏ s : S, A s → UU, D0 s a)).
+    use pathscomp0.
+    - exact (transportf P' e d).
+    - use (transportf_paths _ XR).
+    - induction e. apply idpath.
+  Defined.
+
+  Lemma transportb_funextsec_op
+    {S : UU} {A : sUU S}
+    {l : list S}
+    (D D' : ∏ s : S, A s → UU)
+    (H : ∏ (s: S), D s = D' s)
+    (s : S)
+    (a : A s)
+    (d : D' s a)
+
+  : transportb (λ D0 : ∏ s : S, A s → UU, D0 s a) (funextsec _ _ _ H) d =
+  transportb (λ Ds0 : A s -> UU, Ds0 a) (H s) d.
+  Proof.
+    use (toforallpaths_induction' S (λ s, A s → UU) D D'
+      (λ H',  transportb
+        (λ D0 : ∏ s : S, A s → UU, D0 s a)
+        (funextsec (λ s : S, A s → UU) D D' H') d
+        = transportb
+        (λ Ds0 : A s → UU, Ds0 a)
+        (H' s) d ) _ H).
+    intro e.
+    clear H.
+    simpl.
+
+    set (XR := homotinvweqweq (weqtoforallpaths _ D D') e).
+    set (H := funextsec (λ s, A s → UU) D D' (toforallpaths _ D D' e)).
+    set (P' := (λ D0 : ∏ s : S, A s → UU, D0 s a)).
+    use pathscomp0.
+    - exact (transportb P' e d).
+    - use (transportf_paths _ _).
+      use invrot.
+      eapply pathscomp0.
+      { use pathsinv0inv0. }
+      exact XR.
+    - induction e. apply idpath.
+  Defined.
+
+  Lemma transportf_funextsec_op'
+  {σ : signature} {A : algebra σ}
+  (D D' : ∏ s : sorts σ, A s → UU)
+  (H : ∏ (s: sorts σ), D s = D' s)
+  (nm : names σ)
+  (base_xs : hvec (vec_map A (arity nm)))
+  (opsAnm : (A⋆ (arity nm) → A (sort nm)))
+  (f : D (sort nm) (ops A nm base_xs))
+
+  : transportf (λ D0 : ∏ s : sorts σ, A s → UU, D0 (sort nm) (ops A nm base_xs)) (funextsec _ _ _ H) f =
+  transportf (λ Ds0 : A (sort nm) -> UU, Ds0 (ops A nm base_xs)) (H (sort nm)) f.
+  Proof.
+    use transportf_funextsec_op.
+    exact (arity nm).
+  Defined.

UniMath/Algebra/Universal/Algebras_eq.v

@@ -0,0 +1,73 @@
+Require Import UniMath.Foundations.All.
+Require Import UniMath.MoreFoundations.All.
+
+Require Import UniMath.Algebra.Universal.Algebras.
+
+Local Open Scope sorted.
+Local Open Scope hom_scope.
+
+Theorem make_algebra_support_eq {σ : signature} {A B : algebra σ}
+  (h : A s→ B) (isweq : ∏ s:(sorts σ), isweq (h s))
+  : support A = support B.
+Proof.
+  use funextsec.
+  intro s.
+  use weqtopaths.
+  exact (h s ,, isweq s).
+Defined.
+
+Theorem make_algebra_eq {σ : signature} {A B : algebra σ}
+  (h : A ↷ B) (isweq : ∏ s:(sorts σ), isweq (h s))
+  : A = B.
+Proof.
+  use total2_paths2_f.
+  - use (make_algebra_support_eq h isweq).
+  - eapply pathscomp0.
+    { use transportf_sec_constant. }
+    use funextsec.
+    intro nm.
+    eapply pathscomp0.
+    { use transportf_fun_op. }
+    use funextsec.
+    intro xs.
+    simpl.
+    eapply pathscomp0.
+    { use (transportf_funextfun (λ arg, arg) _ _ _ (sort nm)). }
+    change (λ x0 : UU, x0) with (idfun UU).
+    simpl.
+    change (λ x0 : UU, x0) with (idfun UU).
+    eapply pathscomp0.
+    { use (maponpaths (λ arg, arg _) (weqpath_transport _)). }
+    cbn.
+    eapply pathscomp0.
+    { eapply (maponpaths (h (sort nm))).
+      eapply (maponpaths (ops A nm)).
+      use transportb_funextfun_hvec. }
+    simpl.
+    eapply pathscomp0.
+    { use (pr2 h). }
+    use maponpaths.
+    unfold starfun.
+    eapply pathscomp0.
+    { use h1map_compose. }
+    simpl.
+    eapply pathscomp0.
+    2 :{ use h1map_idfun. }
+    use (maponpaths (λ arg, h1map arg xs)).
+    use funextsec.
+    intro s.
+    simpl.
+    use funextsec.
+    intro b.
+    simpl.
+    use (pathsweq1' (h s,, isweq s)).
+    use (maponpaths (λ arg, arg b)).
+    use weqpath_transportb'.
+Defined.
+
+Theorem support_make_algebra_eq {σ : signature} {A B : algebra σ}
+  (h : A ↷ B) (isweq : ∏ s:(sorts σ), isweq (h s))
+  : maponpaths support (make_algebra_eq h isweq) = make_algebra_support_eq h isweq.
+Proof.
+  use total2_paths2_comp1.
+Defined.

UniMath/Algebra/Universal/Congruences.v

@@ -0,0 +1,84 @@
+Require Import UniMath.Foundations.All.
+Require Import UniMath.MoreFoundations.Notations.
+
+Require Import UniMath.Algebra.Universal.Algebras.
+Require Import UniMath.Algebra.Universal.HVecRel.
+
+Local Open Scope sorted.
+
+Definition shrel {S : UU} (A : sUU S) : UU
+  := ∏ (s:S), hrel (A s).
+
+Definition extensionallift
+  {S : UU} {A : sUU S} (R : shrel A)
+  (P : ∏ (s:S) (R:hrel (A s)), UU) : UU
+  := ∏ (s:S), P s (R s).
+
+Definition siseqrel {S : UU} {A : sUU S} (R : shrel A)
+  := extensionallift R (λ _ R, iseqrel R).
+
+(*Generalization of [[iscomprelfun]]*)
+Definition iscomprelfunrel {X Y : UU}
+  (RX : hrel X) (RY : hrel Y) (f : X -> Y)
+  : UU
+  := ∏ x x' : X, RX x x' -> RY (f x) (f x').
+
+Definition shrelList
+  {σ : signature} {A : algebra σ} (R : shrel A) (l : list (sorts σ))
+  : hrel (A⋆ l).
+Proof.
+  unfold star.
+  use hrelhvec.
+  change (hvec (((vec_map hrel) ∘ (vec_map (support A))) l)).
+  use (transportf hvec (vec_map_comp (support A) (hrel) l)).
+  use h01map.
+  exact R.
+Defined.
+
+Definition iscompatible {σ : signature}
+  (A : algebra σ) (R : shrel A)
+ := ∏ nm: names σ, iscomprelfunrel (shrelList R (arity nm)) (R (sort nm)) (ops A nm).
+
+Definition iscong {σ : signature}
+  (A : algebra σ) (R : shrel A)
+  := siseqrel R × iscompatible A R.
+
+Definition congruence {σ : signature} (A : algebra σ)
+  := ∑ (R : shrel A), iscong A R.
+
+Definition eqrelofcong {σ : signature} {A : algebra σ} (R : congruence A) (s: sorts σ)
+  : eqrel (support A s)
+  := (pr1 R) s ,, (pr12 R) s.
+
+Coercion eqrelofcong : congruence >-> Funclass.
+
+Definition quotalgebra {σ : signature} (A : algebra σ) (R : congruence A)
+  : algebra σ.
+Proof.
+Proof.
+  use make_algebra.
+  - intro s.
+    exact (setquot (eqrelofcong R s)).
+  - simpl.
+    intros nm xs.
+    use (setquotuniv _ (setquot (eqrelofcong R (sort nm)),,_)).
+    + exact (A⋆ (arity nm)).
+    + use shrelList.
+      apply R.
+    + use isasetsetquot.
+    + apply (funcomp (ops A nm) (setquotpr ((eqrelofcong R) (sort nm)))).
+    + simpl.
+      intros a1s b1s rel_ab.
+      simpl.
+      use (iscompsetquotpr (eqrelofcong R (sort nm))).
+      use (pr2 (pr2 R) nm _ _ rel_ab). (*TODO: name pr2 and make opportune coercions*)
+    + simpl.
+      use hvectosetquot.
+      unfold star in xs.
+      refine (eqweqmap (maponpaths hvec _) xs).
+      eapply pathscomp0. { use h01maph1lower.  }
+      eapply pathscomp0. { use h1lower_vec_map_comp. exact (support A). }
+      use maponpaths.
+      use pathsinv0.
+      use h1h01map_transport_vec_map_comp.
+Defined.