free_lattice.v

(* The goal of this file is to define the free bounded distributive lattice
   on a set of generators, subject to some equations and inequations.
   To do so, we first define the signature for distributive lattices,
   then its equational theory, and show that any model of this
   equational theory yield an instance of [IsBoundedDistributiveLattice].
   We introduce the notion of a presentation of a bounded distributive
   lattice and obtain free objects by interpreting such a presentation
   as an extension of the equational theory of distributive lattices.
   We use these tools to define the presentation of the underlying
   distributive lattice of the Spectrum of a ring as presented in
   (Coquand-Lombardi-Schuster09).
 *)

Require Import
  HoTT.Spaces.Finite
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Algebra.UniversalAlgebra.ua_algebra
  HoTT.Algebra.UniversalAlgebra.ua_algebraic_theory
  HoTT.Algebra.UniversalAlgebra.ua_free_algebra.


(** helper functions to manipulate finite sets *)

Definition Fin1_rec {P : Type} (p : P) : Fin 1 -> P :=
  fun x => match x with inr tt => p | inl z => Empty_rec P z end.

Definition Fin1_ind {P : Fin 1 -> Type} (p : P (inr tt)) (x : Fin 1) : P x :=
  match x with inr tt => p | inl z => Empty_rec _ z end.

Definition Fin2_rec {P : Type} (p1 p2 : P) (x : Fin 2) : P :=
  match x with
  | inl x => Fin1_rec p1 x
  | inr tt => p2
  end.

Definition Fin3_rec {P : Type} (p1 p2 p3 : P) (x : Fin 3) : P :=
  match x with
  | inl x => Fin2_rec p1 p2 x
  | inr tt => p3
  end.

(** Special case of single sorted signature *)

Record SingleSortedSignature :=
  Build_SingleSortedSignature
    { SymbolT : Type
    ; hset_SymbolT : IsHSet SymbolT
    ; arity : SymbolT -> Type }.

Definition from_SingleSortedSignature (σ : SingleSortedSignature)
  : Signature :=
  let arity (s : SymbolT σ) := Build_SymbolTypeTo (arity σ s) (fun _ => inr tt) (inr tt) in
  Build_Signature (Fin 1) (SymbolT σ) arity _ (hset_SymbolT σ).


Definition constant (σ : SingleSortedSignature) :=
  { op : SymbolT σ & arity σ op <~> Fin 0 }.

Definition binop (σ : SingleSortedSignature) :=
  { op : SymbolT σ & arity σ op <~> Fin 2 }.


Definition SingleSortedCarrier {σ : SingleSortedSignature} (c : Type)
  : Carriers (from_SingleSortedSignature σ) := Fin1_rec c.

Definition SingleSortedTermAlgebra (σ : SingleSortedSignature) (ctx : Type) :=
  @CarriersTermAlgebra (from_SingleSortedSignature σ)
                       (SingleSortedCarrier ctx)
                       (inr tt).

(* helper functions to build single sorted terms *)
Definition ops_ssta {σ} (c : Type) (op : SymbolT σ) (k : arity σ op -> SingleSortedTermAlgebra σ c) : SingleSortedTermAlgebra σ c :=
  @ops_term_algebra (from_SingleSortedSignature σ)
                    (SingleSortedCarrier c) op k.

Definition var_ssta {σ} {c : Type} (x : c) : SingleSortedTermAlgebra σ c :=
  @var_term_algebra (from_SingleSortedSignature σ)
                    (SingleSortedCarrier c)
                    (inr tt) x.

Definition apply_binop {σ c} (op : binop σ) (t1 t2 : SingleSortedTermAlgebra σ c) : SingleSortedTermAlgebra σ c :=
  ops_ssta _ op.1 (Fin2_rec t1 t2 o op.2).

Definition apply_constant {σ c} (x : constant σ) : SingleSortedTermAlgebra σ c
  := ops_ssta _ x.1 (Empty_rec _ o x.2).

Record SingleSortedEquation {σ : SingleSortedSignature} :=
  Build_SingleSortedEquation
    { sse_ctx : Type
    ; sse_hset_ctx : IsHSet sse_ctx
    ; sse_lhs : SingleSortedTermAlgebra σ sse_ctx
    ; sse_rhs : SingleSortedTermAlgebra σ sse_ctx }.

Arguments SingleSortedEquation _ : clear implicits.

Definition from_SingleSortedEquation {σ} (e : SingleSortedEquation σ)
  : Equation (from_SingleSortedSignature σ) :=
  @Build_Equation _
    (SingleSortedCarrier (sse_ctx e))
    (ltac:(intros [[]|[]]; exact (sse_hset_ctx e)))
    (inr tt)
    (sse_lhs e)
    (sse_rhs e).

Definition SSAlgebra σ := Algebra (from_SingleSortedSignature σ).


(** Signature of lattices *)

Notation top_idx := (inr tt).
Notation bot_idx := (inl (inr tt)).
Notation meet_idx := (inl (inl (inr tt))).
Notation join_idx := (inl (inl (inl (inr tt)))).

Definition distr_lattice_arity (n : Fin 4) : Type :=
  match n with
  | top_idx => Fin 0 (* top *)
  | bot_idx => Fin 0 (* bottom *)
  | meet_idx => Fin 2 (* meet *)
  | join_idx => Fin 2 (* join *)
  | inl (inl (inl (inl x))) => Empty_rec _ x
  end.

Definition distr_lattice_sssignature :=
  Build_SingleSortedSignature (Fin 4) _ distr_lattice_arity.

Definition distributive_lattice_signature :=
  from_SingleSortedSignature distr_lattice_sssignature.



(** Definition of the properties on operations found in
    [HoTT.Classes.interfaces.canonical_names] as (single sorted) equations *)

Ltac vars0 k s c f :=
  match k with
  | S O => let x := eval cbv in (f (inr tt)) in exact (@var_ssta s c x)
  | S ?n =>
    let f' := constr:(fun (x : Fin n) => f (inl x)) in
    let z :=
      let x := eval cbv in (f (inr tt)) in
      constr:(@var_ssta s c x)
    in refine ((_, z)) ; vars0 n%nat s c f'
  end.

(* given a natural k > 1 and a single sorted signature, generates
   the elements of Fin k as ( .. (1, 2) .. k) *)
Ltac vars k s := vars0 k%nat s (Fin k) (fun (x : Fin k) => x).


Definition commutative (σ : SingleSortedSignature) (op : binop σ)
  : SingleSortedEquation σ :=
  Build_SingleSortedEquation σ (Fin 2) _
    (ops_ssta _ op.1 (var_ssta o op.2))
    (ops_ssta _ op.1 (var_ssta o (fin_transpose_last_two 0) o op.2)).

Definition idempotent (σ : SingleSortedSignature) (op : binop σ)
  : SingleSortedEquation σ :=
  Build_SingleSortedEquation σ (Fin 1) _
                             (ops_ssta _ op.1 (fun _ => var_ssta (inr tt)))
                             (var_ssta (inr tt)).

Definition leftIdentity (σ : SingleSortedSignature) (op : binop σ) (u : constant σ) : SingleSortedEquation σ :=
  let x := var_ssta (inr tt) in
  let lhs := apply_binop op (apply_constant u) x in
  Build_SingleSortedEquation σ (Fin 1) _ lhs x.

Definition rightIdentity (σ : SingleSortedSignature) (op : binop σ) (u : constant σ) : SingleSortedEquation σ :=
  let x := var_ssta (inr tt) in
  let lhs := apply_binop op x (apply_constant u) in
  Build_SingleSortedEquation σ (Fin 1) _ lhs x.

Definition associativity (σ : SingleSortedSignature) (op : binop σ)
  : SingleSortedEquation σ :=
  let '((x , y) , z) := ltac:(vars 3%nat σ) in
  let op' := apply_binop op in
  let lhs := op' x (op' y z) in
  let rhs := op' (op' x y) z in
  Build_SingleSortedEquation σ (Fin 3) _ lhs rhs.


Definition absorption (σ : SingleSortedSignature) (op1 op2 : binop σ)
  : SingleSortedEquation σ :=
  let '(x, y) := ltac:(vars 2%nat σ) in
  let op'1 := apply_binop op1 in
  let op'2 := apply_binop op2 in
  Build_SingleSortedEquation σ (Fin 2) _ (op'1 x (op'2 x y)) x.

Definition leftDistribute (σ : SingleSortedSignature) (op1 op2 : binop σ)
  : SingleSortedEquation σ :=
  let '((a , b), c) := ltac:(vars 3%nat σ) in
  let f := apply_binop op1 in
  let g := apply_binop op2 in
  Build_SingleSortedEquation σ (Fin 3) _ (f a (g b c)) (g (f a b) (f a c)).

Definition rightDistribute (σ : SingleSortedSignature) (op1 op2 : binop σ)
  : SingleSortedEquation σ :=
  let '((a , b), c) := ltac:(vars 3%nat σ) in
  let f := apply_binop op1 in
  let g := apply_binop op2 in
  Build_SingleSortedEquation σ (Fin 3) _ (f (g a b) c) (g (f a c) (f b c)).


Definition is_associative {σ} {I : Type} (e : Equations (from_SingleSortedSignature σ) I) (op : binop σ) :=
  { i : I & e i = from_SingleSortedEquation (associativity σ op) }.

Definition is_leftIdentity {σ} {I : Type} (e : Equations (from_SingleSortedSignature σ) I) (op : binop σ) (c : constant σ) :=
  { i : I & e i = from_SingleSortedEquation (leftIdentity σ op c) }.

Definition is_rightIdentity {σ} {I : Type} (e : Equations (from_SingleSortedSignature σ) I) (op : binop σ) (c : constant σ) :=
  { i : I & e i = from_SingleSortedEquation (rightIdentity σ op c) }.

Definition is_commutative {σ} {I : Type} (e : Equations (from_SingleSortedSignature σ) I) (op : binop σ) :=
  { i : I & e i = from_SingleSortedEquation (commutative σ op) }.

Definition is_idempotent {σ} {I : Type} (e : Equations (from_SingleSortedSignature σ) I) (op : binop σ) :=
  { i : I & e i = from_SingleSortedEquation (idempotent σ op) }.

Definition is_absorbing {σ} {I : Type} (e : Equations (from_SingleSortedSignature σ) I) (op1 op2 : binop σ) :=
  { i : I & e i = from_SingleSortedEquation (absorption σ op1 op2) }.

Definition is_leftDistributive {σ} {I : Type} (e : Equations (from_SingleSortedSignature σ) I) (op1 op2 : binop σ) :=
  { i : I & e i = from_SingleSortedEquation (leftDistribute σ op1 op2) }.


(** (Partial) Correspondance with the algebraic hierarchy in
    [HoTT.Classes.interfaces.abstract_algebra] *)

Import algebra_notations.

Definition SgOp_from_sssig {σ} (op : binop σ) (A : SSAlgebra σ)
  : SgOp (A (inr tt)) := fun x y => (op.1 ^^ A) (Fin2_rec x y o op.2).

Definition MonUnit_from_sssig {σ} (c : constant σ) (A : SSAlgebra σ)
  : MonUnit (A (inr tt)) := (c.1 ^^ A) (fun x => Empty_rec _ (c.2 x)).

(* destruct completely a term of type Fin k *)
Ltac caseFin x :=
  let t := type of x in
  lazymatch t with
  | Fin O => destruct x
  | Fin (S ?k) =>
    let x' := fresh "x" in
    destruct x as [x'|[]] ; [caseFin x'|]
  end.

Section ToAlgebraicHierarchy.
  Context `{Funext} {σ} (A : AlgebraicTheory (from_SingleSortedSignature σ)).

  Notation eqsA := (equations_algebraic_theory _ A).
  Notation A0 := (A (inr tt)).
  Notation SgOpA op := (SgOp_from_sssig op A).
  Notation MonUnitA u := (MonUnit_from_sssig u A).
  Notation interpA := (is_algebraic_algebraic_theory _ A).

  Definition to_SemiGroup (op : binop σ) (assoc : is_associative eqsA op)
    : @IsSemiGroup A0 (SgOpA op).
  Proof.
    constructor.
    - apply hset_algebra.
    - intros x y z.
      pose (ass := interpA assoc.1); rewrite assoc.2 in ass.
      specialize (ass (Fin1_ind (Fin3_rec x y z))).
      etransitivity; [| etransitivity; [exact ass|]];
      unfold sg_op, SgOp_from_sssig; cbn;
      apply ap ; funext i; caseFin (op.2 i); try reflexivity;
      simpl; clear i; apply ap ; funext i;
      caseFin (op.2 i) ; reflexivity.
  Defined.

  Definition to_Monoid (op : binop σ) (u : constant σ)
             (assoc : is_associative eqsA op)
             (lidentity : is_leftIdentity eqsA op u)
             (ridentity : is_rightIdentity eqsA op u)
             : @IsMonoid A0 (SgOpA op) (MonUnitA u).
  Proof.
    constructor; [apply to_SemiGroup; assumption|..].
    - intro x.
      pose (lid := interpA lidentity.1); rewrite lidentity.2 in lid.
      specialize (lid (Fin1_ind (Fin1_rec x))).
      etransitivity; [| exact lid];
      unfold sg_op, SgOp_from_sssig; cbn.
      apply ap ; funext i; caseFin (op.2 i); try reflexivity.
      unfold mon_unit, MonUnit_from_sssig; cbn; clear i.
      apply ap ; funext i; caseFin (u.2 i); reflexivity.
    - intro x.
      pose (rid := interpA ridentity.1); rewrite ridentity.2 in rid.
      specialize (rid (Fin1_ind (Fin1_rec x))).
      etransitivity; [| exact rid];
      unfold sg_op, SgOp_from_sssig; cbn.
      apply ap ; funext i; caseFin (op.2 i); try reflexivity.
      unfold mon_unit, MonUnit_from_sssig; cbn; clear i.
      apply ap ; funext i; caseFin (u.2 i); reflexivity.
  Defined.

  Definition to_CommutativeMonoid (op : binop σ) (u : constant σ)
             (assoc : is_associative eqsA op)
             (lidentity : is_leftIdentity eqsA op u)
             (ridentity : is_rightIdentity eqsA op u)
             (commutative : is_commutative eqsA op)
             : @IsCommutativeMonoid A0 (SgOpA op) (MonUnitA u).
  Proof.
    constructor; [apply to_Monoid; assumption|].
    intros x y;
    pose (comm := interpA commutative.1); rewrite commutative.2 in comm.
    specialize (comm (Fin1_ind (Fin2_rec x y))).
    etransitivity; [| etransitivity; [exact comm|]];
    unfold sg_op, SgOp_from_sssig; cbn;
    apply ap ; funext i; caseFin (op.2 i); reflexivity.
  Defined.

  Definition to_BoundedSemiLattice (op : binop σ) (u:constant σ)
             (assoc : is_associative eqsA op)
             (lidentity : is_leftIdentity eqsA op u)
             (ridentity : is_rightIdentity eqsA op u)
             (commutative : is_commutative eqsA op)
             (idempotent : is_idempotent eqsA op)
             : @IsBoundedSemiLattice A0 (SgOpA op) (MonUnitA u).
  Proof.
    constructor; [apply to_CommutativeMonoid; assumption|].
    intro x; pose (idemp := interpA idempotent.1); rewrite idempotent.2 in idemp.
    specialize (idemp (Fin1_ind (Fin1_rec x))).
    red; etransitivity; [| exact idemp].
    unfold sg_op, SgOp_from_sssig; cbn;
    apply ap ; funext i; caseFin (op.2 i); reflexivity.
  Defined.

End ToAlgebraicHierarchy.

Section ToLattices.
  Context `{Funext} {σ} (A : AlgebraicTheory (from_SingleSortedSignature σ))
          (join_op : binop σ) (meet_op : binop σ)
          (top_u : constant σ) (bot_u : constant σ).

  Notation eqsA := (equations_algebraic_theory _ A).
  Notation A0 := (A (inr tt)).
  Notation SgOpA op := (SgOp_from_sssig op A).
  Notation MonUnitA u := (MonUnit_from_sssig u A).
  Notation interpA := (is_algebraic_algebraic_theory _ A).

  Instance join_binop : Join A0 := fun x y => (join_op.1 ^^ A) (Fin2_rec x y o join_op.2).
  Instance meet_binop : Meet A0 := fun x y => (meet_op.1 ^^ A) (Fin2_rec x y o meet_op.2).
  Instance bot_constant : Bottom A0 := (bot_u.1 ^^ A) (fun x => Empty_rec _ (bot_u.2 x)).
  Instance top_constant : Top A0 := (top_u.1 ^^ A) (fun x => Empty_rec _ (top_u.2 x)).

  Definition to_BoundedJoinSemiLattice
             (assoc : is_associative eqsA join_op)
             (lidentity : is_leftIdentity eqsA join_op bot_u)
             (ridentity : is_rightIdentity eqsA join_op bot_u)
             (commutative : is_commutative eqsA join_op)
             (idempotent : is_idempotent eqsA join_op)
             : IsBoundedJoinSemiLattice A0.
  Proof. apply to_BoundedSemiLattice; assumption. Defined.

  Definition to_BoundedMeetSemiLattice
             (assoc : is_associative eqsA meet_op)
             (lidentity : is_leftIdentity eqsA meet_op top_u)
             (ridentity : is_rightIdentity eqsA meet_op top_u)
             (commutative : is_commutative eqsA meet_op)
             (idempotent : is_idempotent eqsA meet_op)
             : IsBoundedMeetSemiLattice A0.
  Proof. apply to_BoundedSemiLattice; assumption. Defined.

  Definition to_BoundedLattice
    (assoc : is_associative eqsA join_op)
    (lidentity : is_leftIdentity eqsA join_op bot_u)
    (ridentity : is_rightIdentity eqsA join_op bot_u)
    (commutative : is_commutative eqsA join_op)
    (idempotent : is_idempotent eqsA join_op)
    (assoc' : is_associative eqsA meet_op)
    (lidentity' : is_leftIdentity eqsA meet_op top_u)
    (ridentity' : is_rightIdentity eqsA meet_op top_u)
    (commutative' : is_commutative eqsA meet_op)
    (idempotent' : is_idempotent eqsA meet_op)
    (jmabsorption : is_absorbing eqsA join_op meet_op)
    (mjabsorption : is_absorbing eqsA meet_op join_op)
    : IsBoundedLattice A0.
  Proof.
    constructor; try (apply to_BoundedSemiLattice; assumption); intros x y;
    [pose (abs := interpA jmabsorption.1); rewrite jmabsorption.2 in abs
    | pose (abs := interpA mjabsorption.1); rewrite mjabsorption.2 in abs];
    specialize (abs (Fin1_ind (Fin2_rec x y)));
    (etransitivity; [| exact abs]) ;
    unfold join, join_binop, meet, meet_binop ; cbn;
    apply ap ; funext i; (caseFin (join_op.2 i) + caseFin (meet_op.2 i));
    try reflexivity; cbn; clear i; apply ap ; funext i;
    (caseFin (join_op.2 i) + caseFin (meet_op.2 i)) ; reflexivity.
  Defined.

  Definition to_DistributiveBoundedLattice
    (assoc : is_associative eqsA join_op)
    (lidentity : is_leftIdentity eqsA join_op bot_u)
    (ridentity : is_rightIdentity eqsA join_op bot_u)
    (commutative : is_commutative eqsA join_op)
    (idempotent : is_idempotent eqsA join_op)
    (assoc' : is_associative eqsA meet_op)
    (lidentity' : is_leftIdentity eqsA meet_op top_u)
    (ridentity' : is_rightIdentity eqsA meet_op top_u)
    (commutative' : is_commutative eqsA meet_op)
    (idempotent' : is_idempotent eqsA meet_op)
    (jmabsorption : is_absorbing eqsA join_op meet_op)
    (mjabsorption : is_absorbing eqsA meet_op join_op)
    (leftdistributive : is_leftDistributive eqsA join_op meet_op)
    : IsDistributiveBoundedLattice A0.
  Proof.
    constructor; [apply  to_BoundedLattice; assumption|].
    intros x y z; pose (distr := interpA leftdistributive.1);
    rewrite leftdistributive.2 in distr.
    specialize (distr (Fin1_ind (Fin3_rec x y z)));
    (etransitivity; [| etransitivity ; [exact distr|]]) ;
    unfold join, join_binop, meet, meet_binop ; cbn;
    apply ap ; funext i; (caseFin (join_op.2 i) + caseFin (meet_op.2 i));
    try reflexivity; cbn; clear i; apply ap ; funext i;
    (caseFin (join_op.2 i) + caseFin (meet_op.2 i)) ; reflexivity.
  Defined.

End ToLattices.


(** Equational theory of distributive bounded lattices *)

Module DistributiveBoundedLattice.
  Inductive distributiveBoundedLatticeIndexEquations :=
  | DBLJoinAssoc
  | DBLBotLeftId
  | DBLBotRightId
  | DBLJoinCommutative
  | DBLJoinIdempotent
  | DBLMeetAssoc
  | DBLTopLeftId
  | DBLTopRightId
  | DBLMeetCommutative
  | DBLMeetIdempotent
  | DBLJoinMeetAbsorption
  | DBLMeetJoinAbsorption
  | DBLJoinMeetLeftDistributive.

  Notation DBLI := distributiveBoundedLatticeIndexEquations.

  Definition top_u : constant distr_lattice_sssignature := (top_idx; 1%equiv).
  Definition bot_u : constant distr_lattice_sssignature := (bot_idx; 1%equiv).
  Definition meet_op : binop distr_lattice_sssignature := (meet_idx; 1%equiv).
  Definition join_op : binop distr_lattice_sssignature := (join_idx; 1%equiv).

  Definition DBLequations : Equations distributive_lattice_signature DBLI :=
    fun i =>
      from_SingleSortedEquation
        match i with
        | DBLJoinAssoc => associativity _ join_op
        | DBLBotLeftId => leftIdentity _ join_op bot_u
        | DBLBotRightId => rightIdentity _ join_op bot_u
        | DBLJoinCommutative => commutative _ join_op
        | DBLJoinIdempotent => idempotent _ join_op
        | DBLMeetAssoc => associativity _ meet_op
        | DBLTopLeftId => leftIdentity _ meet_op top_u
        | DBLTopRightId => rightIdentity _ meet_op top_u
        | DBLMeetCommutative => commutative _ meet_op
        | DBLMeetIdempotent => idempotent _ meet_op
        | DBLJoinMeetAbsorption => absorption _ join_op meet_op
        | DBLMeetJoinAbsorption => absorption _ meet_op join_op
        | DBLJoinMeetLeftDistributive => leftDistribute _ join_op meet_op
        end.

  Section FreeDistributiveBoundedLattice.
    Context `{Funext} (X : Type).

    Definition FreeDistributiveBoundedLattice :=
      AlgebraicTheoryFreeAlgebra (SingleSortedCarrier X) DBLequations.

    Notation FDBL := FreeDistributiveBoundedLattice.
    Notation FDBL0 := (FDBL (inr tt)).

    Definition join_binop0 : Join FDBL0 := (join_binop FDBL join_op).
    Definition meet_binop0 : Meet FDBL0 := (meet_binop FDBL meet_op).
    Definition bot_constant0 := bot_constant FDBL bot_u.
    Definition top_constant0 := top_constant FDBL top_u.

    Existing Instance join_binop0.
    Existing Instance meet_binop0.
    Existing Instance bot_constant0.
    Existing Instance top_constant0.

    Instance freeDBL : IsDistributiveBoundedLattice FDBL0.
    Proof.
      apply to_DistributiveBoundedLattice;
      try (unshelve econstructor; [ constructor| reflexivity]).
    Defined.

  End FreeDistributiveBoundedLattice.
End DistributiveBoundedLattice.



(** Presentation of a distributive lattice with generators and (in)equations *)

Definition distrLatticeWithGenerators_sssig (G : Type) (hset_G : IsHSet G)
  : SingleSortedSignature :=
  Build_SingleSortedSignature
    (SymbolT distr_lattice_sssignature + G) _
    (fun xg => match xg with
            | inl x => arity distr_lattice_sssignature x
            | inr g => Fin 0
            end).

Definition SSEquations σ (I : Type) := I -> SingleSortedEquation σ.

Record DistributiveBoundedLatticePresentation :=
  Build_DBLP
  { dblp_generators : Type
  ; dblp_hset_generators : IsHSet dblp_generators
  ; dblp_sig := distrLatticeWithGenerators_sssig dblp_generators dblp_hset_generators
  ; dblp_equations_index : Type
  ; dblp_equations : SSEquations dblp_sig dblp_equations_index
  ; dblp_inequations_index : Type
  (* For inequations we use the same representation as equations
     but transform them using [ineqToEq] below *)
  ; dblp_inequations : SSEquations dblp_sig dblp_inequations_index }.

Module DBL := DistributiveBoundedLattice.

Section FreePresentedDistributiveBoundedLattice.
  Context (dblp : DistributiveBoundedLatticePresentation)
          (X : Type).

  Definition InequationToEquation :=
    forall (C : Type) (x y : SingleSortedTermAlgebra (dblp_sig dblp) C),
      (SingleSortedTermAlgebra (dblp_sig dblp) C) *
      (SingleSortedTermAlgebra (dblp_sig dblp) C).

  Context (ineqToEq : InequationToEquation).

  Definition dblp_index :=
    DistributiveBoundedLattice.DBLI + (dblp_equations_index dblp + dblp_inequations_index dblp).

  Notation σ := (from_SingleSortedSignature (dblp_sig dblp)).

  (* This copy-paste is annoying but we don't have a notion of morphism
   of theory and the induced action on equations....*)
  Definition top_u : constant (dblp_sig dblp) := (inl top_idx; 1%equiv).
  Definition bot_u : constant (dblp_sig dblp) := (inl bot_idx; 1%equiv).
  Definition meet_op : binop (dblp_sig dblp) := (inl meet_idx; 1%equiv).
  Definition join_op : binop (dblp_sig dblp) := (inl join_idx; 1%equiv).

  Definition DBLequations : SSEquations (dblp_sig dblp) DBL.DBLI :=
    fun i =>
        match i with
        | DBL.DBLJoinAssoc => associativity _ join_op
        | DBL.DBLBotLeftId => leftIdentity _ join_op bot_u
        | DBL.DBLBotRightId => rightIdentity _ join_op bot_u
        | DBL.DBLJoinCommutative => commutative _ join_op
        | DBL.DBLJoinIdempotent => idempotent _ join_op
        | DBL.DBLMeetAssoc => associativity _ meet_op
        | DBL.DBLTopLeftId => leftIdentity _ meet_op top_u
        | DBL.DBLTopRightId => rightIdentity _ meet_op top_u
        | DBL.DBLMeetCommutative => commutative _ meet_op
        | DBL.DBLMeetIdempotent => idempotent _ meet_op
        | DBL.DBLJoinMeetAbsorption => absorption _ join_op meet_op
        | DBL.DBLMeetJoinAbsorption => absorption _ meet_op join_op
        | DBL.DBLJoinMeetLeftDistributive => leftDistribute _ join_op meet_op
        end.

  Definition dblpEquations : Equations σ dblp_index.
  Proof.
    intro x; destruct x as [idbl| [ieq | iineq]];
    apply from_SingleSortedEquation ;
    [ exact (DBLequations idbl)
    | exact (dblp_equations dblp ieq)|].
    destruct (dblp_inequations dblp iineq) as [ctx hset_ctx lhs0 rhs0].
    destruct (ineqToEq ctx lhs0 rhs0) as [lhs rhs].
    exact (Build_SingleSortedEquation _ ctx hset_ctx lhs rhs).
  Defined.

  Definition FreeDBLP :=
    AlgebraicTheoryFreeAlgebra (SingleSortedCarrier X) dblpEquations.

  Notation FDBLP0 := (FreeDBLP (inr tt)).

  Definition join_binop0 : Join FDBLP0 := (join_binop FreeDBLP join_op).
  Definition meet_binop0 : Meet FDBLP0 := (meet_binop FreeDBLP meet_op).
  Definition bot_constant0 := bot_constant FreeDBLP bot_u.
  Definition top_constant0 := top_constant FreeDBLP top_u.

  Existing Instance join_binop0.
  Existing Instance meet_binop0.
  Existing Instance bot_constant0.
  Existing Instance top_constant0.

  Context `{Funext}.

  Instance freeDBLP : IsDistributiveBoundedLattice FDBLP0.
  Proof.
    apply to_DistributiveBoundedLattice;
    try (unshelve econstructor; [left; constructor| reflexivity]).
  Defined.

End FreePresentedDistributiveBoundedLattice.


(** Underlying distributive lattice of the spectrum of a ring
    following (Coquand-Lombardi-Schuster09). *)
Section Spectrum.
  Context (A : Type) `{RingA : IsRing A}.

  Definition SpecDBLP : DistributiveBoundedLatticePresentation.
  Proof.
    pose (σ := (distrLatticeWithGenerators_sssig A (sg_set A))).
    (* The presentation of the spectrum has
       - one generator D(a) for each a ∈ A
       - 3 equations
       - 1 inequation *)
    refine (Build_DBLP A _ (Fin 2 + (A * A)) _ (A * A) _).
    - intro i; destruct i as [i|[a b]]; [caseFin i|].
      (* D(1) = ⊤ *)
      + refine (Build_SingleSortedEquation _ (Fin 0) _ _ _)
        ; apply (@apply_constant σ _);
        [ exact (inr 1%mc; 1%equiv) | exact (inl top_idx; 1%equiv)].
      (* D(0) = ⊥ *)
      + refine (Build_SingleSortedEquation _ (Fin 0) _ _ _)
        ; apply (@apply_constant σ _);
        [ exact (inr 0%mc; 1%equiv) | exact (inl bot_idx; 1%equiv)].
      (* D(ab) = D(a) ⊓ D(b) *)
      + refine (Build_SingleSortedEquation _ (Fin 0) _ _ _).
        * exact (@apply_constant σ _ (inr (a * b)%mc; 1%equiv)).
        * refine (@apply_binop σ _ (inl meet_idx; 1%equiv) _ _)
          ; apply (@apply_constant σ _);
          [exact (inr a; 1%equiv) | exact (inr b; 1%equiv)].
   - intro i; destruct i as [a b];
     (* D(a + b) ≤ D(a) ⊔ D(b) *)
     refine (Build_SingleSortedEquation _ (Fin 0) _ _ _).
     * exact (@apply_constant σ _ (inr (a + b)%mc; 1%equiv)).
     * refine (@apply_binop σ _ (inl join_idx; 1%equiv) _ _)
       ; apply (@apply_constant σ _);
       [exact (inr a; 1%equiv) | exact (inr b; 1%equiv)].
  Defined.
End Spectrum.