jcmckeown/cubeOrderIdeals.v

## cubeOrderIdeals.v
Require Import HoTT. (** the version from 2012... which was a while ago... *)

Open Scope path.
Open Scope equiv.
Open Scope type.

(** you see, back in the day, the hoqide was (by design) missing some things,
 and as a result, the "remember ... as ..." tactic was broken. *)

Ltac mmember X Y :=
 let yy := (fresh Y) in
 let y_eq := (fresh yy "_eqn") in
 set ( yy := X ) in * ; assert ( y_eq := 1 : yy = X ) ; clearbody yy.

Definition BType ( b : Bool ) : Type :=
 if b then Unit else Empty.

(** You've NO IDEA how much time this saves.  I'VE no idea how much needless hassle it introduces *)
Coercion BType : Bool >-> Sortclass.

Instance bt_hprop : forall b: Bool, IsHProp b.
Proof.
  intros [|].
  apply hprop_allpath.
  intros [] []. auto.
  intros [].
Defined.

(** a <= b ("material implication") as booleans, as a boolean *)
Definition compare_b ( a b : Bool ) : Bool :=
  if a then b else true.

Lemma compare_sound ( a b : Bool ) :
  ( a -> b ) -> compare_b a b.
Proof.
  intros.
  destruct a;
  destruct b; simpl in *.
  exact tt.
  destruct (X tt).
  exact tt.
  exact tt.
Defined.

Lemma compare_complete ( a b : Bool ) :
  compare_b a b -> a -> b.
Proof.
  destruct a; destruct b; auto.
Defined.

Lemma and_sound ( a b : Bool ) : (andb a b) -> a * b .
Proof.
  destruct a; destruct b; simpl.
  auto.
  intros [].
  intros [].
  intros [].
Defined.

Lemma or_sound ( a b : Bool ) : (orb a b) -> a + b.
Proof.
  intros.
  destruct a. left. exact tt.
  right.
  destruct b.
  exact tt.
  destruct X.
Defined.

Lemma and_complete { a b : Bool } : a * b -> andb a b.
Proof.
  destruct a.
    destruct b. intros. exact tt.
    intros [ a [] ].
    intros [[] x ].
Defined.

Lemma or_complete { a b : Bool } : a + b -> orb a b.
Proof.
  intro.
  destruct a ; destruct b; try exact tt.
  destruct X.
  destruct b.
  destruct b.
Defined.

(** *reflexive* decidable partial orders *)

Record DecidableOrder :=
  { DO_Dom : Type;
    DO_Dec : DO_Dom -> DO_Dom -> Bool;
    DO_Trans :
      forall a b c,
      (compare_b (DO_Dec a b) (compare_b (DO_Dec b c) (DO_Dec a c)));
    DO_Anti : forall a b , (DO_Dec a b) -> (DO_Dec b a) -> (a = b);
    DO_Norm : forall a, (DO_Dec a a) }.

Example BoolOrder : DecidableOrder.
Proof.
  exists Bool compare_b.
  intros.
    destruct a; destruct b ; try exact tt; destruct c; try exact tt.
  intros a b X Y.
    destruct a; destruct b; try auto.
    destruct X.
    destruct Y.
  intros [|]; exact tt.
Defined.

(** OrderIdeals generally are a Useful Thing. *)

Record OrderIdeal (D : DecidableOrder) := {
 Dom_Class : (DO_Dom D) -> Bool;
 Class_Trans :
  forall x y, (compare_b (DO_Dec D x y) (compare_b (Dom_Class y) (Dom_Class x)))
}.

Lemma allpath_classtrans `{Funext} {D : DecidableOrder} (DC : DO_Dom D -> Bool) :
  forall (f g : forall x y, compare_b (DO_Dec D x y) (compare_b (DC y)(DC x)) ),
 f = g.
Proof.
  intros.
  apply (path_forall f g).
  intro.
  apply allpath_hprop.
Defined.

Lemma oi_ident `{Funext} (D : DecidableOrder) (I J : OrderIdeal D) :
  (Dom_Class _ I) == (Dom_Class _ J) -> I = J.
Proof.
  intro.
  assert ( the_ident := path_forall _ _ X).
  destruct I.
  destruct J.
  simpl in *.
  destruct the_ident.
  apply ap.
  apply allpath_classtrans.
Defined.

(** they generalize downwards-intervals *)
Example DO_Interval (D : DecidableOrder) : DO_Dom D -> OrderIdeal D.
Proof.
  intro z.
  exists ( fun y => DO_Dec D y z ).
  intros.
  apply (DO_Trans D).
Defined.

(** From here, we start building the Poset of Subsets of a Finite Set *)

Fixpoint n_list_b (n : nat) : Type :=
  match n with
  | O => Unit
  | S m => Bool * (n_list_b m) end.

Lemma compare_all {n : nat} ( a b : n_list_b n ) : Bool.
Proof.
  induction n.
  exact true.
  destruct a as [a0 aa]; destruct b as [b0 bb].
  exact (if compare_b a0 b0 then IHn aa bb else false).
Defined.

Definition list_DO : nat -> DecidableOrder.
Proof.
  intro n.
  exists (n_list_b n) (@compare_all n).
  induction n.
  intros. exact tt.
  intros.
  destruct a as [[|] aa]; destruct b as [[|] bb]; destruct c as [[|] cc] ;
   simpl ;
  try apply IHn; try destruct (compare_all aa bb); try exact tt.
  induction n.
    intros. destruct a. destruct b. auto.
    intros. destruct a as [ [|] aa]; destruct b as [[|] bb] ; simpl in *.
    apply ap. auto.
    destruct X. destruct X0.
    apply ap. auto.
  induction n.
   intros. exact tt.
  intros [ [ | ] aa ] ; apply IHn.
Defined.

(** The subset poset is convenient in that we can *list* the immediate
upper neighbours of any subset ([stepsUp]).  hoqide 2012 is missing some harmless
standard libraries; so we fill in some gaps --- [map], [map_compose], [fold] ...
[fold_??_compare] are kinds of zipper folding; they express that n-ary conjunction and
disjunction are monotone.  Almost all this file is about monotone things...
*)

Fixpoint map { A B : Type } (f : A -> B) ( l : list A ) : list B :=
  match l with
  | nil => nil
  | cons a aa => cons (f a) (map f aa) end.

Lemma map_compose { A B C : Type } (f : A -> B) (g : B -> C) :
  forall l,
  map g (map f l) = map (g o f) l.
Proof.
  intro l.
  induction l.
  auto.
  simpl.
  apply ap.
  auto.
Defined.

Definition stepsUp { n : nat } ( J : n_list_b n ) : list (n_list_b n).
Proof.
  induction n.
  exact nil.
  destruct J as [ [ | ] JJ ].
  (* case J = (true , JJ) ;; we can step up J only by stepping-up JJ *)
  exact (map (fun x => (true , x)) (IHn JJ)).
  exact (cons (true, JJ) (map (fun x => (false, x)) (IHn JJ))).
Defined.

Fixpoint fold { A B : Type } (f : A -> B -> B) (b : B) (l : list A) : B :=
  match l with
  | nil => b
  | cons a aa => f a (fold f b aa) end.

Definition nfold {n : nat} { B : Type } (f : Bool -> B -> B) (b : B) (l : n_list_b n) : B.
Proof.
  induction n.
  exact b.
  exact (f (fst l) (IHn (snd l))).
Defined.

Lemma fold_or_compare { A : Type } (P Q : A -> Bool) :
  (forall a , compare_b (P a) (Q a)) ->
  (forall l : list A , compare_b (fold orb false (map P l)) (fold orb false (map Q l))).
Proof.
  intros.
  induction l.
  exact tt.
  simpl.
  assert (Xa := X a).
  destruct (P a).
    simpl in *.
    destruct (Q a). exact tt.
    destruct Xa.
  simpl.
  destruct (Q a).
    simpl. destruct (fold orb false (map P l)); exact tt.
    simpl. auto.
Defined.

Lemma fold_and_compare { A : Type } (P Q : A -> Bool) :
  (forall a, compare_b (P a) (Q a)) ->
  (forall l: list A, compare_b (fold andb true (map P l)) (fold andb true (map Q l))).
Proof.
  intros.
  induction l.
  exact tt.
  simpl.
  assert (Xa := X a).
  destruct (P a).
   destruct (Q a). simpl. apply IHl.
   destruct Xa.
  exact tt.
Defined.

(** This defines the test for (local) maximality in an ideal in the
subset poset of a finite set; we later prove [order_step_dichotomy]
that this Is In Fact Maximality. Do remember that an ideal may have
several maximal elements. *)

Definition Maximal { n : nat } (J : OrderIdeal (list_DO n) ) (x : n_list_b n ) : Type :=
  let L := map (Dom_Class _ J) (stepsUp x) in
  (Dom_Class _ J x ) * (negb (fold orb false L)).

(** we could extract this from DO_Anti and some bit fiddling, but it seems better
 to script a proof such that the proof term cooperates more quickly *)

Definition n_list_b_eqdec {n : nat} (x y : n_list_b n) : Bool.
Proof.
  induction n.
  exact true.
  exact (andb (if (fst x) then (fst y) else negb (fst y)) (IHn (snd x)(snd y))).
Defined.

(** it's ugly, but we will eventually need SOME strict total order, just to avoid
 asking for Too Many Equations.  Don't ask for Too Many Equations, you'll just
 end up trying to collapse them back down again. *)
Definition n_list_b_lexorder { n : nat } ( x y : n_list_b n) : Bool.
Proof.
  induction n.
  exact false. (* dataless things can't be different either way *)
  destruct x as [ x0 xx ]. destruct y as [ y0 yy ].
  (** if x0 << y0, then TRUE.  if x0 = y0, then IHn ; otherwise x0 >> y0 , hence false *)
  exact (if y0 then (if x0 then IHn xx yy else true) else if x0 then false else IHn xx yy).
Defined.

Lemma lex_is_strict { n : nat } : forall (x y : n_list_b n), n_list_b_lexorder x y -> ~ ( x = y ).
Proof.
  induction n.
  intros.
  destruct X.
  intros.
  destruct x as [ x0 xx ] , y as [ y0 yy ].
  simpl in X.
    destruct x0 ; destruct y0.
    intro.
    exact (IHn xx yy X (ap snd H)).
    intro.
    apply (transport BType (ap fst H) tt).
    intro.
    apply (transport BType (ap fst H^) tt).
    intro.
    exact (IHn xx yy X (ap snd H)).
Defined.

(** and now some stuff relating to how (n_list_b k) are all finite
 h-sets, all in essentially the same way.*)

Lemma nlb_eq_eq { n : nat } (x y : n_list_b n) :
  n_list_b_eqdec x y -> x = y .
Proof.
  induction n.
  destruct x. destruct y. intro. auto.
  intro H.
  destruct x.
  destruct y.
  destruct b. destruct b0. apply ap.
  simpl in H. auto.
  destruct H.
  destruct b0.
  destruct H.
  apply ap.
  auto.
Defined.

Lemma nlb_dec_refl { n : nat } : forall x : n_list_b n, n_list_b_eqdec x x.
Proof.
  induction n.
  intro.
  exact tt.
  intros [ bit xx ].
  destruct bit; simpl; auto.
Defined.

Lemma nlb_neq_neq {n : nat} : forall (x y : n_list_b n),
  ~ ( n_list_b_eqdec x y ) -> ~ ( x = y ).
Proof.
  intros x y H C.
  destruct C.
  apply H.
  apply nlb_dec_refl.
Defined.

(** intuition: if x ≼ y , then either x = y or we can step up from x to x' and still have x' ≼ y *)

Lemma order_step_dichotomy { n : nat } (x y : n_list_b n) (C : compare_all x y):
  (x = y) \/ fold orb false (map (fun z => compare_all z y) (stepsUp x)).
Proof.
  assert (x_y_eqn := nlb_eq_eq x y).
  assert (x_y_diff := nlb_neq_neq x y).
  mmember ( n_list_b_eqdec x y) eqdec_x_y.
  destruct eqdec_x_y.
  left. exact (x_y_eqn tt).
  right. clear x_y_eqn.
  assert (x_y_sep := x_y_diff idmap).
  clear x_y_diff.
  clear eqdec_x_y_eqn.
  induction n.
  simpl. apply x_y_sep.
    destruct x; destruct y; auto.
  destruct x as [ [|] xx ] ; destruct y as [ [|] yy ].
  assert ( ~ xx = yy ).
    intro.
    apply x_y_sep.
    apply ap. auto.
  assert ( help := IHn xx yy C X ).
  change (fold orb false (map (fun z : n_list_b (S n) => compare_all z (true,yy)) (map (fun z => (true,z)) (stepsUp xx)))).
  rewrite map_compose. unfold compose. auto.
  destruct C.
  simpl.
  simpl in C.
    destruct (compare_all xx yy).
    exact tt.
    destruct C.
  simpl.
  rewrite map_compose. unfold compose. unfold compare_b.
  apply IHn.
  simpl in C.
    destruct (compare_all xx yy).
    exact tt. destruct C.
  intro p.
  apply x_y_sep.
  apply ap. auto.
Defined.

(** maybe should call this negb_sound ? *)
Lemma bcontra : forall b,
  negb b -> b -> Empty.
Proof.
  intros [ | ] .
  auto. auto.
Defined.

Lemma contra_b : forall b : Bool,
  (~ b) -> negb b.
Proof.
  intros [ | ] .
  intro H.
  destruct (H tt).
  intro. exact tt.
Defined.

(** So. Nifty Thing: if you have an ideal in some order, and something maximal in that ideal,
  you can exclude that maximal something, and the remainder is still an ideal.
*)

Lemma drop_maximal { n : nat } (J : OrderIdeal (list_DO n)) (x : n_list_b n) :
  Maximal J x -> OrderIdeal (list_DO n).
Proof.
  exists (fun y => if (n_list_b_eqdec x y) then false else (Dom_Class _ J y)).
  intros y z.
  simpl in *.
  destruct X.
  mmember (n_list_b_eqdec x z) eqb_x_z.
  mmember (n_list_b_eqdec x y) eqb_x_y.
  assert ( helper := order_step_dichotomy x z ).
  destruct eqb_x_z. simpl. destruct (compare_all y z); exact tt.
  destruct eqb_x_y. assert ( p: x = y ).
    apply (nlb_eq_eq).
    refine ( transport _ eqb_x_y_eqn tt).
  destruct p.
  mmember (compare_all x z) compare_x_z.
  destruct (compare_x_z).
  destruct (helper tt).
    destruct p.
    destruct (transport BType (eqb_x_y_eqn @ eqb_x_z_eqn ^ ) tt).
  simpl.
  assert (b2 : compare_all x z).
    refine (transport _ compare_x_z_eqn tt).
  assert ( the_next := (fun y => (Class_Trans _ J y z) )).
  mmember (Dom_Class (list_DO n) J z) decide_J_z.
   destruct decide_J_z. simpl in the_next.
  assert ( sed_contra := compare_complete _ _ (fold_or_compare _ _ the_next (stepsUp x)) b1).
  simpl in b0.
  destruct (bcontra _ b0 sed_contra).
  exact tt.
  exact tt.
  apply (Class_Trans _ J).
Defined.


(** In Particular, *the* Maximum of an Interval is itself maximal in the ideal it generates. *)

Lemma generatorIsMaximal { n : nat } (x : n_list_b n) :
  Maximal (DO_Interval (list_DO n) x) x.
Proof.
  split.
  apply DO_Norm.
  induction n.
  exact tt.
  destruct x.
  destruct b.
   change
    (negb (fold orb false (map (Dom_Class (list_DO (S n)) (DO_Interval (list_DO (S n)) (true,n0))) (map (fun z => (true, z)) (stepsUp n0))))).
  rewrite map_compose. unfold compose. simpl. apply IHn.
   change
    (negb
      (fold orb false (map (Dom_Class (list_DO (S n)) (DO_Interval (list_DO (S n)) (false, n0)))
                           (cons (true, n0) (map (fun z => (false, z)) (stepsUp n0)))))).
  simpl.
  rewrite map_compose. unfold compose. simpl. apply IHn.
Defined.

(** hence we can cut the head off a cube and are left with an order ideal *)

Definition SubCube { n : nat } (x : n_list_b n) :=
  drop_maximal _ x (generatorIsMaximal x).

(** again, in our case this can be replaced with a Decidable Thing, but
 We don't need that much detail Today.  Maybe when I start trying to prove
 coherences? ...
*)

Definition subIdeal { D : DecidableOrder } ( I J : OrderIdeal D ) :=
  forall x, Dom_Class D I x -> Dom_Class _ J x.

Lemma subsub { D : DecidableOrder } ( I J K : OrderIdeal D ) :
  subIdeal I J -> subIdeal J K -> subIdeal I K.
Proof.
  intros S1 S2 x.
  auto.
Defined.

(** An ideal includes all the intervals under all it contains *)
Lemma intervalIsSub { n : nat } (I : OrderIdeal (list_DO n)) (x : n_list_b n) :
  Dom_Class _ I x -> subIdeal (DO_Interval (list_DO n) x) I.
Proof.
  intros.
  intros y z.
  simpl in *.
  revert X.
  apply compare_complete.
  revert z.
  apply compare_complete.
  apply (Class_Trans _ I).
Defined.

(** and truncating at a maximal produces not just an ideal, but a sub-ideal. the proof is trivial *)

Lemma dropMaxIsSub { n : nat } ( I : OrderIdeal (list_DO n))(x: n_list_b n)(M: Maximal I x) :
  subIdeal (drop_maximal I x M) I.
Proof.
  intro z.
  intro. simpl in *.
  destruct (n_list_b_eqdec x z).
  destruct X. auto.
Defined.

Lemma dropTwoMax { n : nat } ( I : OrderIdeal (list_DO n)) (x y : n_list_b n)
  (u : n_list_b_lexorder x y) (Mx : Maximal I x) (My : Maximal I y):
 Maximal (drop_maximal I y My) x.
Proof.
  assert ( sep := lex_is_strict x y u ).
  split.
  simpl.
    mmember (n_list_b_eqdec y x) eq_y_x.
    destruct eq_y_x.
    assert ( sed_contra := nlb_eq_eq y x (transport _ eq_y_x_eqn tt)).
    destruct ( sep (sed_contra ^)).
  apply Mx.
  apply contra_b.
  intro.
  assert ( help1 := fold_or_compare (Dom_Class (list_DO n) (drop_maximal I y My)) (Dom_Class _ I) ).
  simpl DO_Dom in help1.
  apply (bcontra _ (snd Mx)).
  revert X.  apply compare_complete.
  refine ( help1 _ (stepsUp x)).
  intro. apply compare_sound.
  apply ( dropMaxIsSub I y My).
Defined.

Lemma dropTwoAlternately  { n : nat } ( I : OrderIdeal (list_DO n)) (x y : n_list_b n)
  (u : n_list_b_lexorder x y) (Mx : Maximal I x) (My : Maximal I y):
 Maximal (drop_maximal I x Mx) y.
Proof.
  assert ( sep := lex_is_strict x y u).
  split.
  simpl.
    mmember (n_list_b_eqdec x y) eq_x_y.
    destruct eq_x_y.
    assert ( sed_contra := nlb_eq_eq x y (transport _ eq_x_y_eqn tt)).
    apply sep. auto.
  apply My.
  apply contra_b.
  intro.
  assert ( help1 := fold_or_compare (Dom_Class (list_DO n) (drop_maximal I x Mx)) (Dom_Class _ I)).
  simpl DO_Dom in help1.
  apply (bcontra _ (snd My)).
  revert X. apply compare_complete.
  refine ( help1 _ (stepsUp y)).
  intro. apply compare_sound.
  apply (dropMaxIsSub I x Mx).
Defined.

(** even better, the truncation of a maximal interval is a subideal of a truncation *)
Lemma dropTwoSideways { n : nat } ( I : OrderIdeal (list_DO n)) (x y : n_list_b n)
  (u : n_list_b_lexorder x y) (Mx : Maximal I x) (My : Maximal I y):
  subIdeal (drop_maximal _ _ (dropTwoMax I x y u Mx My)) (drop_maximal I x Mx).
Proof.
  intro.
  simpl.
  destruct (n_list_b_eqdec x x0).
  auto.
  destruct (n_list_b_eqdec y x0).
  intros [].
  auto.
Defined.

Lemma dta_is_dt { n : nat } ( I : OrderIdeal (list_DO n)) (x y : n_list_b n)
  (u : n_list_b_lexorder x y) (Mx : Maximal I x) (My : Maximal I y) :
 Dom_Class _ (drop_maximal _ _ ( dropTwoAlternately I x y u Mx My )) ==
 Dom_Class _ (drop_maximal _ _ ( dropTwoMax I x y u Mx My )).
Proof.
  intro.
  simpl in *.
  destruct (n_list_b_eqdec y x0);
    destruct (n_list_b_eqdec x x0); auto.
Defined.

Definition dta_really_is_dt `{Funext} { n : nat } ( I : OrderIdeal (list_DO n)) (x y : n_list_b n)
  (u : n_list_b_lexorder x y) (Mx : Maximal I x) (My : Maximal I y) :=
  oi_ident _ _ _ ( dta_is_dt I x y u Mx My).

(** this was for when we thought we could use long steps *)
(*
Lemma dropMaxInterval { n : nat } ( I : OrderIdeal (list_DO n)) (x : n_list_b n ) (M : Maximal I x) :
  subIdeal (SubCube x) (drop_maximal I x M).
Proof.
  intro.
  intro.
  simpl in *.
  destruct (n_list_b_eqdec x x0).
    destruct X.
  destruct M.
  revert b.
  apply compare_complete.
  revert X.
  apply compare_complete.
  apply (Class_Trans _ I).
Defined.
*)

(** that is all the orderings nonsense that we need today. For the rest,
 we only need to recall a couple of general constructions.
*)

Definition pullback { A B C : Type } (f : A -> C) (g : B -> C) : Type :=
  { x : A & hfiber g ( f x ) }.
Definition pullbackFst { A B C : Type } (f : A -> C)(g : B -> C) :
  pullback f g -> A .
Proof.
  intros [ a _ ]. auto.
Defined.

Definition pullbackSnd { A B C : Type } (f : A -> C)(g: B -> C) :
  pullback f g -> B.
Proof.
  intros [ a [ b _ ]].
  auto.
Defined.

Definition span A B : Type := { P : Type & (P -> A) * ( P -> B) }.
Definition pullbackSpan { A B C : Type } (f : A -> C) (g : B -> C) : span A B :=
  ( pullback f g ; (pullbackFst f g , pullbackSnd f g) ).

(** SO.  At first I just wanted an Identification of Two Spans.
 unfortunately, that does two ugly things: first, you have to use "ap"
 or "ap10pdq" whenever you want to compute what the identifications do
 to functions; and second, you CONFUSE COQ.  There's something about
 identification of Types that puts all the Universes out of joint.
 So, Instead, we say what the Category Wants for the universal property,
 and hope you all agree that this is indeed the Correct Way to Identify Spans
 Between Given Things.
*)

Definition spanEquiv (A B : Type) (C D : span A B) : Type :=
  { eqv : C .1 <~> D .1 &
  ( fst (C .2) == fst (D .2) o eqv ) * ( snd (C .2) == snd (D .2) o eqv ) }.

(**
 And now, a tour of the Proposed Definition.
 the intuitive picture of a cubic diagram has spaces named at the vertices of a cube,
 and the main difficulty is in figuring out how to say that 'all the maps commute'.
 Notionally, However, "commutativity" under each vertex means: the diagram below that vertex
 has a Limit, and we introduce a space with a map to that limit.  This idea runs out of
 steam in that there are too many different kinds of limit needed, if we want only to
 consider simple truncations of subcubes.

 However, if we replace our notion of truncated-cubical-limit with the related notion of
 terminal-Kan-extension (er... "right"-Kan???) from a downwards-closed subdiagram of the cube
 we can then CALCULATE (in our intuitive picture) that all the maps of the First Limit induced
 by forgetting a Maximal Vertex of an Ideal are pullbacks of eachother --- and then Pullback
 Pasting Lemmata will, hopefully, get us out of the mess we've invented for ourselves.

 Kan ( [ ] ..... [ ]     A ------> C          Kan ( [ ] .....  B     A x_c B ---> B
        .         .      ||       ||                 .         |        |         |
        .         .   =  ||       ||  <-forget-B-    .         |  =     |         |
        .         .      ||       ||                 .         V        V         V
        A ------> C )    A ------> C                 A ------> C )      A ------> C

 Kan ( [ ] ..... [ ]     C ======= C          Kan ( [ ] .....  B        B ======= B
        .         .      ||       ||                 .         |        |         |
        .         .   =  ||       ||  <-forget-B-    .         |  =     |         |
        .         .      ||       ||                 .         V        V         V
       [ ] .....  C )    C ======= C                [ ] -----> C )      C ======= C

    [A x_c B -> A] is [A x_c B -> A] , both as the pullback map and as the map-of-pullbacks.
*)

Record CubicByLimits `{Funext} (n : nat) := {
  partialLimits :
    OrderIdeal (list_DO n) -> Type;
  stepMaps : forall I, forall x, forall (M : Maximal I x), partialLimits I -> partialLimits (drop_maximal I x M);
  cubicRedundancy : forall I, forall x y,
  forall (sep : n_list_b_lexorder x y) (Mx : Maximal I x) (My : Maximal I y),
  spanEquiv _ _
    ( partialLimits I ; ( stepMaps I x Mx , stepMaps I y My ) )
    (pullbackSpan (transport (fun z => _ -> partialLimits z) (dta_really_is_dt I x y sep Mx My)
                     (stepMaps (drop_maximal I x Mx) y (dropTwoAlternately I x y sep Mx My) ))
                 (stepMaps (drop_maximal I y My) x (dropTwoMax I x y sep Mx My) ))
}.
	Require Import HoTT. (** the version from 2012... which was a while ago... *)

	Open Scope path.
	Open Scope equiv.
	Open Scope type.

	(** you see, back in the day, the hoqide was (by design) missing some things,
	and as a result, the "remember ... as ..." tactic was broken. *)

	Ltac mmember X Y :=
	let yy := (fresh Y) in
	let y_eq := (fresh yy "_eqn") in
	set ( yy := X ) in * ; assert ( y_eq := 1 : yy = X ) ; clearbody yy.

	Definition BType ( b : Bool ) : Type :=
	if b then Unit else Empty.

	(** You've NO IDEA how much time this saves. I'VE no idea how much needless hassle it introduces *)
	Coercion BType : Bool >-> Sortclass.

	Instance bt_hprop : forall b: Bool, IsHProp b.
	Proof.
	intros [\|].
	apply hprop_allpath.
	intros [] []. auto.
	intros [].
	Defined.

	(** a <= b ("material implication") as booleans, as a boolean *)
	Definition compare_b ( a b : Bool ) : Bool :=
	if a then b else true.

	Lemma compare_sound ( a b : Bool ) :
	( a -> b ) -> compare_b a b.
	Proof.
	intros.
	destruct a;
	destruct b; simpl in *.
	exact tt.
	destruct (X tt).
	exact tt.
	exact tt.
	Defined.

	Lemma compare_complete ( a b : Bool ) :
	compare_b a b -> a -> b.
	Proof.
	destruct a; destruct b; auto.
	Defined.

	Lemma and_sound ( a b : Bool ) : (andb a b) -> a * b .
	Proof.
	destruct a; destruct b; simpl.
	auto.
	intros [].
	intros [].
	intros [].
	Defined.

	Lemma or_sound ( a b : Bool ) : (orb a b) -> a + b.
	Proof.
	intros.
	destruct a. left. exact tt.
	right.
	destruct b.
	exact tt.
	destruct X.
	Defined.

	Lemma and_complete { a b : Bool } : a * b -> andb a b.
	Proof.
	destruct a.
	destruct b. intros. exact tt.
	intros [ a [] ].
	intros [[] x ].
	Defined.

	Lemma or_complete { a b : Bool } : a + b -> orb a b.
	Proof.
	intro.
	destruct a ; destruct b; try exact tt.
	destruct X.
	destruct b.
	destruct b.
	Defined.

	(** reflexive decidable partial orders *)

	Record DecidableOrder :=
	{ DO_Dom : Type;
	DO_Dec : DO_Dom -> DO_Dom -> Bool;
	DO_Trans :
	forall a b c,
	(compare_b (DO_Dec a b) (compare_b (DO_Dec b c) (DO_Dec a c)));
	DO_Anti : forall a b , (DO_Dec a b) -> (DO_Dec b a) -> (a = b);
	DO_Norm : forall a, (DO_Dec a a) }.

	Example BoolOrder : DecidableOrder.
	Proof.
	exists Bool compare_b.
	intros.
	destruct a; destruct b ; try exact tt; destruct c; try exact tt.
	intros a b X Y.
	destruct a; destruct b; try auto.
	destruct X.
	destruct Y.
	intros [\|]; exact tt.
	Defined.

	(** OrderIdeals generally are a Useful Thing. *)

	Record OrderIdeal (D : DecidableOrder) := {
	Dom_Class : (DO_Dom D) -> Bool;
	Class_Trans :
	forall x y, (compare_b (DO_Dec D x y) (compare_b (Dom_Class y) (Dom_Class x)))
	}.

	Lemma allpath_classtrans `{Funext} {D : DecidableOrder} (DC : DO_Dom D -> Bool) :
	forall (f g : forall x y, compare_b (DO_Dec D x y) (compare_b (DC y)(DC x)) ),
	f = g.
	Proof.
	intros.
	apply (path_forall f g).
	intro.
	apply allpath_hprop.
	Defined.

	Lemma oi_ident `{Funext} (D : DecidableOrder) (I J : OrderIdeal D) :
	(Dom_Class _ I) == (Dom_Class _ J) -> I = J.
	Proof.
	intro.
	assert ( the_ident := path_forall _ _ X).
	destruct I.
	destruct J.
	simpl in *.
	destruct the_ident.
	apply ap.
	apply allpath_classtrans.
	Defined.

	(** they generalize downwards-intervals *)
	Example DO_Interval (D : DecidableOrder) : DO_Dom D -> OrderIdeal D.
	Proof.
	intro z.
	exists ( fun y => DO_Dec D y z ).
	intros.
	apply (DO_Trans D).
	Defined.

	(** From here, we start building the Poset of Subsets of a Finite Set *)

	Fixpoint n_list_b (n : nat) : Type :=
	match n with
	\| O => Unit
	\| S m => Bool * (n_list_b m) end.

	Lemma compare_all {n : nat} ( a b : n_list_b n ) : Bool.
	Proof.
	induction n.
	exact true.
	destruct a as [a0 aa]; destruct b as [b0 bb].
	exact (if compare_b a0 b0 then IHn aa bb else false).
	Defined.

	Definition list_DO : nat -> DecidableOrder.
	Proof.
	intro n.
	exists (n_list_b n) (@compare_all n).
	induction n.
	intros. exact tt.
	intros.
	destruct a as [[\|] aa]; destruct b as [[\|] bb]; destruct c as [[\|] cc] ;
	simpl ;
	try apply IHn; try destruct (compare_all aa bb); try exact tt.
	induction n.
	intros. destruct a. destruct b. auto.
	intros. destruct a as [ [\|] aa]; destruct b as [[\|] bb] ; simpl in *.
	apply ap. auto.
	destruct X. destruct X0.
	apply ap. auto.
	induction n.
	intros. exact tt.
	intros [ [ \| ] aa ] ; apply IHn.
	Defined.

	(** The subset poset is convenient in that we can list the immediate
	upper neighbours of any subset ([stepsUp]). hoqide 2012 is missing some harmless
	standard libraries; so we fill in some gaps --- [map], [map_compose], [fold] ...
	[fold_??_compare] are kinds of zipper folding; they express that n-ary conjunction and
	disjunction are monotone. Almost all this file is about monotone things...
	*)

	Fixpoint map { A B : Type } (f : A -> B) ( l : list A ) : list B :=
	match l with
	\| nil => nil
	\| cons a aa => cons (f a) (map f aa) end.

	Lemma map_compose { A B C : Type } (f : A -> B) (g : B -> C) :
	forall l,
	map g (map f l) = map (g o f) l.
	Proof.
	intro l.
	induction l.
	auto.
	simpl.
	apply ap.
	auto.
	Defined.

	Definition stepsUp { n : nat } ( J : n_list_b n ) : list (n_list_b n).
	Proof.
	induction n.
	exact nil.
	destruct J as [ [ \| ] JJ ].
	(* case J = (true , JJ) ;; we can step up J only by stepping-up JJ *)
	exact (map (fun x => (true , x)) (IHn JJ)).
	exact (cons (true, JJ) (map (fun x => (false, x)) (IHn JJ))).
	Defined.

	Fixpoint fold { A B : Type } (f : A -> B -> B) (b : B) (l : list A) : B :=
	match l with
	\| nil => b
	\| cons a aa => f a (fold f b aa) end.

	Definition nfold {n : nat} { B : Type } (f : Bool -> B -> B) (b : B) (l : n_list_b n) : B.
	Proof.
	induction n.
	exact b.
	exact (f (fst l) (IHn (snd l))).
	Defined.

	Lemma fold_or_compare { A : Type } (P Q : A -> Bool) :
	(forall a , compare_b (P a) (Q a)) ->
	(forall l : list A , compare_b (fold orb false (map P l)) (fold orb false (map Q l))).
	Proof.
	intros.
	induction l.
	exact tt.
	simpl.
	assert (Xa := X a).
	destruct (P a).
	simpl in *.
	destruct (Q a). exact tt.
	destruct Xa.
	simpl.
	destruct (Q a).
	simpl. destruct (fold orb false (map P l)); exact tt.
	simpl. auto.
	Defined.

	Lemma fold_and_compare { A : Type } (P Q : A -> Bool) :
	(forall a, compare_b (P a) (Q a)) ->
	(forall l: list A, compare_b (fold andb true (map P l)) (fold andb true (map Q l))).
	Proof.
	intros.
	induction l.
	exact tt.
	simpl.
	assert (Xa := X a).
	destruct (P a).
	destruct (Q a). simpl. apply IHl.
	destruct Xa.
	exact tt.
	Defined.

	(** This defines the test for (local) maximality in an ideal in the
	subset poset of a finite set; we later prove [order_step_dichotomy]
	that this Is In Fact Maximality. Do remember that an ideal may have
	several maximal elements. *)

	Definition Maximal { n : nat } (J : OrderIdeal (list_DO n) ) (x : n_list_b n ) : Type :=
	let L := map (Dom_Class _ J) (stepsUp x) in
	(Dom_Class _ J x ) * (negb (fold orb false L)).

	(** we could extract this from DO_Anti and some bit fiddling, but it seems better
	to script a proof such that the proof term cooperates more quickly *)

	Definition n_list_b_eqdec {n : nat} (x y : n_list_b n) : Bool.
	Proof.
	induction n.
	exact true.
	exact (andb (if (fst x) then (fst y) else negb (fst y)) (IHn (snd x)(snd y))).
	Defined.

	(** it's ugly, but we will eventually need SOME strict total order, just to avoid
	asking for Too Many Equations. Don't ask for Too Many Equations, you'll just
	end up trying to collapse them back down again. *)
	Definition n_list_b_lexorder { n : nat } ( x y : n_list_b n) : Bool.
	Proof.
	induction n.
	exact false. (* dataless things can't be different either way *)
	destruct x as [ x0 xx ]. destruct y as [ y0 yy ].
	(** if x0 << y0, then TRUE. if x0 = y0, then IHn ; otherwise x0 >> y0 , hence false *)
	exact (if y0 then (if x0 then IHn xx yy else true) else if x0 then false else IHn xx yy).
	Defined.

	Lemma lex_is_strict { n : nat } : forall (x y : n_list_b n), n_list_b_lexorder x y -> ~ ( x = y ).
	Proof.
	induction n.
	intros.
	destruct X.
	intros.
	destruct x as [ x0 xx ] , y as [ y0 yy ].
	simpl in X.
	destruct x0 ; destruct y0.
	intro.
	exact (IHn xx yy X (ap snd H)).
	intro.
	apply (transport BType (ap fst H) tt).
	intro.
	apply (transport BType (ap fst H^) tt).
	intro.
	exact (IHn xx yy X (ap snd H)).
	Defined.

	(** and now some stuff relating to how (n_list_b k) are all finite
	h-sets, all in essentially the same way.*)

	Lemma nlb_eq_eq { n : nat } (x y : n_list_b n) :
	n_list_b_eqdec x y -> x = y .
	Proof.
	induction n.
	destruct x. destruct y. intro. auto.
	intro H.
	destruct x.
	destruct y.
	destruct b. destruct b0. apply ap.
	simpl in H. auto.
	destruct H.
	destruct b0.
	destruct H.
	apply ap.
	auto.
	Defined.

	Lemma nlb_dec_refl { n : nat } : forall x : n_list_b n, n_list_b_eqdec x x.
	Proof.
	induction n.
	intro.
	exact tt.
	intros [ bit xx ].
	destruct bit; simpl; auto.
	Defined.

	Lemma nlb_neq_neq {n : nat} : forall (x y : n_list_b n),
	~ ( n_list_b_eqdec x y ) -> ~ ( x = y ).
	Proof.
	intros x y H C.
	destruct C.
	apply H.
	apply nlb_dec_refl.
	Defined.

	(** intuition: if x ≼ y , then either x = y or we can step up from x to x' and still have x' ≼ y *)

	Lemma order_step_dichotomy { n : nat } (x y : n_list_b n) (C : compare_all x y):
	(x = y) \/ fold orb false (map (fun z => compare_all z y) (stepsUp x)).
	Proof.
	assert (x_y_eqn := nlb_eq_eq x y).
	assert (x_y_diff := nlb_neq_neq x y).
	mmember ( n_list_b_eqdec x y) eqdec_x_y.
	destruct eqdec_x_y.
	left. exact (x_y_eqn tt).
	right. clear x_y_eqn.
	assert (x_y_sep := x_y_diff idmap).
	clear x_y_diff.
	clear eqdec_x_y_eqn.
	induction n.
	simpl. apply x_y_sep.
	destruct x; destruct y; auto.
	destruct x as [ [\|] xx ] ; destruct y as [ [\|] yy ].
	assert ( ~ xx = yy ).
	intro.
	apply x_y_sep.
	apply ap. auto.
	assert ( help := IHn xx yy C X ).
	change (fold orb false (map (fun z : n_list_b (S n) => compare_all z (true,yy)) (map (fun z => (true,z)) (stepsUp xx)))).
	rewrite map_compose. unfold compose. auto.
	destruct C.
	simpl.
	simpl in C.
	destruct (compare_all xx yy).
	exact tt.
	destruct C.
	simpl.
	rewrite map_compose. unfold compose. unfold compare_b.
	apply IHn.
	simpl in C.
	destruct (compare_all xx yy).
	exact tt. destruct C.
	intro p.
	apply x_y_sep.
	apply ap. auto.
	Defined.

	(** maybe should call this negb_sound ? *)
	Lemma bcontra : forall b,
	negb b -> b -> Empty.
	Proof.
	intros [ \| ] .
	auto. auto.
	Defined.

	Lemma contra_b : forall b : Bool,
	(~ b) -> negb b.
	Proof.
	intros [ \| ] .
	intro H.
	destruct (H tt).
	intro. exact tt.
	Defined.

	(** So. Nifty Thing: if you have an ideal in some order, and something maximal in that ideal,
	you can exclude that maximal something, and the remainder is still an ideal.
	*)

	Lemma drop_maximal { n : nat } (J : OrderIdeal (list_DO n)) (x : n_list_b n) :
	Maximal J x -> OrderIdeal (list_DO n).
	Proof.
	exists (fun y => if (n_list_b_eqdec x y) then false else (Dom_Class _ J y)).
	intros y z.
	simpl in *.
	destruct X.
	mmember (n_list_b_eqdec x z) eqb_x_z.
	mmember (n_list_b_eqdec x y) eqb_x_y.
	assert ( helper := order_step_dichotomy x z ).
	destruct eqb_x_z. simpl. destruct (compare_all y z); exact tt.
	destruct eqb_x_y. assert ( p: x = y ).
	apply (nlb_eq_eq).
	refine ( transport _ eqb_x_y_eqn tt).
	destruct p.
	mmember (compare_all x z) compare_x_z.
	destruct (compare_x_z).
	destruct (helper tt).
	destruct p.
	destruct (transport BType (eqb_x_y_eqn @ eqb_x_z_eqn ^ ) tt).
	simpl.
	assert (b2 : compare_all x z).
	refine (transport _ compare_x_z_eqn tt).
	assert ( the_next := (fun y => (Class_Trans _ J y z) )).
	mmember (Dom_Class (list_DO n) J z) decide_J_z.
	destruct decide_J_z. simpl in the_next.
	assert ( sed_contra := compare_complete _ _ (fold_or_compare _ _ the_next (stepsUp x)) b1).
	simpl in b0.
	destruct (bcontra _ b0 sed_contra).
	exact tt.
	exact tt.
	apply (Class_Trans _ J).
	Defined.


	(** In Particular, the Maximum of an Interval is itself maximal in the ideal it generates. *)

	Lemma generatorIsMaximal { n : nat } (x : n_list_b n) :
	Maximal (DO_Interval (list_DO n) x) x.
	Proof.
	split.
	apply DO_Norm.
	induction n.
	exact tt.
	destruct x.
	destruct b.
	change
	(negb (fold orb false (map (Dom_Class (list_DO (S n)) (DO_Interval (list_DO (S n)) (true,n0))) (map (fun z => (true, z)) (stepsUp n0))))).
	rewrite map_compose. unfold compose. simpl. apply IHn.
	change
	(negb
	(fold orb false (map (Dom_Class (list_DO (S n)) (DO_Interval (list_DO (S n)) (false, n0)))
	(cons (true, n0) (map (fun z => (false, z)) (stepsUp n0)))))).
	simpl.
	rewrite map_compose. unfold compose. simpl. apply IHn.
	Defined.

	(** hence we can cut the head off a cube and are left with an order ideal *)

	Definition SubCube { n : nat } (x : n_list_b n) :=
	drop_maximal _ x (generatorIsMaximal x).

	(** again, in our case this can be replaced with a Decidable Thing, but
	We don't need that much detail Today. Maybe when I start trying to prove
	coherences? ...
	*)

	Definition subIdeal { D : DecidableOrder } ( I J : OrderIdeal D ) :=
	forall x, Dom_Class D I x -> Dom_Class _ J x.

	Lemma subsub { D : DecidableOrder } ( I J K : OrderIdeal D ) :
	subIdeal I J -> subIdeal J K -> subIdeal I K.
	Proof.
	intros S1 S2 x.
	auto.
	Defined.

	(** An ideal includes all the intervals under all it contains *)
	Lemma intervalIsSub { n : nat } (I : OrderIdeal (list_DO n)) (x : n_list_b n) :
	Dom_Class _ I x -> subIdeal (DO_Interval (list_DO n) x) I.
	Proof.
	intros.
	intros y z.
	simpl in *.
	revert X.
	apply compare_complete.
	revert z.
	apply compare_complete.
	apply (Class_Trans _ I).
	Defined.

	(** and truncating at a maximal produces not just an ideal, but a sub-ideal. the proof is trivial *)

	Lemma dropMaxIsSub { n : nat } ( I : OrderIdeal (list_DO n))(x: n_list_b n)(M: Maximal I x) :
	subIdeal (drop_maximal I x M) I.
	Proof.
	intro z.
	intro. simpl in *.
	destruct (n_list_b_eqdec x z).
	destruct X. auto.
	Defined.

	Lemma dropTwoMax { n : nat } ( I : OrderIdeal (list_DO n)) (x y : n_list_b n)
	(u : n_list_b_lexorder x y) (Mx : Maximal I x) (My : Maximal I y):
	Maximal (drop_maximal I y My) x.
	Proof.
	assert ( sep := lex_is_strict x y u ).
	split.
	simpl.
	mmember (n_list_b_eqdec y x) eq_y_x.
	destruct eq_y_x.
	assert ( sed_contra := nlb_eq_eq y x (transport _ eq_y_x_eqn tt)).
	destruct ( sep (sed_contra ^)).
	apply Mx.
	apply contra_b.
	intro.
	assert ( help1 := fold_or_compare (Dom_Class (list_DO n) (drop_maximal I y My)) (Dom_Class _ I) ).
	simpl DO_Dom in help1.
	apply (bcontra _ (snd Mx)).
	revert X. apply compare_complete.
	refine ( help1 _ (stepsUp x)).
	intro. apply compare_sound.
	apply ( dropMaxIsSub I y My).
	Defined.

	Lemma dropTwoAlternately { n : nat } ( I : OrderIdeal (list_DO n)) (x y : n_list_b n)
	(u : n_list_b_lexorder x y) (Mx : Maximal I x) (My : Maximal I y):
	Maximal (drop_maximal I x Mx) y.
	Proof.
	assert ( sep := lex_is_strict x y u).
	split.
	simpl.
	mmember (n_list_b_eqdec x y) eq_x_y.
	destruct eq_x_y.
	assert ( sed_contra := nlb_eq_eq x y (transport _ eq_x_y_eqn tt)).
	apply sep. auto.
	apply My.
	apply contra_b.
	intro.
	assert ( help1 := fold_or_compare (Dom_Class (list_DO n) (drop_maximal I x Mx)) (Dom_Class _ I)).
	simpl DO_Dom in help1.
	apply (bcontra _ (snd My)).
	revert X. apply compare_complete.
	refine ( help1 _ (stepsUp y)).
	intro. apply compare_sound.
	apply (dropMaxIsSub I x Mx).
	Defined.

	(** even better, the truncation of a maximal interval is a subideal of a truncation *)
	Lemma dropTwoSideways { n : nat } ( I : OrderIdeal (list_DO n)) (x y : n_list_b n)
	(u : n_list_b_lexorder x y) (Mx : Maximal I x) (My : Maximal I y):
	subIdeal (drop_maximal _ _ (dropTwoMax I x y u Mx My)) (drop_maximal I x Mx).
	Proof.
	intro.
	simpl.
	destruct (n_list_b_eqdec x x0).
	auto.
	destruct (n_list_b_eqdec y x0).
	intros [].
	auto.
	Defined.

	Lemma dta_is_dt { n : nat } ( I : OrderIdeal (list_DO n)) (x y : n_list_b n)
	(u : n_list_b_lexorder x y) (Mx : Maximal I x) (My : Maximal I y) :
	Dom_Class _ (drop_maximal _ _ ( dropTwoAlternately I x y u Mx My )) ==
	Dom_Class _ (drop_maximal _ _ ( dropTwoMax I x y u Mx My )).
	Proof.
	intro.
	simpl in *.
	destruct (n_list_b_eqdec y x0);
	destruct (n_list_b_eqdec x x0); auto.
	Defined.

	Definition dta_really_is_dt `{Funext} { n : nat } ( I : OrderIdeal (list_DO n)) (x y : n_list_b n)
	(u : n_list_b_lexorder x y) (Mx : Maximal I x) (My : Maximal I y) :=
	oi_ident _ _ _ ( dta_is_dt I x y u Mx My).

	(** this was for when we thought we could use long steps *)
	(*
	Lemma dropMaxInterval { n : nat } ( I : OrderIdeal (list_DO n)) (x : n_list_b n ) (M : Maximal I x) :
	subIdeal (SubCube x) (drop_maximal I x M).
	Proof.
	intro.
	intro.
	simpl in *.
	destruct (n_list_b_eqdec x x0).
	destruct X.
	destruct M.
	revert b.
	apply compare_complete.
	revert X.
	apply compare_complete.
	apply (Class_Trans _ I).
	Defined.
	*)

	(** that is all the orderings nonsense that we need today. For the rest,
	we only need to recall a couple of general constructions.
	*)

	Definition pullback { A B C : Type } (f : A -> C) (g : B -> C) : Type :=
	{ x : A & hfiber g ( f x ) }.
	Definition pullbackFst { A B C : Type } (f : A -> C)(g : B -> C) :
	pullback f g -> A .
	Proof.
	intros [ a _ ]. auto.
	Defined.

	Definition pullbackSnd { A B C : Type } (f : A -> C)(g: B -> C) :
	pullback f g -> B.
	Proof.
	intros [ a [ b _ ]].
	auto.
	Defined.

	Definition span A B : Type := { P : Type & (P -> A) * ( P -> B) }.
	Definition pullbackSpan { A B C : Type } (f : A -> C) (g : B -> C) : span A B :=
	( pullback f g ; (pullbackFst f g , pullbackSnd f g) ).

	(** SO. At first I just wanted an Identification of Two Spans.
	unfortunately, that does two ugly things: first, you have to use "ap"
	or "ap10pdq" whenever you want to compute what the identifications do
	to functions; and second, you CONFUSE COQ. There's something about
	identification of Types that puts all the Universes out of joint.
	So, Instead, we say what the Category Wants for the universal property,
	and hope you all agree that this is indeed the Correct Way to Identify Spans
	Between Given Things.
	*)

	Definition spanEquiv (A B : Type) (C D : span A B) : Type :=
	{ eqv : C .1 <~> D .1 &
	( fst (C .2) == fst (D .2) o eqv ) * ( snd (C .2) == snd (D .2) o eqv ) }.

	(**
	And now, a tour of the Proposed Definition.
	the intuitive picture of a cubic diagram has spaces named at the vertices of a cube,
	and the main difficulty is in figuring out how to say that 'all the maps commute'.
	Notionally, However, "commutativity" under each vertex means: the diagram below that vertex
	has a Limit, and we introduce a space with a map to that limit. This idea runs out of
	steam in that there are too many different kinds of limit needed, if we want only to
	consider simple truncations of subcubes.

	However, if we replace our notion of truncated-cubical-limit with the related notion of
	terminal-Kan-extension (er... "right"-Kan???) from a downwards-closed subdiagram of the cube
	we can then CALCULATE (in our intuitive picture) that all the maps of the First Limit induced
	by forgetting a Maximal Vertex of an Ideal are pullbacks of eachother --- and then Pullback
	Pasting Lemmata will, hopefully, get us out of the mess we've invented for ourselves.

	Kan ( [ ] ..... [ ] A ------> C Kan ( [ ] ..... B A x_c B ---> B
	. . \|\| \|\| . \| \| \|
	. . = \|\| \|\| <-forget-B- . \| = \| \|
	. . \|\| \|\| . V V V
	A ------> C ) A ------> C A ------> C ) A ------> C

	Kan ( [ ] ..... [ ] C ======= C Kan ( [ ] ..... B B ======= B
	. . \|\| \|\| . \| \| \|
	. . = \|\| \|\| <-forget-B- . \| = \| \|
	. . \|\| \|\| . V V V
	[ ] ..... C ) C ======= C [ ] -----> C ) C ======= C

	[A x_c B -> A] is [A x_c B -> A] , both as the pullback map and as the map-of-pullbacks.
	*)

	Record CubicByLimits `{Funext} (n : nat) := {
	partialLimits :
	OrderIdeal (list_DO n) -> Type;
	stepMaps : forall I, forall x, forall (M : Maximal I x), partialLimits I -> partialLimits (drop_maximal I x M);
	cubicRedundancy : forall I, forall x y,
	forall (sep : n_list_b_lexorder x y) (Mx : Maximal I x) (My : Maximal I y),
	spanEquiv _ _
	( partialLimits I ; ( stepMaps I x Mx , stepMaps I y My ) )
	(pullbackSpan (transport (fun z => _ -> partialLimits z) (dta_really_is_dt I x y sep Mx My)
	(stepMaps (drop_maximal I x Mx) y (dropTwoAlternately I x y sep Mx My) ))
	(stepMaps (drop_maximal I y My) x (dropTwoMax I x y sep Mx My) ))
	}.