Very nearly how to describe delta-sets by the "dependent type" trick. It isn't quite right, because of Stuff... but never mind that for now. Among other things, it's rather difficult to extract what data a DeltaSkeleton actually involves. That is, coq can `eval cbv` the expressions `projT1 (DeltaSkeleton 0)`, and produces exactly what we want, `…

DeltaSets.v

(** A 0-skeletal filling of an l-simplex is (S l) vertices.
    A (S k)-skeletal filling of an l-simplex has (S l) C (S k)  (S k)-cells
    matching their boundaries in a k-skeletal filling of an l-simplex;
    where to say the (S k)-cell matches its boundary is to say that its boundary
    is the underlying k-skeletal filling of its underlying (S k)-simplex.
 *)

(** I don't know why coq makes its type system so rich and its proof system so comparatively strict.
possibly (almost certainly) because the reverse combination would be too difficult/inconsistent?
for instance, it makes intuitive sense that this next Fixpoint should be equivalent (as a type over nat * nat)
to

  Inductive NcK : nat -> nat -> Type :=
    zz : NcK 0 0
  | incl _ _ : NcK m n -> NcK (S m) (S n)
  | excl _ _ : NcK m n -> NcK (S m) n .

but, for whatever reason, the Fixpoint definition makes writing proofs immensely simpler.
*)


Fixpoint chooseType ( n k : nat ) : Type :=
  match n with
  | 0 => 
    match k with 
    | 0 => True
    | S _ => False end
  | S m => match k with
    | O => True
    | S l => sum (chooseType m l) (chooseType m k) end end.

(** We don't need this, because chooseType 0 (S k) already is False 

Lemma chooseFromNone (k : nat) : chooseType 0 (S k) -> False.
Proof.
  intro.
  remember 0 as n0 in H.
  remember (S k) as sk in H.
  destruct H.
    discriminate Heqsk.
    discriminate Heqn0.
    discriminate Heqn0.
Defined.
*)

(** obviously, a composition law *)

Lemma subsetBySubset { n k l } : chooseType n k -> chooseType k l ->
  chooseType n l.
Proof.
  revert k l.
  induction n.
  intros.
    destruct k.
    destruct l.
     auto.
    contradict X0.
    contradict X.
  intros k l cs ct.
   destruct k.
     destruct l. apply I.
      contradict ct.
    simpl in cs.
     destruct l. apply I.
    destruct cs as [ lcs | rcs ].
     destruct ct as [ lct | rct ]; simpl.
      left. apply (IHn _ _ lcs lct).
      right. apply (IHn _ _ lcs rct).
     right.
      apply (IHn _ _ rcs ct).
Defined.

(** this similarly makes things difficult, but one has to get the objects to match somehow! 
    I was reminded today that `kList A k := chooseType k 1 -> A` would do just as well, and
    clean up some other definitions.  Another revision another day.
*)

Definition kList (A : Type) (k : nat) : Type :=
 chooseType k 1 -> A.

Definition subListBySubSet {k l : nat} { A : Type } ( al : kList A k) (ct:  chooseType k l) : kList A l :=
 fun c => al (subsetBySubset ct c).

(** as with GlobSets.v, implement our own Type-valued equivalence --- or Require Import Homotopy and adjust
  later as required.*)

Inductive eqv { A : Type } : A -> A -> Type :=
  ideq (a : A) : eqv a a.

Notation " a == b " := (eqv a b) (at level 53).

Definition ap { A B : Type } (f : A -> B) { x y : A } : x == y -> (f x) == (f y).
Proof.
  intro h.
  destruct h.
  apply ideq.
Defined.

(** A long proof by cases.  There ought to be a smarter way to do this. Clearly
  the repetetive bits should be automated, but... if we hadn't written *this*,
  we'd want to know *why?* . *)

Lemma subsetBySubsetEq { k l m n : nat }
  (ca : chooseType k l) (cb : chooseType l m) (cc : chooseType m n):
  subsetBySubset ca (subsetBySubset cb cc) == subsetBySubset (subsetBySubset ca cb) cc.
Proof.
  revert l m n ca cb cc. (* to have the most flexible Induction Hypothesis possible *)
  induction k.
  intros. (* there's really only one thing anything can be, now *)
    destruct l.
    destruct ca.
    destruct m.
    destruct cb.
    destruct n.
    destruct cc.
    simpl. apply ideq.
    contradict cc.
    contradict cb.
    contradict ca.
  intros.
    revert m n cb cc.
  destruct l.
    intros.
    destruct ca.
     destruct m.
      destruct cb.
       destruct n.
        destruct cc.
         apply ideq.
     contradict cc.
     contradict cb.
  destruct ca as [ lca | rca ].
    intro m.
    destruct m.
      intros. destruct cb.
       destruct n. apply ideq.
       contradict cc.
      intros.  destruct cb as [ lcb | rcb ].
       destruct n. destruct cc. apply ideq.
        destruct cc. simpl. apply ap. auto.
        simpl. apply ap. auto.
          destruct n. destruct cc. apply ideq.
            simpl. apply ap. auto.
    intro m.
    destruct m.
      intros. destruct cb.
       destruct n. apply ideq.
       contradict cc.
      intros. destruct cb as [lcb | rcb ].
       destruct n. destruct cc. apply ideq.
(* after much fighting, I found the reason the previous stopped working
   is that `simpl` was a tad too eager. *)
        destruct cc as [ lcc | rcc ]; 
          simpl subsetBySubset at 1 3 4; lazy beta iota;
          apply ap; auto.
       destruct n. destruct cc. apply ideq.
        destruct cc as [ lcc | rcc ];
          simpl subsetBySubset at 1 3 4; lazy beta iota;
          apply ap; auto.
Defined.

Lemma listsubsetsubseteq : forall { k l m : nat }, forall { A : Type },
  forall ll : kList A k, forall cs : chooseType k l, forall ct : chooseType l m,
    forall j : chooseType m 1,
  (subListBySubSet (subListBySubSet ll cs) ct) j == (subListBySubSet ll (subsetBySubset cs ct)) j.
Proof.
  intros.
  unfold subListBySubSet.
  apply ap.
  apply subsetBySubsetEq.
Defined.

(** In standard HoTT, this is `transport`. *)

Lemma trans { A : Type } { P : A -> Type } {x y : A} :
  x == y -> P x -> P y.
Proof. intro h. induction h; auto.
Defined.

Notation " ( a ; b ) " := (existT _ a b).

(** and this is the main use of eqv ... just try it with native "=" instead! Again, it's in
  standard HoTT, I don't recall the name. *)

Lemma sigma_path {A : Type } { P : A -> Type } (x y : A) (p : P x) (q : P y)( h : eqv x y):
  eqv (trans h p) q -> eqv (x ; p) (y ; q).
Proof.
  intro.
  induction h.
  simpl in X.
  induction X.
  apply ideq.
Defined.

Lemma inverse { A : Type } { a b : A } : a == b -> b == a.
Proof.
  intro h.
  destruct h.
  apply ideq.
Defined.

Notation "! h" := (inverse h) (at level 90).

 (** trans ( h : a == b ) ( cs => h a cs ) cs0 == h b cs0 
*)

Axiom funext : forall { A : Type } (P : A -> Type) { f g : forall a, P a } ,
 ( forall a , f a == g a ) -> f == g.

(*
Section DeltaSkel. *)

  Record DeltaStage : Type := { 
    DS : Type;
    figs : DS -> nat -> Type;
    subfig : forall X : DS, forall k l, figs X k -> chooseType k l -> figs X l;
    subfigEq : forall X : DS, forall k l m, forall ff : figs X k, forall cs : chooseType k l,
      forall ct : chooseType l m,
       (subfig _ _ _ ff (subsetBySubset cs ct)) == (subfig _ _ _ (subfig _ _ _ ff cs) ct) 
  }.

  Definition DeltaZero : DeltaStage.
  Proof.
    exists Type kList (fun X k l => @subListBySubSet k l X).
    intros.
    apply funext.
    intros.
    apply inverse.
    apply listsubsetsubseteq.
  Defined.

  Definition DS_S (ds_n : DeltaStage) (n : nat) : Type := { X : DS ds_n & figs ds_n X n -> Type }.

  Definition figs_S (ds_n : DeltaStage) (n : nat) :
    (DS_S ds_n n) -> nat -> Type :=
   fun X => let ( X, P ) := X in fun m => 
    { ff : figs ds_n X m & forall cs : chooseType m n, P (subfig ds_n X _ _ ff cs) }.

  Lemma subfig_S (ds_n : DeltaStage) (n : nat) :
    forall X : (DS_S ds_n n), forall k l, figs_S ds_n n X k -> chooseType k l -> figs_S ds_n n X l.
  Proof.
    intros X k l f cs.
    destruct X as [X P].
    simpl in *.
    destruct ds_n. simpl in *.
    destruct f as [ ff R ].
    exists (subfig0 X k l ff cs).
    intros.
    refine (trans (subfigEq0 _ k l n ff cs cs0) _ ).
    apply R.
  Defined.

  Lemma subfigEq_S (ds_n : DeltaStage) (n : nat) :
    forall X : (DS_S ds_n n), forall k l m, forall ff : figs_S ds_n n X k,
      forall cs : chooseType k l, forall ct : chooseType l m,
    eqv (subfig_S ds_n n X _ _ ff (subsetBySubset cs ct)) (subfig_S ds_n n X _ _ (subfig_S ds_n n X _ _ ff cs) ct).
  Proof.
    intros.
    destruct X as [X P].
    simpl in * |- .
    destruct ff as [ff R]. simpl in * |- .
    destruct ds_n. simpl in *.
    refine ( sigma_path _ _ _ _  (subfigEq0 _ k l m ff cs ct) _).
    apply funext.
      intro cq.
      (**  Hmmm... I really thought the issue was a discrete one at this point,
         but this is looking more and more like a genuine coherence issue.
         ha-rumphf!
       *)
      admit.
  Defined.

  Definition DeltaSkeleton : nat -> DeltaStage.
  Proof.
    intro n; induction n.
    exact DeltaZero.
    exists (DS_S IHn n) (figs_S IHn n) (subfig_S IHn n).
    intros.
    apply subfigEq_S.
  Defined.

(*
End DeltaSkel. *)

(** the first try was this
Definition DeltaSkeleton : nat -> 
 { DS : Type &
   { figs : DS -> nat -> Type & 
     { subfig : forall X : DS, forall k l, figs X k -> chooseType k l -> figs X l &
        forall X, forall k l m, forall ff : figs X k, forall cs : chooseType k l, forall ct : chooseType l m, 
          subfig _ _ _ ff (subsetBySubset cs ct) = subfig _ _ _ (subfig _ _ _ ff cs) ct } } }.
Proof.
  intro n.  induction n.
  exists Type.
    exists kList.
    exists (fun X k l => @subListBySubSet k l X ).
    exact (fun X k l m  => @listsubsetsubseteq k l m X ).
  destruct IHn as [ nSkel [ nFig [ nSubFig nFigEq ]]].
  set (SnSkel := { X : nSkel & nFig X (S n) -> Type }). 
  (** strictly, this leads to "coloured" Delta-Skeleta; never mind for now. *)
  exists SnSkel.
  set (SnFig := fun XP : SnSkel => fun k =>
    { ff : nFig (projT1 XP) k &
  forall cs : chooseType k (S n), (projT2 XP) (nSubFig (projT1 XP) _ _ ff cs) }).
  exists SnFig.
  assert ( SnSubFig : forall (X : SnSkel) (k l : nat), SnFig X k -> chooseType k l -> SnFig X l ).
    intros.
    destruct X as [X P].
    destruct X0 as [ ff R ].
    unfold SnFig. simpl in *.
    exists (nSubFig X k l ff H ).
    intro.
    rewrite <- nFigEq.
    apply R.
  exists SnSubFig.
  (** Of course it is difficult to proceed from here; while coq certainly knows what is the
  term  SnSubFig, it isn't about to tell /me/, not 'till I discharge the proof somehow. And
  in any case, we're sure to devolve in the end upon a stranger case of an equally-obvious
  proposition of the Wsubsetsubseteq family.  For myself, I'm convinced that there's no funny-
  stuff lurking, and we can admit the theorem. *)
  admit.
Defined.
*)