mikeshulman / coq-hott Goto Github PK

Have a look in this branch:

https://github.com/Alizter/HoTT/blob/graph_wildcat/theories/WildCat/Core.v

There is a really weird universe error in the definition of Is1Cat now. I can't work out why this is.

The Limits and Colimits directories should be generalizable from Type to arbitrary wild categories.

For ooCat.v, similar to how Laxity is defined, we could have a stream of op's. This would then allow us to consider all opping at once.

It is mentioned in ooCat.v that DComma could possible be generalised to act on sections of displayed categories. This could then be used to define what a transfor is in general. I tried messing around with defining such a thing on paper but couldn't get it to work. What do we have in mind here?

Should this go in WildCat/Type?

I've finished the proof of CORS 2.26 (which was needed for my general-modalities version of the LES), but am having universe problems. Right now I think that my initial attempt at defining separated modalities with a simple typeclass relating two modalities was too naive, because the resulting relation refers only to types in one universe, whereas it ought to apply to types in any universe. I guess that means it has to be a module type (unless we want to depend on the join construction, the way CORS does, or restrict to accessible modalities).

On the plus side, I finally hacked through the universes in O_ind_from_inO_sigma and realized that ReflectiveSubuniverses_to_Modalities can actually instantiate Modalities after all.

So the hfiber of a X-coherent Y-functor should probably be itself a X-coherent Y-category. I'm not sure how this relates to notions of Grothendieck fibration,

As @fpvandoorn pointed out, the proof that loops commute with dependent pointed map is very slow. We should look into trying to speed it up.

I'll make note of this here in case I forget about it. We can construct the wild category of prespectra as a comma category of a functor F : (forall n:N, pType) -> (forall n:N, pType) where N is a successor structure and the identity functor. N ends up inducing an endofunctor on (forall n:N, pType) which takes (fun n => P n) and gives (fun n => P n.+1). F is then defined to take (fun n => P n) and give (fun n => loops (P n.+1)).

I wonder if there is a comma category like construction for equivalences instead of maps. Then it seems that spectra would be constructed this way. I also wonder what the relation with comma categories and comma categories with equivalences is. Are there other analogues of spectrification from this?

I just added the following lemma to the library:

Lemma pmap_pi_functor {X Y : pType} (f : X ->* Y) (n : nat) 
  : pi_functor_type_pmap (pi_functor (S n) f) ==* 
  ptr_functor 0 (iterated_loops_functor (S n) f).
Proof.
  srapply Build_pHomotopy. 1: reflexivity. apply path_ishprop.
Defined

Is it possible to redefine pi_functor so that these maps become definitionally equal? This would also ensure that the underlying maps of Pi_les are definitionally equal to the expected maps, e.g. that les_fn (Pi_les i f) (S n, 1) $== pi_functor (S n) i is true by reflexivity.

Every time I switch from the wildcat branch to the master branch, the leftover compiled WildCat/Square.vo gets mistakenly imported by Cubical/DSquare until I delete it. Let's at least merge a change that will stop that from happening.

First we'll have to merge master back into wildcat, which will require a bit of manual work.

There are a lot of choices as to how to go about that, each of which has different possible amounts of coherence:

• Equivalences of hom-functors
• Unit and counit with triangle identities
• Comma categories and universal arrows

To what extent are they equivalent? Which one(s) should we use?

As Egbert pointed out, a lot of the theory of reflective subuniverses should generalize. But we couldn't get the theory of reflective subuniverses itself as a special case, unless we did away with the modules there.

Should be useful for #22

Consider defining IsGraph (or maybe Is0Coh0Cat?) to have a Hom but no identities or composition yet. A 0-coherent 1-functor, and a 1-natural transformation, can be defined between these alone, and we use such things when talking about diagrams and (co)limits over graphs (#27).

Will be useful for to #22.

I am opening this issue as a discussion about the notions of equivalences in ooCat.v

It occurred to me earlier that if an ooCat has a terminal object and "pullbacks" (whatever that means), we could define a notion of "homotopy fiber". Then we could ask if a map's fibers are terminal in the category, which I think corresponds to equivalences by contractible fibers. This might be a more coherent notion of equivalence, at least for categories with hfibers.