kyoDralliam

(** Trying to unnest the "pathological" example of an inductive type
 that nests with an indexed family, here equality *)

Inductive I := K : forall x : I, x = x -> I.


(* A more general induction principle for I than what Coq generates *)
Section GeneralElim.

kyoDralliam

From Coq Require Import ssreflect.
From Coq Require Import StrictProp.
From Coq Require Import List.

(* Access to nth element of a list,
   stdpp's notation for simpler test writing *)
Notation "l !! n" := (nth_error l n) (at level 20).


(** Discriminator for Some *)

kyoDralliam

From Equations Require Import Equations.
From Coq Require Import ssreflect.

Section Defs.
  Context {A : Type} (R : A -> A -> Prop).

  Definition entire := forall x, exists y, R y x.

  Definition idc_from a0 :=
    exists f : nat -> A, f 0 = a0 /\ forall n, R (f (S n)) (f n).

kyoDralliam

module GradualSTLC where

open import Agda.Primitive
open import Relation.Binary.Core
open import Relation.Binary.Definitions
open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
open import Data.Nat
open import Data.Empty
open import Data.Unit
open import Data.Maybe

kyoDralliam

(* 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