Require Import
  universal_algebra ua_homomorphisms canonical_names theory.categories abstract_algebra.
  categories.algebras forget_algebra.

Section subalgebras.
  Context `{Algebra sign A} (P: s, A s Prop).

  Fixpoint op_closed {o: OpType (sorts sign)}: op_type A o Prop :=
    match o with
    | x => P x
    | ne_list.cons _ _ => λ d, z, P _ z op_closed (d z)

  Global Instance op_closed_proper: `{∀ s, Proper ((=) ==> iff) (P s)} o, Proper ((=) ==> iff) (@op_closed o).

  Class ClosedSubset: Prop :=
    { subset_proper:> s, Proper ((=) ==> iff) (P s)
    ; subset_closed: o, op_closed (algebra_op o) }.

  Context `{ClosedSubset}.

  Definition carrier s := sig (P s).

  Hint Unfold carrier: typeclass_instances.

  Program Fixpoint close_op {d}: (o: op_type A d), op_closed o op_type carrier d :=
    match d with
    | _ => λ o c, exist _ o (c)
    | ne_list.cons _ _ => λ o c X, close_op (o X) (c X (proj2_sig X))

  Global Instance impl: AlgebraOps sign carrier := λ o, close_op (algebra_op o) (subset_closed o).

  Definition close_op_proper d (o0 o1: op_type A d)
    (P': op_closed o0) (Q: op_closed o1): o0 = o1 close_op o0 P' = close_op o1 Q.

  Global Instance subalgebra: Algebra sign carrier.

  Definition proj s := @proj1_sig (A s) (P s).

  Global Instance: HomoMorphism sign carrier A proj.

  Instance: Injective (proj i).

  Global Instance: Mono (algebras.arrow _ proj).
End subalgebras.

Hint Extern 10 (Equiv (carrier _ _)) => apply @sig_equiv : typeclass_instances.