jcmckeown

Require Import HoTT.

Open Scope path_scope.
Open Scope type_scope.

Section Categories.

  (** Everyone knows a category has an underlying graph, so we should
   mention them *)

jcmckeown

Require Import HoTT. 

(* or your favourite source for the needed arrithmetic types *)

Open Scope list_scope.

(** 
  These are tactics to aid human consumption/production of terms compatible
  with the goal type --- sometimes coq prettyprinting produces ambiguous 
  appearances, while refine fails unless you fill in more holes --- which is

jcmckeown

Require Import Arith.

Open Scope list_scope.

(** Print le
Inductive le (n : nat) : nat -> Prop :=
    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
    
*)

jcmckeown

(** Define the types we need.  Checked in version Trunk of April 2013 *)

Polymorphic Inductive eqv { X : Type } : X -> X -> Type :=
  reflect (x : X) : eqv x x.

(** and assume the simplification we want *)

Polymorphic Axiom funextT :
 forall (X : Type) (P : X -> Type) (f g : forall x , P x) (s : 
  forall x, eqv (f x) (g x)) , eqv f g.

jcmckeown

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

jcmckeown

(** Approximating decidable equality for the type nCk.
 
As with GlobSet and DeltaSet, we implement locally the needed homotopy theory (which is trivial);
 `Require Import Homotopy` will do as well, modulo some notation, some names. I'd also bet some
 disappointment that the rhyming staves at the end of `nCk_uniq` are encapsulated in some named
 Lemma in `Homotopy`. Since the path arguments to `trans` in the concluding Lemma are cases of
 `@path nat`, which is a proposition in the sense of Voevodsky, it should be straight-forward (if
 tedious) to produce decidable equality in `nCk` by using those in `(list bool)` and `nat`.
*)

jcmckeown

Inductive nCk : nat -> nat -> Type :=
  |zz : nCk 0 0
  | incl { m n : nat } : nCk m n -> nCk (S m) (S n)
  | excl { m n : nat } : nCk m n -> nCk (S m) n.

Definition nCkComp { l m n : nat } :
  nCk l m -> nCk m n -> nCk l n.
Proof.
  intro.
  revert n.

jcmckeown

Require Import HoTT.

Local Open Scope path_scope.
Local Open Scope equiv_scope.

Module Export Cofiber.

  Local Inductive cofiber {A B : Type} (f : A -> B) : Type :=
    | apex : cofiber f
    | ground : B -> cofiber f.

jcmckeown

var id_math_stuff = {
    // id_math_stuff.theMJ
    theMJ : window.MathJax,
    
    // id_math_stuff.idMathRun =
    idMathRun : function () {
        if (id_math_stuff.theMJ) {
            id_math_stuff.theMJ.Hub.Queue(["Typeset", id_math_stuff.theMJ.Hub, "idc-cover"]);
        } else {
            console.log("there is still no mathjax?");

jcmckeown

/**
  PRELUDE: the names given in this initial comment are (in my own thinking) mostly fanciful, in that I don't mean that
  any of the particular people named particularly considered those particular things named for them in this note except
  perhaps Thurston; but they *are* meant to lend recognition to some names genuinely connected with the subject of this
  sketch.  Of course, the name that really makes any of this connect to that thing is Yoccoz, and none of these things
  is named for him...
  NOTATION: until further notice, capitals [W] indicate words and miniscules [x] indicate single letters. 
  length of a word is notated #[W].
  DEFINITION: given a word A of the form [WxY], where [x] is the n'th letter; the n'th SPLIT of A is the word
  [WxxYWxxY]