(** 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.Universes.HSet
  HoTT.Classes.interfaces.canonical_names
  HoTT.Algebra.Universal.Homomorphism
  HoTT.Algebra.Universal.Congruence.

Unset Elimination Schemes.

Local Open Scope Algebra_scope.

(** 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 := Induction 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 relations. *)

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)}.

  #[export] Instance hprop_extend_drel_term_algebra {s1 s2 : Sort σ}
    (S : CarriersTermAlgebra C s1) (T : CarriersTermAlgebra C s2)
    : IsHProp (ExtendDRelTermAlgebra R S T).
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
s1, s2: Sort σ
S: CarriersTermAlgebra C s1
T: CarriersTermAlgebra C s2
IsHProp (ExtendDRelTermAlgebra R S T)
  Proof.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
s1, s2: Sort σ
S: CarriersTermAlgebra C s1
T: CarriersTermAlgebra C s2
IsHProp (ExtendDRelTermAlgebra R S T)
    generalize dependent s2.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
s1: Sort σ
S: CarriersTermAlgebra C s1
forall (s2 : Sort σ) (T : CarriersTermAlgebra C s2),
IsHProp (ExtendDRelTermAlgebra R S T)
    induction S; intros s2 T; destruct T; exact _.
  Qed.

  #[export] Instance reflexive_extend_rel_term_algebra
    `{!forall s, Reflexive (R s)} {s : Sort σ}
    : Reflexive (@ExtendRelTermAlgebra σ C R s).
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Reflexive (R s0)
s: Sort σ
Reflexive (ExtendRelTermAlgebra R)
  Proof.
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Reflexive (R s0)
s: Sort σ
Reflexive (ExtendRelTermAlgebra R)
    intro S.
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Reflexive (R s0)
s: Sort σ
S: CarriersTermAlgebra C s
ExtendRelTermAlgebra R S S induction S as [| u c h].
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Reflexive (R s0)
s: Sort σ
c: C s
ExtendRelTermAlgebra R (var_term_algebra C s c) (var_term_algebra C s c)
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Reflexive (R s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall i : Arity (σ u), ExtendRelTermAlgebra R (c i) (c i)
ExtendRelTermAlgebra R (ops_term_algebra C u c) (ops_term_algebra C u c)
    -
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Reflexive (R s0)
s: Sort σ
c: C s
ExtendRelTermAlgebra R (var_term_algebra C s c) (var_term_algebra C s c) by exists idpath.
    -
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Reflexive (R s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall i : Arity (σ u), ExtendRelTermAlgebra R (c i) (c i)
ExtendRelTermAlgebra R (ops_term_algebra C u c) (ops_term_algebra C u c) exists idpath.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Reflexive (R s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall i : Arity (σ u), ExtendRelTermAlgebra R (c i) (c i)
forall i : Arity (σ u),
ExtendDRelTermAlgebra R (c i)
  (c (transport (fun v : Symbol σ => Arity (σ v)) 1 i)) intro i.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Reflexive (R s)
u: Symbol σ
c: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
h: forall i0 : Arity (σ u), ExtendRelTermAlgebra R (c i0) (c i0)
i: Arity (σ u)
ExtendDRelTermAlgebra R (c i)
  (c (transport (fun v : Symbol σ => Arity (σ v)) 1 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.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Symmetric (R s)
s1, s2: Sort σ
S: CarriersTermAlgebra C s1
T: CarriersTermAlgebra C s2
h: ExtendDRelTermAlgebra R S T
ExtendDRelTermAlgebra R T S
  Proof.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Symmetric (R s)
s1, s2: Sort σ
S: CarriersTermAlgebra C s1
T: CarriersTermAlgebra C s2
h: ExtendDRelTermAlgebra R S T
ExtendDRelTermAlgebra R T S
    generalize dependent s2.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Symmetric (R s)
s1: Sort σ
S: CarriersTermAlgebra C s1
forall (s2 : Sort σ) (T : CarriersTermAlgebra C s2),
ExtendDRelTermAlgebra R S T -> ExtendDRelTermAlgebra R T S
    induction S as [| u c h]; intros s2 [] p.
H: Funext
σ: Signature
C: Carriers σ
R: forall s1 : Sort σ, Relation (C s1)
H0: forall (s1 : Sort σ) (x y : C s1), IsHProp (R s1 x y)
H1: forall s1 : Sort σ, Symmetric (R s1)
s: Sort σ
c: C s
s2, s0: Sort σ
c0: C s0
p: ExtendDRelTermAlgebra R (var_term_algebra C s c) (var_term_algebra C s0 c0)
ExtendDRelTermAlgebra R (var_term_algebra C s0 c0) (var_term_algebra C s c)
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Symmetric (R s0)
s: Sort σ
c: C s
s2: Sort σ
u: Symbol σ
c0: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
p: ExtendDRelTermAlgebra R (var_term_algebra C s c) (ops_term_algebra C u c0)
ExtendDRelTermAlgebra R (ops_term_algebra C u c0) (var_term_algebra C s c)
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Symmetric (R s0)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i) T -> ExtendDRelTermAlgebra R T (c i)
s2, s: Sort σ
c0: C s
p: ExtendDRelTermAlgebra R (ops_term_algebra C u c) (var_term_algebra C s c0)
ExtendDRelTermAlgebra R (var_term_algebra C s c0) (ops_term_algebra C u c)
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Symmetric (R s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i) T -> ExtendDRelTermAlgebra R T (c i)
s2: Sort σ
u0: Symbol σ
c0: forall i : Arity (σ u0), CarriersTermAlgebra C (sorts_dom (σ u0) i)
p: ExtendDRelTermAlgebra R (ops_term_algebra C u c) (ops_term_algebra C u0 c0)
ExtendDRelTermAlgebra R (ops_term_algebra C u0 c0) (ops_term_algebra C u c)
    -
H: Funext
σ: Signature
C: Carriers σ
R: forall s1 : Sort σ, Relation (C s1)
H0: forall (s1 : Sort σ) (x y : C s1), IsHProp (R s1 x y)
H1: forall s1 : Sort σ, Symmetric (R s1)
s: Sort σ
c: C s
s2, s0: Sort σ
c0: C s0
p: ExtendDRelTermAlgebra R (var_term_algebra C s c) (var_term_algebra C s0 c0)
ExtendDRelTermAlgebra R (var_term_algebra C s0 c0) (var_term_algebra C s c) destruct p as [p1 p2].
H: Funext
σ: Signature
C: Carriers σ
R: forall s1 : Sort σ, Relation (C s1)
H0: forall (s1 : Sort σ) (x y : C s1), IsHProp (R s1 x y)
H1: forall s1 : Sort σ, Symmetric (R s1)
s: Sort σ
c: C s
s2, s0: Sort σ
c0: C s0
p1: s = s0
p2: R s0 (transport C p1 c) c0
ExtendDRelTermAlgebra R (var_term_algebra C s0 c0) (var_term_algebra C s c)
      induction p1.
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Symmetric (R s0)
s: Sort σ
c: C s
s2: Sort σ
c0: C s
p2: R s (transport C 1 c) c0
ExtendDRelTermAlgebra R (var_term_algebra C s c0) (var_term_algebra C s c) exists idpath.
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Symmetric (R s0)
s: Sort σ
c: C s
s2: Sort σ
c0: C s
p2: R s (transport C 1 c) c0
R s (transport C 1 c0) c by symmetry.
    -
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Symmetric (R s0)
s: Sort σ
c: C s
s2: Sort σ
u: Symbol σ
c0: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
p: ExtendDRelTermAlgebra R (var_term_algebra C s c) (ops_term_algebra C u c0)
ExtendDRelTermAlgebra R (ops_term_algebra C u c0) (var_term_algebra C s c) elim p.
    -
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Symmetric (R s0)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i) T -> ExtendDRelTermAlgebra R T (c i)
s2, s: Sort σ
c0: C s
p: ExtendDRelTermAlgebra R (ops_term_algebra C u c) (var_term_algebra C s c0)
ExtendDRelTermAlgebra R (var_term_algebra C s c0) (ops_term_algebra C u c) elim p.
    -
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Symmetric (R s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i) T -> ExtendDRelTermAlgebra R T (c i)
s2: Sort σ
u0: Symbol σ
c0: forall i : Arity (σ u0), CarriersTermAlgebra C (sorts_dom (σ u0) i)
p: ExtendDRelTermAlgebra R (ops_term_algebra C u c) (ops_term_algebra C u0 c0)
ExtendDRelTermAlgebra R (ops_term_algebra C u0 c0) (ops_term_algebra C u c) destruct p as [p f].
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Symmetric (R s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i) T -> ExtendDRelTermAlgebra R T (c i)
s2: Sort σ
u0: Symbol σ
c0: forall i : Arity (σ u0), CarriersTermAlgebra C (sorts_dom (σ u0) i)
p: u = u0
f: forall i : Arity (σ u),
ExtendDRelTermAlgebra R (c i)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) p i))
ExtendDRelTermAlgebra R (ops_term_algebra C u0 c0) (ops_term_algebra C u c)
      induction p.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Symmetric (R s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i) T -> ExtendDRelTermAlgebra R T (c i)
s2: Sort σ
c0: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
f: forall i : Arity (σ u),
ExtendDRelTermAlgebra R (c i)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) 1 i))
ExtendDRelTermAlgebra R (ops_term_algebra C u c0) (ops_term_algebra C u c) exists idpath.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Symmetric (R s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i) T -> ExtendDRelTermAlgebra R T (c i)
s2: Sort σ
c0: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
f: forall i : Arity (σ u),
ExtendDRelTermAlgebra R (c i)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) 1 i))
forall i : Arity (σ u),
ExtendDRelTermAlgebra R (c0 i)
  (c (transport (fun v : Symbol σ => Arity (σ v)) 1 i)) intro i.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Symmetric (R s)
u: Symbol σ
c: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
h: forall (i0 : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i0) T -> ExtendDRelTermAlgebra R T (c i0)
s2: Sort σ
c0: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
f: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra R (c i0)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) 1 i0))
i: Arity (σ u)
ExtendDRelTermAlgebra R (c0 i)
  (c (transport (fun v : Symbol σ => Arity (σ v)) 1 i)) apply h.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Symmetric (R s)
u: Symbol σ
c: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
h: forall (i0 : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i0) T -> ExtendDRelTermAlgebra R T (c i0)
s2: Sort σ
c0: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
f: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra R (c i0)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) 1 i0))
i: Arity (σ u)
ExtendDRelTermAlgebra R (c (transport (fun v : Symbol σ => Arity (σ v)) 1 i))
  (c0 i) apply f.
  Qed.

  #[export] Instance symmetric_extend_rel_term_algebra
    `{!forall s, Symmetric (R s)} {s : Sort σ}
    : Symmetric (@ExtendRelTermAlgebra σ C R s).
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Symmetric (R s0)
s: Sort σ
Symmetric (ExtendRelTermAlgebra R)
  Proof.
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Symmetric (R s0)
s: Sort σ
Symmetric (ExtendRelTermAlgebra R)
    intros S T.
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Symmetric (R s0)
s: Sort σ
S, T: CarriersTermAlgebra C s
ExtendRelTermAlgebra R S T -> ExtendRelTermAlgebra R T S 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.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, 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.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, 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
    generalize dependent s3.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Transitive (R s)
s1, s2: Sort σ
S: CarriersTermAlgebra C s1
T: CarriersTermAlgebra C s2
h1: ExtendDRelTermAlgebra R S T
forall (s3 : Sort σ) (U : CarriersTermAlgebra C s3),
ExtendDRelTermAlgebra R T U -> ExtendDRelTermAlgebra R S U
    generalize dependent s2.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Transitive (R s)
s1: Sort σ
S: CarriersTermAlgebra C s1
forall (s2 : Sort σ) (T : CarriersTermAlgebra C s2),
ExtendDRelTermAlgebra R S T ->
forall (s3 : Sort σ) (U : CarriersTermAlgebra C s3),
ExtendDRelTermAlgebra R T U -> ExtendDRelTermAlgebra R S U
    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).
H: Funext
σ: Signature
C: Carriers σ
R: forall s4 : Sort σ, Relation (C s4)
H0: forall (s4 : Sort σ) (x y : C s4), IsHProp (R s4 x y)
H1: forall s4 : Sort σ, Transitive (R s4)
s: Sort σ
c: C s
s2, s0: Sort σ
d: C s0
p2: s = s0
P2: R s0 (transport C p2 c) d
s3, s1: Sort σ
c0: C s1
p3: s0 = s1
P3: R s1 (transport C p3 d) c0
ExtendDRelTermAlgebra R (var_term_algebra C s c) (var_term_algebra C s1 c0)
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Transitive (R s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i) T ->
forall (s1 : Sort σ) (U : CarriersTermAlgebra C s1),
ExtendDRelTermAlgebra R T U -> ExtendDRelTermAlgebra R (c i) U
s2: Sort σ
u0: Symbol σ
d: forall i : Arity (σ u0), CarriersTermAlgebra C (sorts_dom (σ u0) i)
p2: u = u0
P2: forall i : Arity (σ u),
ExtendDRelTermAlgebra R (c i)
  (d (transport (fun v : Symbol σ => Arity (σ v)) p2 i))
s3: Sort σ
u1: Symbol σ
c0: forall i : Arity (σ u1), CarriersTermAlgebra C (sorts_dom (σ u1) i)
p3: u0 = u1
P3: forall i : Arity (σ u0),
ExtendDRelTermAlgebra R (d i)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) p3 i))
ExtendDRelTermAlgebra R (ops_term_algebra C u c) (ops_term_algebra C u1 c0)
    -
H: Funext
σ: Signature
C: Carriers σ
R: forall s4 : Sort σ, Relation (C s4)
H0: forall (s4 : Sort σ) (x y : C s4), IsHProp (R s4 x y)
H1: forall s4 : Sort σ, Transitive (R s4)
s: Sort σ
c: C s
s2, s0: Sort σ
d: C s0
p2: s = s0
P2: R s0 (transport C p2 c) d
s3, s1: Sort σ
c0: C s1
p3: s0 = s1
P3: R s1 (transport C p3 d) c0
ExtendDRelTermAlgebra R (var_term_algebra C s c) (var_term_algebra C s1 c0) exists (p2 @ p3).
H: Funext
σ: Signature
C: Carriers σ
R: forall s4 : Sort σ, Relation (C s4)
H0: forall (s4 : Sort σ) (x y : C s4), IsHProp (R s4 x y)
H1: forall s4 : Sort σ, Transitive (R s4)
s: Sort σ
c: C s
s2, s0: Sort σ
d: C s0
p2: s = s0
P2: R s0 (transport C p2 c) d
s3, s1: Sort σ
c0: C s1
p3: s0 = s1
P3: R s1 (transport C p3 d) c0
R s1 (transport C (p2 @ p3) c) c0
      rewrite transport_pp.
H: Funext
σ: Signature
C: Carriers σ
R: forall s4 : Sort σ, Relation (C s4)
H0: forall (s4 : Sort σ) (x y : C s4), IsHProp (R s4 x y)
H1: forall s4 : Sort σ, Transitive (R s4)
s: Sort σ
c: C s
s2, s0: Sort σ
d: C s0
p2: s = s0
P2: R s0 (transport C p2 c) d
s3, s1: Sort σ
c0: C s1
p3: s0 = s1
P3: R s1 (transport C p3 d) c0
R s1 (transport C p3 (transport C p2 c)) c0
      induction p2, p3.
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Transitive (R s0)
s: Sort σ
c: C s
s2: Sort σ
d: C s
P2: R s (transport C 1 c) d
s3: Sort σ
c0: C s
P3: R s (transport C 1 d) c0
R s (transport C 1 (transport C 1 c)) c0
      by transitivity d.
    -
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Transitive (R s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i) T ->
forall (s1 : Sort σ) (U : CarriersTermAlgebra C s1),
ExtendDRelTermAlgebra R T U -> ExtendDRelTermAlgebra R (c i) U
s2: Sort σ
u0: Symbol σ
d: forall i : Arity (σ u0), CarriersTermAlgebra C (sorts_dom (σ u0) i)
p2: u = u0
P2: forall i : Arity (σ u),
ExtendDRelTermAlgebra R (c i)
  (d (transport (fun v : Symbol σ => Arity (σ v)) p2 i))
s3: Sort σ
u1: Symbol σ
c0: forall i : Arity (σ u1), CarriersTermAlgebra C (sorts_dom (σ u1) i)
p3: u0 = u1
P3: forall i : Arity (σ u0),
ExtendDRelTermAlgebra R (d i)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) p3 i))
ExtendDRelTermAlgebra R (ops_term_algebra C u c) (ops_term_algebra C u1 c0) exists (p2 @ p3).
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Transitive (R s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i) T ->
forall (s1 : Sort σ) (U : CarriersTermAlgebra C s1),
ExtendDRelTermAlgebra R T U -> ExtendDRelTermAlgebra R (c i) U
s2: Sort σ
u0: Symbol σ
d: forall i : Arity (σ u0), CarriersTermAlgebra C (sorts_dom (σ u0) i)
p2: u = u0
P2: forall i : Arity (σ u),
ExtendDRelTermAlgebra R (c i)
  (d (transport (fun v : Symbol σ => Arity (σ v)) p2 i))
s3: Sort σ
u1: Symbol σ
c0: forall i : Arity (σ u1), CarriersTermAlgebra C (sorts_dom (σ u1) i)
p3: u0 = u1
P3: forall i : Arity (σ u0),
ExtendDRelTermAlgebra R (d i)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) p3 i))
forall i : Arity (σ u),
ExtendDRelTermAlgebra R (c i)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) (p2 @ p3) i))
      intro i.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Transitive (R s)
u: Symbol σ
c: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
h: forall (i0 : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i0) T ->
forall (s1 : Sort σ) (U : CarriersTermAlgebra C s1),
ExtendDRelTermAlgebra R T U -> ExtendDRelTermAlgebra R (c i0) U
s2: Sort σ
u0: Symbol σ
d: forall i0 : Arity (σ u0), CarriersTermAlgebra C (sorts_dom (σ u0) i0)
p2: u = u0
P2: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra R (c i0)
  (d (transport (fun v : Symbol σ => Arity (σ v)) p2 i0))
s3: Sort σ
u1: Symbol σ
c0: forall i0 : Arity (σ u1), CarriersTermAlgebra C (sorts_dom (σ u1) i0)
p3: u0 = u1
P3: forall i0 : Arity (σ u0),
ExtendDRelTermAlgebra R (d i0)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) p3 i0))
i: Arity (σ u)
ExtendDRelTermAlgebra R (c i)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) (p2 @ p3) i))
      induction p2.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Transitive (R s)
u: Symbol σ
c: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
h: forall (i0 : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i0) T ->
forall (s1 : Sort σ) (U : CarriersTermAlgebra C s1),
ExtendDRelTermAlgebra R T U -> ExtendDRelTermAlgebra R (c i0) U
s2: Sort σ
d: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
P2: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra R (c i0)
  (d (transport (fun v : Symbol σ => Arity (σ v)) 1 i0))
s3: Sort σ
u1: Symbol σ
c0: forall i0 : Arity (σ u1), CarriersTermAlgebra C (sorts_dom (σ u1) i0)
p3: u = u1
P3: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra R (d i0)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) p3 i0))
i: Arity (σ u)
ExtendDRelTermAlgebra R (c i)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) (1 @ p3) i))
      apply (h i _ (d i)).
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Transitive (R s)
u: Symbol σ
c: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
h: forall (i0 : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i0) T ->
forall (s1 : Sort σ) (U : CarriersTermAlgebra C s1),
ExtendDRelTermAlgebra R T U -> ExtendDRelTermAlgebra R (c i0) U
s2: Sort σ
d: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
P2: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra R (c i0)
  (d (transport (fun v : Symbol σ => Arity (σ v)) 1 i0))
s3: Sort σ
u1: Symbol σ
c0: forall i0 : Arity (σ u1), CarriersTermAlgebra C (sorts_dom (σ u1) i0)
p3: u = u1
P3: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra R (d i0)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) p3 i0))
i: Arity (σ u)
ExtendDRelTermAlgebra R (c i) (d i)
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Transitive (R s)
u: Symbol σ
c: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
h: forall (i0 : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i0) T ->
forall (s1 : Sort σ) (U : CarriersTermAlgebra C s1),
ExtendDRelTermAlgebra R T U -> ExtendDRelTermAlgebra R (c i0) U
s2: Sort σ
d: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
P2: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra R (c i0)
  (d (transport (fun v : Symbol σ => Arity (σ v)) 1 i0))
s3: Sort σ
u1: Symbol σ
c0: forall i0 : Arity (σ u1), CarriersTermAlgebra C (sorts_dom (σ u1) i0)
p3: u = u1
P3: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra R (d i0)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) p3 i0))
i: Arity (σ u)
ExtendDRelTermAlgebra R (d i)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) (1 @ p3) i))
      +
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Transitive (R s)
u: Symbol σ
c: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
h: forall (i0 : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i0) T ->
forall (s1 : Sort σ) (U : CarriersTermAlgebra C s1),
ExtendDRelTermAlgebra R T U -> ExtendDRelTermAlgebra R (c i0) U
s2: Sort σ
d: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
P2: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra R (c i0)
  (d (transport (fun v : Symbol σ => Arity (σ v)) 1 i0))
s3: Sort σ
u1: Symbol σ
c0: forall i0 : Arity (σ u1), CarriersTermAlgebra C (sorts_dom (σ u1) i0)
p3: u = u1
P3: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra R (d i0)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) p3 i0))
i: Arity (σ u)
ExtendDRelTermAlgebra R (c i) (d i) apply P2.
      +
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Transitive (R s)
u: Symbol σ
c: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
h: forall (i0 : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i0) T ->
forall (s1 : Sort σ) (U : CarriersTermAlgebra C s1),
ExtendDRelTermAlgebra R T U -> ExtendDRelTermAlgebra R (c i0) U
s2: Sort σ
d: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
P2: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra R (c i0)
  (d (transport (fun v : Symbol σ => Arity (σ v)) 1 i0))
s3: Sort σ
u1: Symbol σ
c0: forall i0 : Arity (σ u1), CarriersTermAlgebra C (sorts_dom (σ u1) i0)
p3: u = u1
P3: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra R (d i0)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) p3 i0))
i: Arity (σ u)
ExtendDRelTermAlgebra R (d i)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) (1 @ p3) i)) rewrite concat_1p.
H: Funext
σ: Signature
C: Carriers σ
R: forall s : Sort σ, Relation (C s)
H0: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
H1: forall s : Sort σ, Transitive (R s)
u: Symbol σ
c: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
h: forall (i0 : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra R (c i0) T ->
forall (s1 : Sort σ) (U : CarriersTermAlgebra C s1),
ExtendDRelTermAlgebra R T U -> ExtendDRelTermAlgebra R (c i0) U
s2: Sort σ
d: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
P2: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra R (c i0)
  (d (transport (fun v : Symbol σ => Arity (σ v)) 1 i0))
s3: Sort σ
u1: Symbol σ
c0: forall i0 : Arity (σ u1), CarriersTermAlgebra C (sorts_dom (σ u1) i0)
p3: u = u1
P3: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra R (d i0)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) p3 i0))
i: Arity (σ u)
ExtendDRelTermAlgebra R (d i)
  (c0 (transport (fun v : Symbol σ => Arity (σ v)) p3 i)) apply P3.
  Qed.

  #[export] Instance transitive_extend_rel_term_algebra
    `{!forall s, Transitive (R s)} {s : Sort σ}
    : Transitive (@ExtendRelTermAlgebra σ C R s).
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Transitive (R s0)
s: Sort σ
Transitive (ExtendRelTermAlgebra R)
  Proof.
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Transitive (R s0)
s: Sort σ
Transitive (ExtendRelTermAlgebra R)
    intros S T U.
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, Transitive (R s0)
s: Sort σ
S, T, U: CarriersTermAlgebra C s
ExtendRelTermAlgebra R S T ->
ExtendRelTermAlgebra R T U -> ExtendRelTermAlgebra R S U apply transitive_extend_drel_term_algebra.
  Defined.

  #[export] Instance equivrel_extend_rel_term_algebra
    `{!forall s, EquivRel (R s)} (s : Sort σ)
    : EquivRel (@ExtendRelTermAlgebra σ C R s).
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, EquivRel (R s0)
s: Sort σ
EquivRel (ExtendRelTermAlgebra R)
  Proof.
H: Funext
σ: Signature
C: Carriers σ
R: forall s0 : Sort σ, Relation (C s0)
H0: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
H1: forall s0 : Sort σ, EquivRel (R s0)
s: Sort σ
EquivRel (ExtendRelTermAlgebra R)
    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.

  #[export] Instance reflexive_extend_path_term_algebra
    : forall s : Sort σ, Reflexive (@ExtendPathTermAlgebra s).
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
forall s : Sort σ, Reflexive ExtendPathTermAlgebra
  Proof.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
forall s : Sort σ, Reflexive ExtendPathTermAlgebra
    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.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
S, T: CarriersTermAlgebra C s
p: S = T
ExtendPathTermAlgebra S T
  Proof.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
S, T: CarriersTermAlgebra C s
p: S = T
ExtendPathTermAlgebra S T
    induction p.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
S: CarriersTermAlgebra C s
ExtendPathTermAlgebra S S apply reflexive_extend_path_term_algebra.
  Defined.

  #[export] Instance symmetric_extend_path_term_algebra
    : forall s : Sort σ, Symmetric (@ExtendPathTermAlgebra s).
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
forall s : Sort σ, Symmetric ExtendPathTermAlgebra
  Proof.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
forall s : Sort σ, Symmetric ExtendPathTermAlgebra
    apply symmetric_extend_rel_term_algebra.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
forall s : Sort σ, Symmetric paths intros s x y.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
x, y: C s
x = y -> y = x exact inverse.
  Defined.

  #[export] Instance transitive_extend_path_term_algebra
    : forall s : Sort σ, Transitive (@ExtendPathTermAlgebra s).
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
forall s : Sort σ, Transitive ExtendPathTermAlgebra
  Proof.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
forall s : Sort σ, Transitive ExtendPathTermAlgebra
    apply transitive_extend_rel_term_algebra.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
forall s : Sort σ, Transitive paths intros s x y z.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
x, y, z: C s
x = y -> y = z -> x = z exact concat.
  Defined.

  #[export] Instance equivrel_extend_path_term_algebra
    : forall s : Sort σ, EquivRel (@ExtendPathTermAlgebra s).
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
forall s : Sort σ, EquivRel ExtendPathTermAlgebra
  Proof.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
forall s : Sort σ, EquivRel ExtendPathTermAlgebra
    constructor; exact _.
  Qed.

  #[export] Instance hprop_extend_path_term_algebra (s : Sort σ)
    : is_mere_relation (CarriersTermAlgebra C s) ExtendPathTermAlgebra.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
is_mere_relation (CarriersTermAlgebra C s) ExtendPathTermAlgebra
  Proof.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
is_mere_relation (CarriersTermAlgebra C s) ExtendPathTermAlgebra
    intros S T.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
S, T: CarriersTermAlgebra C s
IsHProp (ExtendPathTermAlgebra 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}.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
s1, s2: Sort σ
S: CarriersTermAlgebra C s1
T: CarriersTermAlgebra C s2
e: ExtendDRelTermAlgebra (fun s : Sort σ => paths) S T
{p : s1 = s2 & transport (CarriersTermAlgebra C) p S = T}
  Proof.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
s1, s2: Sort σ
S: CarriersTermAlgebra C s1
T: CarriersTermAlgebra C s2
e: ExtendDRelTermAlgebra (fun s : Sort σ => paths) S T
{p : s1 = s2 & transport (CarriersTermAlgebra C) p S = T}
    generalize dependent s2.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
s1: Sort σ
S: CarriersTermAlgebra C s1
forall (s2 : Sort σ) (T : CarriersTermAlgebra C s2),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) S T ->
{p : s1 = s2 & transport (CarriersTermAlgebra C) p S = T}
    induction S as [| u c h];
        intros s2 [? d | ? d] e;
        solve [elim e] || destruct e as [p e].
H: Funext
σ: Signature
C: Carriers σ
H0: forall s1 : Sort σ, IsHSet (C s1)
s: Sort σ
c: C s
s2, s0: Sort σ
d: C s0
p: s = s0
e: transport C p c = d
{p0 : s = s0 &
transport (CarriersTermAlgebra C) p0 (var_term_algebra C s c) =
var_term_algebra C s0 d}
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i) T ->
{p0 : sorts_dom (σ u) i = s0 &
transport (CarriersTermAlgebra C) p0 (c i) = T}
s2: Sort σ
u0: Symbol σ
d: forall i : Arity (σ u0), CarriersTermAlgebra C (sorts_dom (σ u0) i)
p: u = u0
e: forall i : Arity (σ u),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i)
  (d (transport (fun v : Symbol σ => Arity (σ v)) p i))
{p0 : sort_cod (σ u) = sort_cod (σ u0) &
transport (CarriersTermAlgebra C) p0 (ops_term_algebra C u c) =
ops_term_algebra C u0 d}
    -
H: Funext
σ: Signature
C: Carriers σ
H0: forall s1 : Sort σ, IsHSet (C s1)
s: Sort σ
c: C s
s2, s0: Sort σ
d: C s0
p: s = s0
e: transport C p c = d
{p0 : s = s0 &
transport (CarriersTermAlgebra C) p0 (var_term_algebra C s c) =
var_term_algebra C s0 d} exists p.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s1 : Sort σ, IsHSet (C s1)
s: Sort σ
c: C s
s2, s0: Sort σ
d: C s0
p: s = s0
e: transport C p c = d
transport (CarriersTermAlgebra C) p (var_term_algebra C s c) =
var_term_algebra C s0 d by induction p, e.
    -
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i) T ->
{p0 : sorts_dom (σ u) i = s0 &
transport (CarriersTermAlgebra C) p0 (c i) = T}
s2: Sort σ
u0: Symbol σ
d: forall i : Arity (σ u0), CarriersTermAlgebra C (sorts_dom (σ u0) i)
p: u = u0
e: forall i : Arity (σ u),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i)
  (d (transport (fun v : Symbol σ => Arity (σ v)) p i))
{p0 : sort_cod (σ u) = sort_cod (σ u0) &
transport (CarriersTermAlgebra C) p0 (ops_term_algebra C u c) =
ops_term_algebra C u0 d} induction p.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i) T ->
{p : sorts_dom (σ u) i = s0 & transport (CarriersTermAlgebra C) p (c i) = T}
s2: Sort σ
d: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
e: forall i : Arity (σ u),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i)
  (d (transport (fun v : Symbol σ => Arity (σ v)) 1 i))
{p : sort_cod (σ u) = sort_cod (σ u) &
transport (CarriersTermAlgebra C) p (ops_term_algebra C u c) =
ops_term_algebra C u d} exists idpath.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i) T ->
{p : sorts_dom (σ u) i = s0 & transport (CarriersTermAlgebra C) p (c i) = T}
s2: Sort σ
d: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
e: forall i : Arity (σ u),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i)
  (d (transport (fun v : Symbol σ => Arity (σ v)) 1 i))
transport (CarriersTermAlgebra C) 1 (ops_term_algebra C u c) =
ops_term_algebra C u d cbn.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i) T ->
{p : sorts_dom (σ u) i = s0 & transport (CarriersTermAlgebra C) p (c i) = T}
s2: Sort σ
d: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
e: forall i : Arity (σ u),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i)
  (d (transport (fun v : Symbol σ => Arity (σ v)) 1 i))
ops_term_algebra C u c = ops_term_algebra C u d f_ap.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i) T ->
{p : sorts_dom (σ u) i = s0 & transport (CarriersTermAlgebra C) p (c i) = T}
s2: Sort σ
d: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
e: forall i : Arity (σ u),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i)
  (d (transport (fun v : Symbol σ => Arity (σ v)) 1 i))
c = d funext a.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i) T ->
{p : sorts_dom (σ u) i = s0 & transport (CarriersTermAlgebra C) p (c i) = T}
s2: Sort σ
d: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
e: forall i : Arity (σ u),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i)
  (d (transport (fun v : Symbol σ => Arity (σ v)) 1 i))
a: Arity (σ u)
c a = d a
      destruct (h a _ (d a) (e a)) as [p q].
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall (i : Arity (σ u)) (s0 : Sort σ) (T : CarriersTermAlgebra C s0),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i) T ->
{p0 : sorts_dom (σ u) i = s0 &
transport (CarriersTermAlgebra C) p0 (c i) = T}
s2: Sort σ
d: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
e: forall i : Arity (σ u),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (c i)
  (d (transport (fun v : Symbol σ => Arity (σ v)) 1 i))
a: Arity (σ u)
p: sorts_dom (σ u) a = sorts_dom (σ u) a
q: transport (CarriersTermAlgebra C) p (c a) = d a
c a = d a
      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.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
S, T: CarriersTermAlgebra C s
e: ExtendPathTermAlgebra S T
S = T
  Proof.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
S, T: CarriersTermAlgebra C s
e: ExtendPathTermAlgebra S T
S = T
    destruct (dependent_path_extend_path_term_algebra S T e) as [p q].
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
S, T: CarriersTermAlgebra C s
e: ExtendPathTermAlgebra S T
p: s = s
q: transport (CarriersTermAlgebra C) p S = T
S = T
    by induction (hset_path2 idpath p).
  Defined.

  #[export] Instance hset_carriers_term_algebra (s : Sort σ)
    : IsHSet (CarriersTermAlgebra C s).
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
IsHSet (CarriersTermAlgebra C s)
  Proof.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
IsHSet (CarriersTermAlgebra C s)
    apply (@ishset_hrel_subpaths _ ExtendPathTermAlgebra).
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
Reflexive ExtendPathTermAlgebra
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
is_mere_relation (CarriersTermAlgebra C s) ExtendPathTermAlgebra
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
forall x y : CarriersTermAlgebra C s, ExtendPathTermAlgebra x y -> x = y
    -
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
Reflexive ExtendPathTermAlgebra apply reflexive_extend_path_term_algebra.
    -
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
is_mere_relation (CarriersTermAlgebra C s) ExtendPathTermAlgebra apply hprop_extend_path_term_algebra; exact _.
    -
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
s: Sort σ
forall x y : CarriersTermAlgebra C s, ExtendPathTermAlgebra x y -> x = y exact 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.
σ: Signature
C: Carriers σ
s: Sort σ
x, y: C s
var_term_algebra C s x = var_term_algebra C s y -> x = y
Proof.
σ: Signature
C: Carriers σ
s: Sort σ
x, y: C s
var_term_algebra C s x = var_term_algebra C s y -> x = y
  intro p.
σ: Signature
C: Carriers σ
s: Sort σ
x, y: C s
p: var_term_algebra C s x = var_term_algebra C s y
x = y
  apply reflexive_extend_path_term_algebra_path in p.
σ: Signature
C: Carriers σ
s: Sort σ
x, y: C s
p: ExtendPathTermAlgebra (var_term_algebra C s x) (var_term_algebra C s y)
x = y
  destruct p as [p1 p2].
σ: Signature
C: Carriers σ
s: Sort σ
x, y: C s
p1: s = s
p2: transport C p1 x = y
x = y
  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.
H: Funext
σ: Signature
C: Carriers σ
u: Symbol σ
a, b: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
ops_term_algebra C u a = ops_term_algebra C u b -> a = b
Proof.
H: Funext
σ: Signature
C: Carriers σ
u: Symbol σ
a, b: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
ops_term_algebra C u a = ops_term_algebra C u b -> a = b
  intro p.
H: Funext
σ: Signature
C: Carriers σ
u: Symbol σ
a, b: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
p: ops_term_algebra C u a = ops_term_algebra C u b
a = b
  apply reflexive_extend_path_term_algebra_path in p.
H: Funext
σ: Signature
C: Carriers σ
u: Symbol σ
a, b: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
p: ExtendPathTermAlgebra (ops_term_algebra C u a) (ops_term_algebra C u b)
a = b
  destruct p as [p1 p2].
H: Funext
σ: Signature
C: Carriers σ
u: Symbol σ
a, b: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
p1: u = u
p2: forall i : Arity (σ u),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (a i)
  (b (transport (fun v : Symbol σ => Arity (σ v)) p1 i))
a = b
  destruct (hset_path2 p1 idpath)^.
H: Funext
σ: Signature
C: Carriers σ
u: Symbol σ
a, b: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
p2: forall i : Arity (σ u),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (a i)
  (b (transport (fun v : Symbol σ => Arity (σ v)) 1 i))
a = b
  funext i.
H: Funext
σ: Signature
C: Carriers σ
u: Symbol σ
a, b: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
p2: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (a i0)
  (b (transport (fun v : Symbol σ => Arity (σ v)) 1 i0))
i: Arity (σ u)
a i = b i
  apply path_extend_path_term_algebra.
H: Funext
σ: Signature
C: Carriers σ
u: Symbol σ
a, b: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
p2: forall i0 : Arity (σ u),
ExtendDRelTermAlgebra (fun s : Sort σ => paths) (a i0)
  (b (transport (fun v : Symbol σ => Arity (σ v)) 1 i0))
i: Arity (σ u)
ExtendPathTermAlgebra (a i) (b i)
  apply p2.
Qed.

(** The extension [ExtendRelTermAlgebra R], of a family of mere
    equivalence relations [R], is a congruence. *)

#[export] 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).
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
R: forall s : Sort σ, Relation (C s)
H1: forall s : Sort σ, EquivRel (R s)
H2: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
IsCongruence (TermAlgebra C) (@ExtendRelTermAlgebra σ C R)
Proof.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
R: forall s : Sort σ, Relation (C s)
H1: forall s : Sort σ, EquivRel (R s)
H2: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
IsCongruence (TermAlgebra C) (@ExtendRelTermAlgebra σ C R)
  constructor.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
R: forall s : Sort σ, Relation (C s)
H1: forall s : Sort σ, EquivRel (R s)
H2: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
forall (s : Sort σ) (x y : TermAlgebra C s),
IsHProp (ExtendRelTermAlgebra R x y)
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
R: forall s : Sort σ, Relation (C s)
H1: forall s : Sort σ, EquivRel (R s)
H2: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
forall s : Sort σ, EquivRel (ExtendRelTermAlgebra R)
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
R: forall s : Sort σ, Relation (C s)
H1: forall s : Sort σ, EquivRel (R s)
H2: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
OpsCompatible (TermAlgebra C) (@ExtendRelTermAlgebra σ C R)
  -
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
R: forall s : Sort σ, Relation (C s)
H1: forall s : Sort σ, EquivRel (R s)
H2: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
forall (s : Sort σ) (x y : TermAlgebra C s),
IsHProp (ExtendRelTermAlgebra R x y) intros.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
R: forall s0 : Sort σ, Relation (C s0)
H1: forall s0 : Sort σ, EquivRel (R s0)
H2: forall (s0 : Sort σ) (x0 y0 : C s0), IsHProp (R s0 x0 y0)
s: Sort σ
x, y: TermAlgebra C s
IsHProp (ExtendRelTermAlgebra R x y) exact _.
  -
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
R: forall s : Sort σ, Relation (C s)
H1: forall s : Sort σ, EquivRel (R s)
H2: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
forall s : Sort σ, EquivRel (ExtendRelTermAlgebra R) intros.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
R: forall s0 : Sort σ, Relation (C s0)
H1: forall s0 : Sort σ, EquivRel (R s0)
H2: forall (s0 : Sort σ) (x y : C s0), IsHProp (R s0 x y)
s: Sort σ
EquivRel (ExtendRelTermAlgebra R) exact _.
  -
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
R: forall s : Sort σ, Relation (C s)
H1: forall s : Sort σ, EquivRel (R s)
H2: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
OpsCompatible (TermAlgebra C) (@ExtendRelTermAlgebra σ C R) intros u a b c.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
R: forall s : Sort σ, Relation (C s)
H1: forall s : Sort σ, EquivRel (R s)
H2: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
u: Symbol σ
a, b: forall i : Arity (σ u), TermAlgebra C (sorts_dom (σ u) i)
c: forall i : Arity (σ u), ExtendRelTermAlgebra R (a i) (b i)
ExtendRelTermAlgebra R (u.#(TermAlgebra C) a) (u.#(TermAlgebra C) b) exists idpath.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
R: forall s : Sort σ, Relation (C s)
H1: forall s : Sort σ, EquivRel (R s)
H2: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
u: Symbol σ
a, b: forall i : Arity (σ u), TermAlgebra C (sorts_dom (σ u) i)
c: forall i : Arity (σ u), ExtendRelTermAlgebra R (a i) (b i)
forall i : Arity (σ u),
ExtendDRelTermAlgebra R (a i)
  (b (transport (fun v : Symbol σ => Arity (σ v)) 1 i)) intro i.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
R: forall s : Sort σ, Relation (C s)
H1: forall s : Sort σ, EquivRel (R s)
H2: forall (s : Sort σ) (x y : C s), IsHProp (R s x y)
u: Symbol σ
a, b: forall i0 : Arity (σ u), TermAlgebra C (sorts_dom (σ u) i0)
c: forall i0 : Arity (σ u), ExtendRelTermAlgebra R (a i0) (b i0)
i: Arity (σ u)
ExtendDRelTermAlgebra R (a i)
  (b (transport (fun v : Symbol σ => Arity (σ v)) 1 i)) apply c.
Defined.

(** Given and family of functions [f : forall s, C s -> A s], we can extend it to a [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.

  #[export] Instance is_homomorphism_map_term_algebra
    : @IsHomomorphism σ (TermAlgebra C) A (map_term_algebra A f).
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
f: forall s : Sort σ, C s -> A s
IsHomomorphism (map_term_algebra A f)
  Proof.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
f: forall s : Sort σ, C s -> A s
IsHomomorphism (map_term_algebra A f)
    intros u a.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
f: forall s : Sort σ, C s -> A s
u: Symbol σ
a: forall i : Arity (σ u), TermAlgebra C (sorts_dom (σ u) i)
map_term_algebra A f (sort_cod (σ u)) (u.#(TermAlgebra C) a) =
u.#A (fun i : Arity (σ u) => map_term_algebra A f (sorts_dom (σ u) i) (a i)) by refine (ap u.#A _).
  Qed.

  Definition hom_term_algebra : 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 : 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 : TermAlgebra C $-> A),
      hom_term_algebra A (precomp_var_term_algebra f) = f.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
forall f : TermAlgebra C $-> A,
hom_term_algebra A (precomp_var_term_algebra f) = f
  Proof.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
forall f : TermAlgebra C $-> A,
hom_term_algebra A (precomp_var_term_algebra f) = f
    intro f.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
f: TermAlgebra C $-> A
hom_term_algebra A (precomp_var_term_algebra f) = f
    apply path_homomorphism.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
f: TermAlgebra C $-> A
hom_term_algebra A (precomp_var_term_algebra f) = f
    funext s T.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
A: Algebra σ
f: TermAlgebra C $-> A
s: Sort σ
T: TermAlgebra C s
hom_term_algebra A (precomp_var_term_algebra f) s T = f s T
    induction T as [|u c h].
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
A: Algebra σ
f: TermAlgebra C $-> A
s: Sort σ
c: C s
hom_term_algebra A (precomp_var_term_algebra f) s (var_term_algebra C s c) =
f s (var_term_algebra C s c)
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
f: TermAlgebra C $-> A
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall i : Arity (σ u),
hom_term_algebra A (precomp_var_term_algebra f) (sorts_dom (σ u) i) (c i) =
f (sorts_dom (σ u) i) (c i)
hom_term_algebra A (precomp_var_term_algebra f) (sort_cod (σ u))
  (ops_term_algebra C u c) =
f (sort_cod (σ u)) (ops_term_algebra C u c)
    -
H: Funext
σ: Signature
C: Carriers σ
H0: forall s0 : Sort σ, IsHSet (C s0)
A: Algebra σ
f: TermAlgebra C $-> A
s: Sort σ
c: C s
hom_term_algebra A (precomp_var_term_algebra f) s (var_term_algebra C s c) =
f s (var_term_algebra C s c) reflexivity.
    -
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
f: TermAlgebra C $-> A
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall i : Arity (σ u),
hom_term_algebra A (precomp_var_term_algebra f) (sorts_dom (σ u) i) (c i) =
f (sorts_dom (σ u) i) (c i)
hom_term_algebra A (precomp_var_term_algebra f) (sort_cod (σ u))
  (ops_term_algebra C u c) =
f (sort_cod (σ u)) (ops_term_algebra C u c) refine (_ @ (is_homomorphism f u c)^).
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
f: TermAlgebra C $-> A
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall i : Arity (σ u),
hom_term_algebra A (precomp_var_term_algebra f) (sorts_dom (σ u) i) (c i) =
f (sorts_dom (σ u) i) (c i)
hom_term_algebra A (precomp_var_term_algebra f) (sort_cod (σ u))
  (ops_term_algebra C u c) =
u.#A (fun i : Arity (σ u) => f (sorts_dom (σ u) i) (c i))
      refine (ap u.#A _).
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
f: TermAlgebra C $-> A
u: Symbol σ
c: forall i : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i)
h: forall i : Arity (σ u),
hom_term_algebra A (precomp_var_term_algebra f) (sorts_dom (σ u) i) (c i) =
f (sorts_dom (σ u) i) (c i)
(fun i : Arity (σ u) =>
 (fix F (s : Sort σ) (c0 : CarriersTermAlgebra C s) {struct c0} : A s :=
    match c0 in (CarriersTermAlgebra _ s0) return (A s0) with
    | @var_term_algebra _ _ s0 y => precomp_var_term_algebra f s0 y
    | @ops_term_algebra _ _ u0 c1 =>
        u0.#A (fun i0 : Arity (σ u0) => F (sorts_dom (σ u0) i0) (c1 i0))
    end)
   (sorts_dom (σ u) i) (c i)) =
(fun i : Arity (σ u) => f (sorts_dom (σ u) i) (c i)) funext i.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
f: TermAlgebra C $-> A
u: Symbol σ
c: forall i0 : Arity (σ u), CarriersTermAlgebra C (sorts_dom (σ u) i0)
h: forall i0 : Arity (σ u),
hom_term_algebra A (precomp_var_term_algebra f) (sorts_dom (σ u) i0) (c i0) =
f (sorts_dom (σ u) i0) (c i0)
i: Arity (σ u)
(fix F (s : Sort σ) (c0 : CarriersTermAlgebra C s) {struct c0} : A s :=
   match c0 in (CarriersTermAlgebra _ s0) return (A s0) with
   | @var_term_algebra _ _ s0 y => precomp_var_term_algebra f s0 y
   | @ops_term_algebra _ _ u0 c1 =>
       u0.#A (fun i0 : Arity (σ u0) => F (sorts_dom (σ u0) i0) (c1 i0))
   end)
  (sorts_dom (σ u) i) (c i) =
f (sorts_dom (σ u) i) (c 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.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
forall f : forall s : Sort σ, C s -> A s,
precomp_var_term_algebra (hom_term_algebra A f) = f
  Proof.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
forall f : forall s : Sort σ, C s -> A s,
precomp_var_term_algebra (hom_term_algebra A f) = f
    intro f.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
f: forall s : Sort σ, C s -> A s
precomp_var_term_algebra (hom_term_algebra A f) = f by funext s a.
  Defined.

  (** Precomposition with [var_term_algebra] is an equivalence *)

  #[export] Instance isequiv_precomp_var_term_algebra
    : IsEquiv precomp_var_term_algebra.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
IsEquiv precomp_var_term_algebra
  Proof.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
IsEquiv precomp_var_term_algebra
    srapply isequiv_adjointify.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
(forall s : Sort σ, C s -> A s) -> TermAlgebra C $-> A
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
precomp_var_term_algebra o ?g == idmap
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
?g o precomp_var_term_algebra == idmap
    -
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
(forall s : Sort σ, C s -> A s) -> TermAlgebra C $-> A apply hom_term_algebra.
    -
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
precomp_var_term_algebra o hom_term_algebra A == idmap intro.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
x: forall s : Sort σ, C s -> A s
precomp_var_term_algebra (hom_term_algebra A x) = x apply path_hom_term_algebra_to_precomp_var_term_algebra.
    -
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
hom_term_algebra A o precomp_var_term_algebra == idmap intro.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
x: TermAlgebra C $-> A
hom_term_algebra A (precomp_var_term_algebra x) = x 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
    : (TermAlgebra C $-> A) <~> (forall s, C s -> A s).
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
(TermAlgebra C $-> A) <~> (forall s : Sort σ, C s -> A s)
  Proof.
H: Funext
σ: Signature
C: Carriers σ
H0: forall s : Sort σ, IsHSet (C s)
A: Algebra σ
(TermAlgebra C $-> A) <~> (forall s : Sort σ, C s -> A s)
    exact (Build_Equiv _ _ precomp_var_term_algebra _).
  Defined.

End ump_term_algebra.