Some extremely basic description stuff

description.v

Require Import Coq.Unicode.Utf8.

Import IfNotations.

Inductive U: Set :=
| self
| void
| sum (A B: U)
| unit
| prod (A B: U).

Infix "*" := prod.
Infix "+" := sum.

Inductive Ext {X: Set}: U → Set :=
| I: X → Ext self

| tt: Ext unit
| pair {A B}: Ext A → Ext B → Ext (A * B)
| i1 {A B}: Ext A → Ext (A + B)
| i2 {A B}: Ext B → Ext (A + B)
.
Arguments Ext: clear implicits.

Infix "#" := pair (at level 30).

Definition π1 {X A B} (e: Ext X (A * B)): Ext X A :=
  let '(a # b) := e in a.
Definition π2 {X A B} (e: Ext X (A * B)): Ext X B :=
  let '(a # b) := e in b.

Definition unI {X} (e: Ext X self): X :=
  let '(I x) := e in x.

Inductive μ {u}: Set := roll (x: Ext μ u).
Arguments μ: clear implicits.

Coercion μ: U >-> Sortclass.

Definition unroll {F} (e: μ F) :=
  let '(roll x) := e in x.

Fixpoint map {F} {A B: Set} (f: A → B) (e: Ext A F): Ext B F :=
  match e with
  | I x => I (f x)
  | tt => tt
  | x # y => map f x # map f y
  | i1 x => i1 (map f x)
  | i2 x => i2 (map f x)
  end.

Fixpoint fold {F} {A: Set} (f: Ext A F → A) (e: μ F) {struct e}: A :=
  f ((fix loop {G} (x: Ext (μ F) G): Ext A G :=
        match x with
        | I x => I (fold f x)
        | tt => tt
        | x # y => loop x # loop y
        | i1 x => i1 (loop x)
        | i2 x => i2 (loop x)
        end) _ (unroll e)).

poly.v

Require Import Coq.Unicode.Utf8.

Import IfNotations.

Inductive U :=
| self

| compose (A B: U)

| unit
| prod (A B: U)

| void
| sum (A B: U)

| K (A: Set)
| tensor (A: Set) (B: U)
| power (A: Set) (B: U)
| Σ (A: Set) (B: A → U)
| Π (A: Set) (B: A → U)
.

Infix "*" := prod.
Infix "+" := sum.
Infix "∘" := compose (at level 30).
Infix "⊗" := tensor (at level 30).

Record Poly := poly { El: Set ; π: El → Set ; }.
Infix "▹" := poly (at level 30).

Fixpoint eval (x: U): Poly :=
  match x with
  | self => Datatypes.unit ▹ λ _, Datatypes.unit

  (* I don't recall if this is right at all *)
  | compose A B =>
      { xy: El (eval A) * El (eval B) & π (eval A) (fst xy) → π (eval B) (snd xy) } ▹
        λ x, π (eval A) (fst (projT1 x))

  | K A => A ▹ λ _, Empty_set

  | unit => Datatypes.unit ▹ λ _, Empty_set
  | prod A B =>
      (El (eval A) * El (eval B)) ▹ λ x, π (eval A) (fst x) + π (eval B) (snd x)

  | void => Empty_set ▹ λ x, match x with end
  | sum A B =>
      (El (eval A) + El (eval B)) ▹
        λ x, match x with
             | inl x => π (eval A) x
             | inr x => π (eval B) x
             end

  | tensor A B =>
      (A * El (eval B)) ▹ λ x, π (eval B) (snd x)
  | power A B =>
      (A → El (eval B)) ▹ λ x, { j & π (eval B) (x j) }

  | Σ A B => { a: A & El (eval (B a)) } ▹ λ x, π (eval (B _)) (projT2 x)
  | Π A B => (∀ a: A, El (eval (B a)) ) ▹ λ x, { j & π (eval (B _)) (x j) }
  end%type.

Inductive μ {u: U}: Set := sup (x: El (eval u)) (p: π (eval u) x → μ).
Arguments μ: clear implicits.

Coercion μ: U >-> Sortclass.