Require Import UniMath.Foundations.All.

Require Export UniMath.Algebra.Universal.Algebras.
Require Export UniMath.Algebra.Universal.Terms.

Local Open Scope sorted.
Local Open Scope hom.

Section TermAlgebra.

  Definition term_algebra (σ: signature): algebra σ
    := make_algebra (gterm σ) build_gterm.

  Definition has_supportsets_termalgebra (σ: signature): has_supportsets (term_algebra σ)
    := λ (s: sorts σ), isasetterm s.

  Definition term_hSetalgebra (σ: signature): hSetalgebra σ
    := make_hSetalgebra (has_supportsets_termalgebra σ).

  Context {σ: signature}.

  Definition geval (a: algebra σ): term_algebra σ s→ a
    := @fromgterm σ a (ops a).

  Lemma gevalstep {a: algebra σ} (nm: names σ) (v: (gterm σ)⋆ (arity nm))
    : geval a _ (build_gterm nm v) = ops a nm (h1map (geval a) v).
  Proof.
    unfold geval.
    apply fromtermstep.
  Defined.

  Lemma ishomgeval (a: algebra σ): ishom (geval a).
  Proof.
    red.
    intros.
    unfold starfun.
    apply gevalstep.
  Defined.

  Definition gevalhom (a: algebra σ): term_algebra σ ↷ a
    := make_hom (ishomgeval a).

  Lemma gevalhom_is_unique {a: algebra σ} (f: term_algebra σ ↷ a):
    pr1 f = pr1 (gevalhom a).
  Proof.
    induction f as [f fishom].
    apply funextsec.
    intro s.
    apply funextfun.
    intro t.
    apply (term_ind (λ s t, f s t = geval a s t)).
    unfold term_ind_HP.
    intros.
    change (build_gterm nm v) with (ops (term_algebra σ) nm v) at 1.
    rewrite fishom.
    rewrite gevalstep.
    apply maponpaths.
    unfold starfun.
    apply h1map_path.
    exact IH.
  Qed.

  Definition iscontrhomsfromgterm (a: algebra σ) (setprop: has_supportsets a)
    : iscontr (term_algebra σ ↷ a).
  Proof.
    exists (gevalhom a).
    intro f.
    apply subtypePairEquality'.
    - apply gevalhom_is_unique.
    - apply isapropishom.
      exact setprop.
  Defined.

End TermAlgebra.