Roughly, ordinary globular sets, by the dependent type trick described for n-skeletal simplicial sets during the IAS Univalent Foundations programme year. It was remarked that getting a good notion of "simplicial set", with all degrees occupied, elluded codification, but the trick in the following should adapt trivially; that is, a Δ-set with ce…

GlobSets.v

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

(** a finite-skeletal globular set is either ... *)

Polymorphic Fixpoint n_glob (n : nat) : Type :=
  match n with
  | O => Type (** just a set... *)
  | S m => { t : Type & t -> t -> n_glob m } end. (** or a set with a finite-skeletal globular relation *)

(** The trouble with this definition is that subskeleta must be defined; but this is easy~ish *)

Polymorphic Lemma lastSkeleton {n : nat} : n_glob (S n) -> n_glob n.
Proof.
  induction n.
  intro.
  destruct X. exact x.
  intro.
  destruct X as [ s x' ].
  exists s.
  exact (fun x y => IHn (x' x y)).
Defined.

(** I should explain that lastSkeleton is why everything before it is supposed Polymorphic.  Before that, this recursion gave a Universe Inconsitency; I don't understand why nor what that means really. *)

(** To get a fully general ∞-globular set, ask for a sequence of skeleta, and insist (in as few ways as possible)
that subskeleta are previous skeleta. *)

Record GlobularSet : Type := {
  finGlobs : forall n : nat, n_glob n ;
  glob_skeletality : forall n, eqv (lastSkeleton (finGlobs (S n))) (finGlobs n)
}.

(** An example, to argue that we're close to the right idea.  This isn't *really* the right notion of "fundamental something", but it is suggestive *)

Fixpoint fundamental_n_glob (n : nat) (X : Type) : n_glob n :=
  match n with
  | O => X 
  | S m => existT _ X (fun x y => fundamental_n_glob m (eqv x y)) end.

(** some tedious stuff; if we were to Require Import Homotopy the equivalent things would be there by other names. *)

Polymorphic Lemma transp { A : Type } (P : A -> Type) :
  forall (a b : A) (eqn : eqv a b) (p : P a), P b.
Proof.
  intros.
  destruct eqn. auto.
Defined.

Polymorphic Lemma eqv_in_sigT { A : Type } ( P : A -> Type ) :
  forall (a b : A) (ab : eqv a b) (p : P a) (q : P b) 
    (pq : eqv (transp P a b ab p) q),
  eqv (existT P a p) (existT P b q).
Proof.
  intros.
  destruct ab.
  simpl in pq.
  destruct pq.
  apply reflect.
Defined.

(** of course, we obviously *want* this to be true;  *)

Lemma fundamental_glob_set (X : Type) : GlobularSet.
Proof.
  exists (fun n => fundamental_n_glob n X). (** obviously *)
  intro n.
  revert X. (** otherwise we get the wrong Induction hypothesis *)
  induction n.
  simpl. apply reflect. (** the zero case simplifies automagically *)
  intro.
  apply (eqv_in_sigT _ X X (reflect _)).
  unfold transp.
  apply funextT.  (** this is Why; though I ought to review, because ... *)
    intro.
  apply funextT.
  intro.
  auto. (** ... this works.  and I haven't added [reflect] as a hint, which means it must be hidden in the hypotheses somewhere,
 but they and especially the goal are quite illegible. *)
Defined.

(** all is well. *)