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.
 *)

(** This is both the heart of the matter, and the weakest link; for some reason
    this presentation of n C k makes it very difficult to prove equations.
    Perhaps some clever person can rework the whole around a different presentation.
 *)

Inductive chooseType : nat -> nat -> Set :=
  | empt n : chooseType n 0
  | incl n k : chooseType n k -> chooseType (S n) (S k)
  | excl n k : chooseType n k -> chooseType (S n) k.

(** to handle base cases in recursive constructions *)

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 } (ss : chooseType n k) (tt : chooseType k l) :
  chooseType n l.
Proof.
  revert l tt.
  induction ss.
  intros.
    destruct l.
    apply empt.
    contradict tt. refine (chooseFromNone _).
  intros.
    remember (S k) as sk.
    destruct tt. apply empt.
    assert (n0 = k).
      injection Heqsk; auto.
    rewrite H in tt.
    apply incl.
    apply IHss. auto.
    assert (n0 = k).
      injection Heqsk; auto.
    rewrite H in tt.
    apply excl.
    apply IHss. auto.
  intros.
    apply excl.
    apply IHss.
    auto.
Defined.

(** this similarly makes things difficult, but one has to get the objects to match somehow! *)

Inductive kList (A : Type) : nat -> Type :=
  | zlist : kList A 0
  | oneMore { k : nat } : A -> kList A k -> kList A (S k).

Lemma subListBySubSet {k l : nat} { A : Type } : kList A k -> chooseType k l -> kList A l.
Proof.
  intro ll; revert l.
  induction ll.
  intros.
    destruct l.
    apply zlist.
    contradict H.
    refine (chooseFromNone _).
  intros.
    remember (S k) as sk.
    destruct H.
    apply zlist.
    assert (n = k).
      injection Heqsk; auto.
      rewrite H0 in H.
      apply (oneMore A a).
      auto.
    assert (n = k).
      injection Heqsk; auto.
      rewrite H0 in H.
      auto.
Defined.

(** the following are axioms because coq makes proving them much too difficult. *)

Axiom subsetsubseteq : forall { k l m n : nat},
  forall cs : chooseType k l, forall ct : chooseType l m, forall cq : chooseType m n,
  subsetBySubset cs (subsetBySubset ct cq) = subsetBySubset (subsetBySubset cs ct) cq.

(** that is, (nat, subsetType, subsetBySubset) is a category, once you figure out
  what the identities are --- which isn't difficult *)

Axiom listsubsetsubseteq : forall { k l m : nat }, forall { A : Type },
  forall ll : kList A k, forall cs : chooseType k l, forall ct : chooseType l m,
  subListBySubSet ll (subsetBySubset cs ct) = subListBySubSet (subListBySubSet ll cs) ct.

(** So that, similarly, the subset category acts on lists the way you'd want it to. *)

(** Delta-Types generalize Types the way ... I'm not sure how to say, exactly.  Anyways,
  Delta-Types also generalize lists in that there's a natural-enough action of the chooseType
  category on them. It's customary to think of DeltaSkeleton(n).DS as "The" Type of n-skeletal Delta sets;
  nonetheless, the notions of figure, subfigure, and the representation of chooseType are on an equal footing here.
  *)

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.

I'm contemplating whether to use Section NNN to hold enough context for SnSubFig to be defined by a Let ...; the trouble that occurs to me is how this tends to interfere with destructuring, not to mention guming up the terms eventually discharged... if you do have suggestions... pull-requests will be read kindly.

Could we ask @mattam82 to toss in a more transparent set/assert hybrid?

A New tack from a completely different angle: "cubical" categories
https://gist.github.com/jcmckeown/2210b6932c8705d01da2