diff --git a/_CoqProject b/_CoqProject
index 5e726ebd9df..2e15e489d32 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -354,6 +354,8 @@ theories/Spectra/Coinductive.v
 theories/Algebra/Universal/Algebra.v
 theories/Algebra/Universal/Homomorphism.v
 theories/Algebra/Universal/Operation.v
+theories/Algebra/Universal/Congruence.v
+theories/Algebra/Universal/TermAlgebra.v
 
 #
 #   Algebra
diff --git a/theories/Algebra/Universal/Algebra.v b/theories/Algebra/Universal/Algebra.v
index c2f933720c7..1c98927b620 100644
--- a/theories/Algebra/Universal/Algebra.v
+++ b/theories/Algebra/Universal/Algebra.v
@@ -95,6 +95,8 @@ Global Existing Instance hset_algebra.
 
 Global Coercion carriers : Algebra >-> Funclass.
 
+Bind Scope Algebra_scope with Algebra.
+
 Definition SigAlgebra (σ : Signature) : Type
   := {c : Carriers σ
         | { _ : forall (u : Symbol σ), Operation c (σ u)
@@ -158,8 +160,7 @@ Defined.
 Arguments path_path_algebra {_} {σ} {A B}%Algebra_scope (p q r)%path_scope.
 
 Module notations_algebra.
-  (** Conflicts with inverse notation so cannot be reserved *)
-  Global Notation "u ^^ A" := (operations A u)
-                              (at level 6, no associativity)
-                              : Algebra_scope.
+
+  Global Notation "u .# A" := (operations A u) : Algebra_scope.
+
 End notations_algebra.
diff --git a/theories/Algebra/Universal/Congruence.v b/theories/Algebra/Universal/Congruence.v
new file mode 100644
index 00000000000..5358cfa98b6
--- /dev/null
+++ b/theories/Algebra/Universal/Congruence.v
@@ -0,0 +1,91 @@
+(** This file implements algebra congruence relation. It serves as a
+    universal algebra generalization of normal subgroup, ring ideal, etc.
+
+    Congruence is used to construct quotients, in similarity with how
+    normal subgroup and ring ideal is used to construct quotients. *)
+
+Require Export HoTT.Algebra.Universal.Algebra.
+
+Require Import
+  HoTT.Basics
+  HoTT.Types
+  HoTT.HProp
+  HoTT.Classes.interfaces.canonical_names
+  HoTT.Algebra.Universal.Homomorphism.
+
+Unset Elimination Schemes.
+
+Import notations_algebra.
+
+Section congruence.
+  Context {σ : Signature} (A : Algebra σ) (Φ : forall s, Relation (A s)).
+
+(** A finitary operation [f : A s1 * A s2 * ... * A sn -> A t]
+    satisfies [OpCompatible f] iff
+
+    <<
+      Φ s1 x1 y1 * Φ s2 x2 y2 * ... * Φ sn xn yn
+    >>
+
+    implies
+
+    <<
+      Φ t (f (x1, x2, ..., xn)) (f (y1, y2, ..., yn)).
+    >>
+
+    The below definition generalizes this to infinitary operations.
+*)
+
+  Definition OpCompatible {w : SymbolType σ} (f : Operation A w) : Type
+    := forall (a b : DomOperation A w),
+       (forall i : Arity w, Φ (sorts_dom w i) (a i) (b i)) ->
+       Φ (sort_cod w) (f a) (f b).
+
+  Class OpsCompatible : Type
+    := ops_compatible : forall (u : Symbol σ), OpCompatible u.#A.
+
+  Global Instance trunc_ops_compatible `{Funext} {n : trunc_index}
+    `{!forall s x y, IsTrunc n (Φ s x y)}
+    : IsTrunc n OpsCompatible.
+  Proof.
+    apply trunc_forall.
+  Defined.
+
+  (** A family of relations [Φ] is a congruence iff it is a family of
+      mere equivalence relations and [OpsCompatible A Φ] holds. *)
+
+  Class IsCongruence : Type := Build_IsCongruence
+   { is_mere_relation_cong : forall (s : Sort σ), is_mere_relation (A s) (Φ s)
+   ; equiv_rel_cong : forall (s : Sort σ), EquivRel (Φ s)
+   ; ops_compatible_cong : OpsCompatible }.
+
+  Global Arguments Build_IsCongruence {is_mere_relation_cong}
+                                      {equiv_rel_cong}
+                                      {ops_compatible_cong}.
+
+  Global Existing Instance is_mere_relation_cong.
+
+  Global Existing Instance equiv_rel_cong.
+
+  Global Existing Instance ops_compatible_cong.
+
+  Global Instance hprop_is_congruence `{Funext} : IsHProp IsCongruence.
+  Proof.
+    apply (equiv_hprop_allpath _)^-1.
+    intros [C1 C2 C3] [D1 D2 D3].
+    by destruct (path_ishprop C1 D1),
+                (path_ishprop C2 D2),
+                (path_ishprop C3 D3).
+  Defined.
+
+End congruence.
+
+(** A homomorphism [f : forall s, A s -> B s] is compatible
+    with a congruence [Φ] iff [Φ s x y] implies [f s x = f s y]. *)
+
+Definition HomCompatible {σ : Signature} {A B : Algebra σ}
+  (Φ : forall s, Relation (A s)) `{!IsCongruence A Φ}
+  (f : forall s, A s -> B s) `{!IsHomomorphism f}
+  : Type
+  := forall s (x y : A s), Φ s x y -> f s x = f s y.
+
diff --git a/theories/Algebra/Universal/Homomorphism.v b/theories/Algebra/Universal/Homomorphism.v
index c6fc7ff5d64..4db3b015a80 100644
--- a/theories/Algebra/Universal/Homomorphism.v
+++ b/theories/Algebra/Universal/Homomorphism.v
@@ -28,7 +28,7 @@ Section is_homomorphism.
   Qed.
 
   Class IsHomomorphism : Type
-    := oppreserving_hom : forall (u : Symbol σ), OpPreserving u^^A u^^B.
+    := oppreserving_hom : forall (u : Symbol σ), OpPreserving u.#A u.#B.
 
   Global Instance hprop_is_homomorphism `{Funext}
     : IsHProp IsHomomorphism.
diff --git a/theories/Algebra/Universal/TermAlgebra.v b/theories/Algebra/Universal/TermAlgebra.v
new file mode 100644
index 00000000000..7e230475ae2
--- /dev/null
+++ b/theories/Algebra/Universal/TermAlgebra.v
@@ -0,0 +1,414 @@
+(** This file defines the term algebra [TermAlgebra], also
+    referred to as the absolutely free algebra.
+
+    We show that term algebra forms an adjoint functor from
+    the category of hset carriers
+
+    <<
+      {C : Carrier σ | forall s, IsHSet (C s)}
+    >>
+
+    to the category of algebras (without equations) [Algebra σ],
+    where [Carriers σ] is notation for [Sort σ -> Type].
+    See [ump_term_algebra].
+
+    There is a similar construction for algebras with equations,
+    the free algebra [FreeAlgebra]. The free algebra is defined in
+    another file. *)
+
+Require Export HoTT.Algebra.Universal.Algebra.
+
+Require Import
+  HoTT.Types
+  HoTT.HProp
+  HoTT.HSet
+  HoTT.Classes.interfaces.canonical_names
+  HoTT.Algebra.Universal.Homomorphism
+  HoTT.Algebra.Universal.Congruence.
+
+Unset Elimination Schemes.
+
+Import notations_algebra.
+
+(** The term algebra carriers are generated by [C : Carriers σ],
+    with an element for each element of [C s], and an operation for
+    each operation symbol [u : Symbol σ]. *)
+
+Inductive CarriersTermAlgebra {σ} (C : Carriers σ) : Carriers σ :=
+  | var_term_algebra : forall s, C s -> CarriersTermAlgebra C s
+  | ops_term_algebra : forall (u : Symbol σ),
+      DomOperation (CarriersTermAlgebra C) (σ u) ->
+      CarriersTermAlgebra C (sort_cod (σ u)).
+
+Scheme CarriersTermAlgebra_ind := Elimination for CarriersTermAlgebra Sort Type.
+Arguments CarriersTermAlgebra_ind {σ}.
+
+Definition CarriersTermAlgebra_rect {σ} := @CarriersTermAlgebra_ind σ.
+
+Definition CarriersTermAlgebra_rec {σ : Signature} (C : Carriers σ)
+  (P : Sort σ -> Type) (vs : forall (s : Sort σ), C s -> P s)
+  (os : forall (u : Symbol σ) (c : DomOperation (CarriersTermAlgebra C) (σ u)),
+        (forall i : Arity (σ u), P (sorts_dom (σ u) i)) -> P (sort_cod (σ u)))
+  (s : Sort σ) (T : CarriersTermAlgebra C s)
+  : P s
+  := CarriersTermAlgebra_ind C (fun s _ => P s) vs os s T.
+
+(** A family of relations [R : forall s, Relation (C s)] can be
+    extended to a family of relations on the term algebra carriers,
+
+    <<
+      forall s, Relation (CarriersTermAlgebra C s)
+    >>
+
+    See [ExtendDRelTermAlgebra] and [ExtendRelTermAlgebra] below. *)
+
+Fixpoint ExtendDRelTermAlgebra {σ : Signature} {C : Carriers σ}
+  (R : forall s, Relation (C s)) {s1 s2 : Sort σ}
+  (S : CarriersTermAlgebra C s1) (T : CarriersTermAlgebra C s2)
+  : Type
+  := match S, T with
+     | var_term_algebra s1 x, var_term_algebra s2 y =>
+        {p : s1 = s2 | R s2 (p # x) y}
+     | ops_term_algebra u1 a, ops_term_algebra u2 b =>
+        { p : u1 = u2 |
+          forall i : Arity (σ u1),
+          ExtendDRelTermAlgebra
+            R (a i) (b (transport (fun v => Arity (σ v)) p i))}
+     | _, _ => Empty
+     end.
+
+Definition ExtendRelTermAlgebra {σ : Signature} {C : Carriers σ}
+  (R : forall s, Relation (C s)) {s : Sort σ}
+  : CarriersTermAlgebra C s -> CarriersTermAlgebra C s -> Type
+  := ExtendDRelTermAlgebra R.
+
+(** The next section shows, in particular, the following:
+    If [R : forall s, Relation (C s)] is a family of mere
+    equivalence relations, then [@ExtendRelTermAlgebra σ C R] is
+    a family of mere equivalence eqlations. *)
+
+Section extend_rel_term_algebra.
+  Context `{Funext} {σ : Signature} {C : Carriers σ}
+    (R : forall s, Relation (C s))
+    `{!forall s, is_mere_relation (C s) (R s)}.
+
+  Global Instance hprop_extend_drel_term_algebra {s1 s2 : Sort σ}
+    (S : CarriersTermAlgebra C s1) (T : CarriersTermAlgebra C s2)
+    : IsHProp (ExtendDRelTermAlgebra R S T).
+  Proof.
+    generalize dependent s2.
+    induction S; intros s2 T; destruct T; exact _.
+  Qed.
+
+  Global Instance reflexive_extend_rel_term_algebra
+    `{!forall s, Reflexive (R s)} {s : Sort σ}
+    : Reflexive (@ExtendRelTermAlgebra σ C R s).
+  Proof.
+    intro S. induction S as [| u c h].
+    - by exists idpath.
+    - exists idpath. intro i. apply h.
+  Qed.
+
+  Lemma symmetric_extend_drel_term_algebra
+    `{!forall s, Symmetric (R s)} {s1 s2 : Sort σ}
+    (S : CarriersTermAlgebra C s1) (T : CarriersTermAlgebra C s2)
+    (h : ExtendDRelTermAlgebra R S T)
+    : ExtendDRelTermAlgebra R T S.
+  Proof.
+    generalize dependent s2.
+    induction S as [| u c h]; intros s2 [] p.
+    - destruct p as [p1 p2].
+      induction p1. exists idpath. by symmetry.
+    - elim p.
+    - elim p.
+    - destruct p as [p f].
+      induction p. exists idpath. intro i. apply h. apply f.
+  Qed.
+
+  Global Instance symmetric_extend_rel_term_algebra
+    `{!forall s, Symmetric (R s)} {s : Sort σ}
+    : Symmetric (@ExtendRelTermAlgebra σ C R s).
+  Proof.
+    intros S T. apply symmetric_extend_drel_term_algebra.
+  Defined.
+
+  Lemma transitive_extend_drel_term_algebra
+    `{!forall s, Transitive (R s)} {s1 s2 s3 : Sort σ}
+    (S : CarriersTermAlgebra C s1)
+    (T : CarriersTermAlgebra C s2)
+    (U : CarriersTermAlgebra C s3)
+    (h1 : ExtendDRelTermAlgebra R S T)
+    (h2 : ExtendDRelTermAlgebra R T U)
+    : ExtendDRelTermAlgebra R S U.
+  Proof.
+    generalize dependent s3.
+    generalize dependent s2.
+    induction S as [| u c h];
+      intros s2 [? d | ? d] h2 s3 [] h3;
+      destruct h2 as [p2 P2], h3 as [p3 P3] || by (elim h2 || elim h3).
+    - exists (p2 @ p3).
+      rewrite transport_pp.
+      induction p2, p3.
+      by transitivity d.
+    - exists (p2 @ p3).
+      intro i.
+      induction p2.
+      apply (h i _ (d i)).
+      + apply P2.
+      + rewrite concat_1p. apply P3.
+  Qed.
+
+  Global Instance transitive_extend_rel_term_algebra
+    `{!forall s, Transitive (R s)} {s : Sort σ}
+    : Transitive (@ExtendRelTermAlgebra σ C R s).
+  Proof.
+    intros S T U. apply transitive_extend_drel_term_algebra.
+  Defined.
+
+  Global Instance equivrel_extend_rel_term_algebra
+    `{!forall s, EquivRel (R s)} (s : Sort σ)
+    : EquivRel (@ExtendRelTermAlgebra σ C R s).
+  Proof.
+    constructor; exact _.
+  Qed.
+
+End extend_rel_term_algebra.
+
+(** By using path (propositional equality) as equivalence relation
+    for [ExtendRelTermAlgebra], we obtain an equivalent notion
+    of equality of term algebra carriers,
+    [equiv_path_extend_path_term_algebra]. The reason for introducing
+    [ExtendRelTermAlgebra] is to have a notion of equality which
+    works well together with induction on term algebras. *)
+
+Section extend_path_term_algebra.
+  Context `{Funext} {σ} {C : Carriers σ} `{!forall s, IsHSet (C s)}.
+
+  Definition ExtendPathTermAlgebra {s : Sort σ}
+    (S : CarriersTermAlgebra C s) (T : CarriersTermAlgebra C s)
+    : Type
+    := ExtendRelTermAlgebra (fun s => paths) S T.
+
+  Global Instance reflexive_extend_path_term_algebra
+    : forall s : Sort σ, Reflexive (@ExtendPathTermAlgebra s).
+  Proof.
+    by apply reflexive_extend_rel_term_algebra.
+  Defined.
+
+  Lemma reflexive_extend_path_term_algebra_path {s : Sort σ}
+    {S T : CarriersTermAlgebra C s} (p : S = T)
+    : ExtendPathTermAlgebra S T.
+  Proof.
+    induction p. apply reflexive_extend_path_term_algebra.
+  Defined.
+
+  Global Instance symmetric_extend_path_term_algebra
+    : forall s : Sort σ, Symmetric (@ExtendPathTermAlgebra s).
+  Proof.
+    apply symmetric_extend_rel_term_algebra. intros s x y. apply inverse.
+  Defined.
+
+  Global Instance transitive_extend_path_term_algebra
+    : forall s : Sort σ, Transitive (@ExtendPathTermAlgebra s).
+  Proof.
+    apply transitive_extend_rel_term_algebra. intros s x y z. apply concat.
+  Defined.
+
+  Global Instance equivrel_extend_path_term_algebra
+    : forall s : Sort σ, EquivRel (@ExtendPathTermAlgebra s).
+  Proof.
+    constructor; exact _.
+  Qed.
+
+  Global Instance hprop_extend_path_term_algebra (s : Sort σ)
+    : is_mere_relation (CarriersTermAlgebra C s) ExtendPathTermAlgebra.
+  Proof.
+    intros S T. exact _.
+  Defined.
+
+  Lemma dependent_path_extend_path_term_algebra {s1 s2 : Sort σ}
+    (S : CarriersTermAlgebra C s1) (T : CarriersTermAlgebra C s2)
+    (e : ExtendDRelTermAlgebra (fun s => paths) S T)
+    : {p : s1 = s2 | p # S = T}.
+  Proof.
+    generalize dependent s2.
+    induction S as [| u c h];
+        intros s2 [? d | ? d] e;
+        solve [elim e] || destruct e as [p e].
+    - exists p. by induction p, e.
+    - induction p. exists idpath. cbn. f_ap. funext a.
+      destruct (h a _ (d a) (e a)) as [p q].
+      by induction (hset_path2 idpath p).
+  Defined.
+
+  Lemma path_extend_path_term_algebra {s : Sort σ}
+    (S T : CarriersTermAlgebra C s) (e : ExtendPathTermAlgebra S T)
+    : S = T.
+  Proof.
+    destruct (dependent_path_extend_path_term_algebra S T e) as [p q].
+    by induction (hset_path2 idpath p).
+  Defined.
+
+  Global Instance hset_carriers_term_algebra (s : Sort σ)
+    : IsHSet (CarriersTermAlgebra C s).
+  Proof.
+    apply (@ishset_hrel_subpaths _ ExtendPathTermAlgebra).
+    - apply reflexive_extend_path_term_algebra.
+    - apply hprop_extend_path_term_algebra; exact _.
+    - apply path_extend_path_term_algebra.
+  Defined.
+
+  Definition equiv_path_extend_path_term_algebra {s : Sort σ}
+    (S T : CarriersTermAlgebra C s)
+    : ExtendPathTermAlgebra S T <~> (S = T)
+    := equiv_iff_hprop
+        (path_extend_path_term_algebra S T)
+        reflexive_extend_path_term_algebra_path.
+
+End extend_path_term_algebra.
+
+(** At this point we can define the term algebra. *)
+
+Definition TermAlgebra `{Funext} {σ : Signature}
+  (C : Carriers σ) `{!forall s, IsHSet (C s)}
+  : Algebra σ
+  := Build_Algebra (CarriersTermAlgebra C) (@ops_term_algebra _ C).
+
+Lemma isinj_var_term_algebra {σ} (C : Carriers σ) (s : Sort σ) (x y : C s)
+  : var_term_algebra C s x = var_term_algebra C s y -> x = y.
+Proof.
+  intro p.
+  apply reflexive_extend_path_term_algebra_path in p.
+  destruct p as [p1 p2].
+  by destruct (hset_path2 p1 idpath)^.
+Qed.
+
+Lemma isinj_ops_term_algebra `{Funext} {σ} (C : Carriers σ)
+  (u : Symbol σ) (a b : DomOperation (CarriersTermAlgebra C) (σ u))
+  : ops_term_algebra C u a = ops_term_algebra C u b -> a = b.
+Proof.
+  intro p.
+  apply reflexive_extend_path_term_algebra_path in p.
+  destruct p as [p1 p2].
+  destruct (hset_path2 p1 idpath)^.
+  funext i.
+  apply path_extend_path_term_algebra.
+  apply p2.
+Qed.
+
+(** The extension [ExtendRelTermAlgebra R], of a family of mere
+    equivalence relations [R], is a congruence. *)
+
+Global Instance is_congruence_extend_rel_term_algebra
+  `{Funext} {σ} (C : Carriers σ) `{!forall s, IsHSet (C s)}
+  (R : forall s, Relation (C s)) `{!forall s, EquivRel (R s)}
+  `{!forall s, is_mere_relation (C s) (R s)}
+  : IsCongruence (TermAlgebra C) (@ExtendRelTermAlgebra σ C R).
+Proof.
+  constructor.
+  - intros. exact _.
+  - intros. exact _.
+  - intros u a b c.
+    exists idpath.
+    intro i.
+    apply c.
+Defined.
+
+(** Given and family of functions [f : forall s, C s -> A s],
+    we can extend it to a [Homomorphism (TermAlgebra C) A],
+    as shown in the next section. *)
+
+Section hom_term_algebra.
+  Context
+    `{Funext} {σ} {C : Carriers σ} `{!forall s, IsHSet (C s)}
+    (A : Algebra σ) (f : forall s, C s -> A s).
+
+  Definition map_term_algebra {σ} {C : Carriers σ} (A : Algebra σ)
+    (f : forall s, C s -> A s) (s : Sort σ) (T : CarriersTermAlgebra C s)
+    : A s
+    := CarriersTermAlgebra_rec C A f (fun u _ r => u.#A r) s T.
+
+  Global Instance is_homomorphism_map_term_algebra
+    : @IsHomomorphism σ (TermAlgebra C) A (map_term_algebra A f).
+  Proof.
+    intros u a. by refine (ap u.#A _).
+  Qed.
+
+  Definition hom_term_algebra : Homomorphism (TermAlgebra C) A
+    := @Build_Homomorphism σ (TermAlgebra C) A (map_term_algebra A f) _.
+
+End hom_term_algebra.
+
+(** The next section proves the universal property of the term algebra,
+    that [TermAlgebra] is a left adjoint functor
+
+    >>
+      {C : Carriers σ | forall s, IsHSet (C s)} -> Algebra σ,
+    <<
+
+    with right adjoint the forgetful functor. This is stated below as
+    an equivalence
+
+    >>
+      Homomorphism (TermAlgebra C) A <~> (forall s, C s -> A s),
+    <<
+
+    given by precomposition with
+    
+    >>
+      var_term_algebra C s : C s -> TermAlgebra C s.
+    << *)
+
+Section ump_term_algebra.
+  Context
+    `{Funext} {σ} (C : Carriers σ) `{forall s, IsHSet (C s)} (A : Algebra σ).
+
+  (** By precomposing [Homomorphism (TermAlgebra C) A] with
+      [var_term_algebra], we obtain a family [forall s, C s -> A s]. *)
+
+  Definition precomp_var_term_algebra (f : Homomorphism (TermAlgebra C) A)
+    : forall s, C s -> A s
+    := fun s x => f s (var_term_algebra C s x).
+
+  Lemma path_precomp_var_term_algebra_to_hom_term_algebra
+    : forall (f : Homomorphism (TermAlgebra C) A),
+      hom_term_algebra A (precomp_var_term_algebra f) = f.
+  Proof.
+    intro f.
+    apply path_homomorphism.
+    funext s T.
+    induction T as [|u c h].
+    - reflexivity.
+    - refine (_ @ (is_homomorphism_hom f u c)^).
+      refine (ap u.#A _). funext i. apply h.
+  Defined.
+
+  Lemma path_hom_term_algebra_to_precomp_var_term_algebra
+    : forall (f : forall s, C s -> A s),
+      precomp_var_term_algebra (hom_term_algebra A f) = f.
+  Proof.
+    intro f. by funext s a.
+  Defined.
+
+  (** Precomposition with [var_term_algebra] is an equivalence *)
+
+  Global Instance isequiv_precomp_var_term_algebra
+    : IsEquiv precomp_var_term_algebra.
+  Proof.
+    srapply isequiv_adjointify.
+    - apply hom_term_algebra.
+    - intro. apply path_hom_term_algebra_to_precomp_var_term_algebra.
+    - intro. apply path_precomp_var_term_algebra_to_hom_term_algebra.
+  Defined.
+
+  (** The universal property of the term algebra: The [TermAlgebra]
+      is a left adjoint functor.
+      Notice [isequiv_precomp_var_term_algebra] above. *)
+
+  Theorem ump_term_algebra
+    : Homomorphism (TermAlgebra C) A <~> (forall s, C s -> A s).
+  Proof.
+    exact (Build_Equiv _ _ precomp_var_term_algebra _).
+  Defined.
+
+End ump_term_algebra.
diff --git a/theories/Basics/Notations.v b/theories/Basics/Notations.v
index 492c8d57099..279be582475 100644
--- a/theories/Basics/Notations.v
+++ b/theories/Basics/Notations.v
@@ -142,6 +142,9 @@ Reserved Notation "'CAT' // a" (at level 40, left associativity).
 Reserved Notation "'CAT' \\ a" (at level 40, left associativity).
 Reserved Notation "C ^op" (at level 3, format "C '^op'").
 
+(** Universal algebra *)
+Reserved Notation "u .# A" (at level 3, format "u '.#' A").
+
 (** Natural numbers *)
 Reserved Infix "=n" (at level 70, no associativity).
 
@@ -216,7 +219,6 @@ Reserved Notation "x \\ F" (at level 40, left associativity).
 Reserved Notation "x // F" (at level 40, left associativity).
 Reserved Notation "{ { xL | xR // xcut } }" (at level 0, xR at level 39, format "{ {  xL  |  xR  //  xcut  } }").
 Reserved Notation "x \ F" (at level 40, left associativity).
-Reserved Notation "x / F" (at level 40, left associativity).
 Reserved Notation "x <> y" (at level 70, no associativity).
 Reserved Notation "x ->> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x -|-> y" (at level 99, right associativity, y at level 200).
diff --git a/theories/Classes/interfaces/ua_algebra.v b/theories/Classes/interfaces/ua_algebra.v
index beb4055bb53..9b9f5b56e61 100644
--- a/theories/Classes/interfaces/ua_algebra.v
+++ b/theories/Classes/interfaces/ua_algebra.v
@@ -160,6 +160,8 @@ Arguments BuildAlgebra {σ} carriers operations.
     family of carriers. *)
 Global Coercion carriers : Algebra >-> Funclass.
 
+Bind Scope Algebra_scope with Algebra.
+
 Definition SigAlgebra (σ : Signature) : Type
   := {c : Carriers σ | ∀ (u : Symbol σ), Operation c (σ u) }.
 
@@ -240,11 +242,8 @@ Defined.
 Module algebra_notations.
 
 (** Given [A : Algebra σ] and function symbol [u : Symbol σ], we use
-    the notation [u ^^ A] to refer to the corresponding algebra
+    the notation [u .# A] to refer to the corresponding algebra
     operation of type [Operation A (σ u)]. *)
-(** Note: We must reserve this notation here since it messes with the parsing of double inversion of paths *)
-  Global Notation "u ^^ A" := (operations A u)
-                              (at level 60, no associativity)
-                              : Algebra_scope.
+  Global Notation "u .# A" := (operations A u) : Algebra_scope.
 
 End algebra_notations.
diff --git a/theories/Classes/interfaces/ua_congruence.v b/theories/Classes/interfaces/ua_congruence.v
index 05056eb8046..6cdb849a16d 100644
--- a/theories/Classes/interfaces/ua_congruence.v
+++ b/theories/Classes/interfaces/ua_congruence.v
@@ -32,7 +32,7 @@ Section congruence.
        Φ (cod_symboltype w) (ap_operation f a) (ap_operation f b).
 
   Class OpsCompatible : Type
-    := ops_compatible : ∀ (u : Symbol σ), OpCompatible (u^^A).
+    := ops_compatible : ∀ (u : Symbol σ), OpCompatible u.#A.
 
   Global Instance trunc_ops_compatible `{Funext} {n : trunc_index}
     `{!∀ s x y, IsTrunc n (Φ s x y)}
diff --git a/theories/Classes/theory/ua_first_isomorphism.v b/theories/Classes/theory/ua_first_isomorphism.v
index 718568a20f2..ec81c7ebc02 100644
--- a/theories/Classes/theory/ua_first_isomorphism.v
+++ b/theories/Classes/theory/ua_first_isomorphism.v
@@ -119,7 +119,7 @@ Section first_isomorphism.
 *)
 
   Definition def_first_isomorphism (s : Sort σ)
-    : (A / cong_ker f) s → (B & in_image_hom f) s.
+    : (A / cong_ker f) s → (B && in_image_hom f) s.
   Proof.
     refine (quotient_rec (cong_ker f s) (λ x, (f s x; tr (x; idpath))) _).
     intros x y p.
@@ -154,13 +154,13 @@ Section first_isomorphism.
   Global Instance is_homomorphism_first_isomorphism
     : IsHomomorphism def_first_isomorphism.
   Proof.
-    intro u. apply (oppreserving_first_isomorphism (u^^A)).
+    intro u. apply (oppreserving_first_isomorphism u.#A).
     - apply hom.
     - apply compute_op_quotient.
   Qed.
 
   Definition hom_first_isomorphism
-    : Homomorphism (A / cong_ker f) (B & in_image_hom f)
+    : Homomorphism (A / cong_ker f) (B && in_image_hom f)
     := BuildHomomorphism def_first_isomorphism.
 
   Global Instance embedding_first_isomorphism (s : Sort σ)
@@ -191,7 +191,7 @@ Section first_isomorphism.
   Qed.
 
   Theorem isomorphic_first_isomorphism
-    : A / cong_ker f ≅ B & in_image_hom f.
+    : A / cong_ker f ≅ B && in_image_hom f.
   Proof.
     exact (BuildIsomorphic def_first_isomorphism).
   Defined.
@@ -199,7 +199,7 @@ Section first_isomorphism.
 (* The first identification theorem [id_first_isomorphism] is an
    h-prop, so we can leave it opaque. *)
 
-  Corollary id_first_isomorphism : A / cong_ker f = B & in_image_hom f.
+  Corollary id_first_isomorphism : A / cong_ker f = B && in_image_hom f.
   Proof.
     exact (id_isomorphic isomorphic_first_isomorphism).
   Qed.
@@ -259,15 +259,15 @@ Section first_isomorphism_inj.
     composition of two isomorphisms, so it is an isomorphism. *)
 
   Definition hom_first_isomorphism_inj
-    : Homomorphism A (B & in_image_hom f)
+    : Homomorphism A (B && in_image_hom f)
     := hom_compose
           (hom_first_isomorphism f)
           (hom_quotient (cong_ker f)).
 
-  Definition isomorphic_first_isomorphism_inj : A ≅ B & in_image_hom f
+  Definition isomorphic_first_isomorphism_inj : A ≅ B && in_image_hom f
     := BuildIsomorphic hom_first_isomorphism_inj.
 
-  Definition id_first_isomorphism_inj : A = B & in_image_hom f
+  Definition id_first_isomorphism_inj : A = B && in_image_hom f
     := id_isomorphic isomorphic_first_isomorphism_inj.
 
 End first_isomorphism_inj.
diff --git a/theories/Classes/theory/ua_homomorphism.v b/theories/Classes/theory/ua_homomorphism.v
index b1a475a444f..42116bafed4 100644
--- a/theories/Classes/theory/ua_homomorphism.v
+++ b/theories/Classes/theory/ua_homomorphism.v
@@ -44,11 +44,11 @@ Section is_homomorphism.
 
 (** The family of functions [f : ∀ (s : Sort σ), A s → B s] above is
     a homomorphism if for each function symbol [u : Symbol σ], it is
-    [OpPreserving (u^^A) (u^^B)] with respect to the algebra
-    operations [u^^A] and [u^^B] corresponding to [u]. *)
+    [OpPreserving u.#A u.#B] with respect to the algebra
+    operations [u.#A] and [u.#B] corresponding to [u]. *)
 
   Class IsHomomorphism : Type
-    := oppreserving_hom : ∀ (u : Symbol σ), OpPreserving (u^^A) (u^^B).
+    := oppreserving_hom : ∀ (u : Symbol σ), OpPreserving u.#A u.#B.
 
   Global Instance trunc_is_homomorphism `{Funext} {n : trunc_index}
     `{!IsTruncAlgebra n.+1 B}
@@ -182,13 +182,13 @@ Section homomorphism_ap_operation.
     >>
 
     where [(a1, a2, ..., an, tt) : FamilyProd A [s1; s2; ...; sn]] and
-    [α], [β] uncurried versions of [u^^A], [u^^B] respectively. *)
+    [α], [β] uncurried versions of [u.#A], [u.#B] respectively. *)
 
   Lemma path_homomorphism_ap_operation (f : ∀ s, A s → B s)
     `{!IsHomomorphism f}
     : ∀ (u : Symbol σ) (a : FamilyProd A (dom_symboltype (σ u))),
-      f (cod_symboltype (σ u)) (ap_operation (u^^A) a)
-      = ap_operation (u^^B) (map_family_prod f a).
+      f (cod_symboltype (σ u)) (ap_operation u.#A a)
+      = ap_operation u.#B (map_family_prod f a).
   Proof.
     intros u a. by apply path_oppreserving_ap_operation.
   Defined.
@@ -203,7 +203,7 @@ Section hom_id.
   Global Instance is_homomorphism_id
     : IsHomomorphism (λ s (x : A s), x).
   Proof.
-    intro u. generalize (u^^A). intro w. induction (σ u).
+    intro u. generalize u.#A. intro w. induction (σ u).
     - reflexivity.
     - now intro x.
   Defined.
@@ -231,7 +231,7 @@ Section hom_inv.
   Global Instance is_homomorphism_inv : IsHomomorphism (λ s, (f s)^-1).
   Proof.
    intro u.
-   generalize (u^^A) (u^^B) (oppreserving_hom f u).
+   generalize u.#A u.#B (oppreserving_hom f u).
    intros a b P.
    induction (σ u).
    - destruct P. apply (eissect (f t)).
@@ -275,7 +275,7 @@ Section hom_compose.
     : IsHomomorphism (λ s, g s o f s).
   Proof.
     intro u.
-    by apply (oppreserving_compose g f (u^^A) (u^^B) (u^^C)).
+    by apply (oppreserving_compose g f u.#A u.#B u.#C).
   Defined.
 
   Global Instance is_isomorphism_compose
@@ -338,21 +338,21 @@ Section path_isomorphism.
   Qed.
 
 (** Suppose [u : Symbol σ] is a function symbol. Recall that
-    [u^^A] is notation for [operations A u : Operation A (σ u)]. This
+    [u.#A] is notation for [operations A u : Operation A (σ u)]. This
     is the algebra operation corresponding to function symbol [u]. *)
 
 (** An isomorphism [f : ∀ s, A s → B s] induces a family of
     equivalences [e : ∀ (s : Sort σ), A s <~> B s]. Let [u : Symbol σ]
     be a function symbol. Since [f] is a homomorphism, the induced
-    family of equivalences [e] satisfies [OpPreserving e (u^^A) (u^^B)].
-    By [path_operations_equiv] above, we can then transport [u^^A] along
-    the path [path_equiv_family e] and obtain a path to [u^^B]. *)
+    family of equivalences [e] satisfies [OpPreserving e (u.#A) (u.#B)].
+    By [path_operations_equiv] above, we can then transport [u.#A] along
+    the path [path_equiv_family e] and obtain a path to [u.#B]. *)
 
   Lemma path_operations_isomorphism (f : ∀ s, A s → B s)
     `{IsIsomorphism σ A B f} (u : Symbol σ)
     : transport (λ C : Carriers σ, Operation C (σ u))
-        (path_equiv_family (equiv_isomorphism f)) (u^^A)
-      = u^^B.
+        (path_equiv_family (equiv_isomorphism f)) u.#A
+      = u.#B.
   Proof.
     by apply path_operations_equiv.
   Defined.
diff --git a/theories/Classes/theory/ua_prod_algebra.v b/theories/Classes/theory/ua_prod_algebra.v
index d7c485a0f3e..b2ef2e41619 100644
--- a/theories/Classes/theory/ua_prod_algebra.v
+++ b/theories/Classes/theory/ua_prod_algebra.v
@@ -30,7 +30,7 @@ Section prod_algebra.
 
   Definition ops_prod_algebra (u : Symbol σ)
     : Operation carriers_prod_algebra (σ u)
-    := op_prod_algebra (σ u) (λ (i:I), u ^^ A i).
+    := op_prod_algebra (σ u) (λ (i:I), u.#(A i)).
 
   Definition ProdAlgebra : Algebra σ
     := BuildAlgebra carriers_prod_algebra ops_prod_algebra.
diff --git a/theories/Classes/theory/ua_quotient_algebra.v b/theories/Classes/theory/ua_quotient_algebra.v
index 3a6b79bbd48..4d3d0c9bd61 100644
--- a/theories/Classes/theory/ua_quotient_algebra.v
+++ b/theories/Classes/theory/ua_quotient_algebra.v
@@ -127,7 +127,7 @@ Section quotient_algebra.
 
   Definition ops_quotient_algebra (u : Symbol σ)
     : Operation carriers_quotient_algebra (σ u)
-    := (op_quotient_algebra (u^^A) (ops_compatible_cong A Φ u)).1.
+    := (op_quotient_algebra u.#A (ops_compatible_cong A Φ u)).1.
 
 (** Definition of quotient algebra. See Lemma [compute_op_quotient]
     below for the computation rule of quotient algebra operations. *)
@@ -152,11 +152,11 @@ Section quotient_algebra.
       = class_of _ (α (a1, a2, ..., an))
     >>
 
-    where [α] is the uncurried [u^^A] operation and [β] is the
-    uncurried [u^^QuotientAlgebra] operation. *)
+    where [α] is the uncurried [u.#A] operation and [β] is the
+    uncurried [u.#QuotientAlgebra] operation. *)
 
   Lemma compute_op_quotient (u : Symbol σ)
-    : ComputeOpQuotient (u^^A) (u^^QuotientAlgebra).
+    : ComputeOpQuotient u.#A u.#QuotientAlgebra.
   Proof.
     apply op_quotient_algebra.
   Defined.
diff --git a/theories/Classes/theory/ua_second_isomorphism.v b/theories/Classes/theory/ua_second_isomorphism.v
index 628a03afda3..22c63dcc1b1 100644
--- a/theories/Classes/theory/ua_second_isomorphism.v
+++ b/theories/Classes/theory/ua_second_isomorphism.v
@@ -27,7 +27,7 @@ Section cong_trace.
     (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)
+  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 σ)
@@ -41,8 +41,8 @@ Section cong_trace.
   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)
+    (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.
@@ -53,7 +53,7 @@ Section cong_trace.
   Qed.
 
   Global Instance ops_compatible_trace_trace
-    : OpsCompatible (A&P) cong_trace.
+    : OpsCompatible (A&&P) cong_trace.
   Proof.
     intros u a b R.
     refine (transport (λ X, Φ _ X _)
@@ -64,9 +64,9 @@ Section cong_trace.
     exact (for_all_2_family_prod_trace_congruence a b R).
   Qed.
 
-  Global Instance is_congruence_trace : IsCongruence (A&P) cong_trace.
+  Global Instance is_congruence_trace : IsCongruence (A&&P) cong_trace.
   Proof.
-    apply (@BuildIsCongruence _ (A&P) cong_trace);
+    apply (@BuildIsCongruence _ (A&&P) cong_trace);
       [intros; apply (is_mere_relation_cong A Φ) | exact _ ..].
   Qed.
 End cong_trace.
@@ -81,7 +81,7 @@ Section is_subalgebra_class.
     (Φ : ∀ 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)).
+    := hexists (λ (y : (A&&P) s), in_class (Φ s) x (i s y)).
 
   Lemma op_closed_subalgebra_is_subalgebra_class {w : SymbolType σ}
     (γ : Operation (A/Φ) w)
@@ -125,7 +125,7 @@ End is_subalgebra_class.
 (** The next section proves the second isomorphism theorem,
 
     <<
-      (A&P) / (cong_trace P Φ) ≅ (A/Φ) & (is_subalgebra_class P Φ).
+      (A&&P) / (cong_trace P Φ) ≅ (A/Φ) && (is_subalgebra_class P Φ).
     >>
 *)
 
@@ -143,19 +143,19 @@ Section second_isomorphism.
   Local Notation Q := (is_subalgebra_class P Φ).
 
   Definition def_second_isomorphism (s : Sort σ)
-    : ((A&P) / Ψ) s → ((A/Φ) & Q) s
+    : ((A&&P) / Ψ) s → ((A/Φ) && Q) s
     := quotient_rec (Ψ s)
-        (λ (x : (A&P) 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),
+        (λ (x y : (A&&P) s) (T : Ψ s x y),
          path_sigma_hprop (class_of (Φ s) (i s x); _)
            (class_of (Φ s) (i s y); _) (related_classes_eq (Φ s) T)).
 
   Lemma oppreserving_second_isomorphism {w : SymbolType σ}
     (α : Operation A w) (γ : Operation (A/Φ) w)
-    (ζ : Operation ((A&P) / Ψ) w) (CA : ClosedUnderOp (A/Φ) Q γ)
+    (ζ : Operation ((A&&P) / Ψ) w) (CA : ClosedUnderOp (A/Φ) Q γ)
     (CB : ClosedUnderOp A P α) (QA : ComputeOpQuotient A Φ α γ)
-    (QB : ComputeOpQuotient (A&P) Ψ (op_subalgebra A P α CB) ζ)
+    (QB : ComputeOpQuotient (A&&P) Ψ (op_subalgebra A P α CB) ζ)
     : OpPreserving def_second_isomorphism ζ (op_subalgebra (A/Φ) Q γ CA).
   Proof.
     unfold ComputeOpQuotient in *.
@@ -178,11 +178,11 @@ Section second_isomorphism.
     intro u.
     eapply oppreserving_second_isomorphism.
     - apply (compute_op_quotient A).
-    - apply (compute_op_quotient (A&P)).
+    - apply (compute_op_quotient (A&&P)).
   Defined.
 
   Definition hom_second_isomorphism
-    : Homomorphism ((A&P) / Ψ) ((A/Φ) & Q)
+    : Homomorphism ((A&&P) / Ψ) ((A/Φ) && Q)
     := BuildHomomorphism def_second_isomorphism.
 
   Global Instance embedding_second_isomorphism (s : Sort σ)
@@ -217,12 +217,12 @@ Section second_isomorphism.
 
   Global Existing Instance is_isomorphism_second_isomorphism.
 
-  Theorem isomorphic_second_isomorphism : (A&P) / Ψ ≅ (A/Φ) & Q.
+  Theorem isomorphic_second_isomorphism : (A&&P) / Ψ ≅ (A/Φ) && Q.
   Proof.
     exact (BuildIsomorphic def_second_isomorphism).
   Defined.
 
-  Corollary id_second_isomorphism : (A&P) / Ψ = (A/Φ) & Q.
+  Corollary id_second_isomorphism : (A&&P) / Ψ = (A/Φ) && Q.
   Proof.
     exact (id_isomorphic isomorphic_second_isomorphism).
   Defined.
diff --git a/theories/Classes/theory/ua_subalgebra.v b/theories/Classes/theory/ua_subalgebra.v
index 3f4506bfb1f..4c01570b6d1 100644
--- a/theories/Classes/theory/ua_subalgebra.v
+++ b/theories/Classes/theory/ua_subalgebra.v
@@ -40,7 +40,7 @@ Section closed_under_op.
   Qed.
 
   Definition IsClosedUnderOps : Type
-    := ∀ (u : Symbol σ), ClosedUnderOp (u^^A).
+    := ∀ (u : Symbol σ), ClosedUnderOp u.#A.
 
   Global Instance trunc_is_closed_under_ops
     {n} `{∀ s x, IsTrunc n (P s x)}
@@ -110,7 +110,7 @@ Section subalgebra.
 
   Definition ops_subalgebra (u : Symbol σ)
     : Operation carriers_subalgebra (σ u)
-    := op_subalgebra (u^^A) (is_closed_under_ops_subalgebra_predicate A P u).
+    := op_subalgebra u.#A (is_closed_under_ops_subalgebra_predicate A P u).
 
   Definition Subalgebra : Algebra σ
     := BuildAlgebra carriers_subalgebra ops_subalgebra.
@@ -127,10 +127,9 @@ Section subalgebra.
 End subalgebra.
 
 Module subalgebra_notations.
-  (** Cannot reserve since it messes with sigma type notation *)
-  Notation "A & P" := (Subalgebra A P)
-                      (at level 50, left associativity)
-                      : Algebra_scope.
+
+  Notation "A && P" := (Subalgebra A P) : Algebra_scope.
+
 End subalgebra_notations.
 
 Import subalgebra_notations.
@@ -143,7 +142,7 @@ Section hom_inc_subalgebra.
     {σ : Signature} (A : Algebra σ)
     (P : ∀ s, A s → Type) `{!IsSubalgebraPredicate A P}.
 
-  Definition def_inc_subalgebra (s : Sort σ) : (A&P) s → A s
+  Definition def_inc_subalgebra (s : Sort σ) : (A&&P) s → A s
     := pr1.
 
   Lemma oppreserving_inc_subalgebra {w : SymbolType σ}
@@ -161,7 +160,7 @@ Section hom_inc_subalgebra.
     intro u. apply oppreserving_inc_subalgebra.
   Defined.
 
-  Definition hom_inc_subalgebra : Homomorphism (A&P) A
+  Definition hom_inc_subalgebra : Homomorphism (A&&P) A
     := BuildHomomorphism def_inc_subalgebra.
 
   Lemma is_isomorphism_inc_improper_subalgebra
@@ -185,13 +184,13 @@ Section path_subalgebra.
     (P : ∀ s, A s → Type) {CP : IsSubalgebraPredicate A P}
     (Q : ∀ s, A s → Type) {CQ : IsSubalgebraPredicate A Q}.
 
-  Lemma path_subalgebra `{Funext} (p : P = Q) : A&P = A&Q.
+  Lemma path_subalgebra `{Funext} (p : P = Q) : A&&P = A&&Q.
   Proof.
     by destruct p, (path_ishprop CP CQ).
   Defined.
 
   Lemma path_subalgebra_iff `{Univalence} (R : ∀ s x, P s x <-> Q s x)
-    : A&P = A&Q.
+    : A&&P = A&&Q.
   Proof.
     apply path_subalgebra.
     funext s x.
diff --git a/theories/Classes/theory/ua_third_isomorphism.v b/theories/Classes/theory/ua_third_isomorphism.v
index 973a0f9f927..fcb00541eba 100644
--- a/theories/Classes/theory/ua_third_isomorphism.v
+++ b/theories/Classes/theory/ua_third_isomorphism.v
@@ -67,17 +67,17 @@ Section cong_quotient.
     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 / Ψ)
+              : ap_operation (u.#(A / Ψ))
                  (map_family_prod (λ s, class_of (Ψ s)) _) = _)^.
     destruct (compute_op_quotient A Ψ u b
-              : ap_operation (u^^A / Ψ)
+              : 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).
+    transitivity (ap_operation u.#A a).
     - by symmetry.
-    - transitivity (ap_operation (u^^A) b); try assumption.
+    - transitivity (ap_operation u.#A b); try assumption.
       apply (ops_compatible A Φ u).
       by apply for_all_relation_quotient.
   Defined.