theory.ua_subalgebraT

Require Import
  RelationClasses
  universal_algebra ua_homomorphisms theory.categories abstract_algebra.
Require
  categories.algebras.

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


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

  Definition op_closed_proper:
    (Pproper: s x x', x = x' iffT (P s x) (P s x')) o,
    x x', x = x' iffT (@op_closed o x) (@op_closed o x').

  Class ClosedSubset: Type :=
    { subset_proper: s x x', x = x' iffT (P s x) (P s x')
    ; subset_closed: o, op_closed (algebra_op o) }.


  Context `{ClosedSubset}.


  Definition carrier s := sigT (P s).

  Hint Unfold carrier: typeclass_instances.


  Fixpoint close_op {d}: (o: op_type A d), op_closed o op_type carrier d :=
    match d with
    | ne_list.one _ => λ o c, existT _ o (c)
    | ne_list.cons _ _ => λ o c X, close_op (o (projT1 X)) (c (projT1 X) (projT2 X))
    end.

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

  Instance: d, Equiv (op_type carrier d).
  Defined.

  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.
End subalgebras.

Hint Unfold carrier: typeclass_instances.