TOC for fibred category theory

]]>From my phone, am in a talk, so just briefly:

That’s a good plan!

For the floating TOC just create a page as usual (say by requesting it from the Sandbox) with a title like fibred categories – contents.

To include it as a TOC, just copy and paste the include-code with the evident substitutions. I can help if you get stuck.

]]>Thanks. So I have appended pointer to *categorical semantics of dependent types*.

I'd start by creating a fibred category theory page in which to list some results and ideas.

Then I'd like to have a dropdown ToC like the one at the top right corner of category theory. How does one create this?

Then I'll slowly gather some pages around fibred category theory and make them a little more integrated with each other. For instance they'd all have the same dropdown.

Among them:

* Grothendieck fibration

* cleavage

* split fibration

* dual fibration

* definability (fibred category theory)

* etc.

There's also pages to be created, off the top of my head

* fibred adjunction

* fibred limits

* fibred Yoneda lemma

* comprehension category (in particular this one deserves its own page)

* 2-category of fibrations

* 2-fibration of fibrations

* etc.

Is it this ok to do? What else would you suggest to include? ]]>

Redirects opposite fibration

]]>added pointer to:

- Frank Quinn,
*Lectures on axiomatic topological quantum field theory*, in Dan Freed, Karen Uhlenbeck (eds.)*Geometry and Quantum Field Theory***1**(1995) [doi:10.1090/pcms/001]

Changed opening sentence as suggested by Urs

]]>Oh, I see. So I misread what you mean. (Haven’t take much time with the entry, admittedly).

But then lets’ say this in the entry: “whose objects are type families”.

And add a link to *category with families*! (or whatever it may be)

added pointer to

- Frank Quinn,
*Lectures on axiomatic topological quantum field theory*, in Dan Freed, Karen Uhlenbeck (eds.)*Geometry and Quantum Field Theory***1**(1995) [doi:10.1090/pcms/001]

added DOI and publication year to this item:

- Frank Quinn,
*Lectures on axiomatic topological quantum field theory*, in Dan Freed, Karen Uhlenbeck (eds.)*Geometry and Quantum Field Theory***1**(1995) [doi:10.1090/pcms/001]

and bruched-up the way it is referenced in the text.

]]>added cross-link with *classical modality*

added pointers for *infinitesimal cohesion* and *classical modality*

starting something on the modality of infinitesimal cohesion as it appears in linear homotopy type theory

]]>I have slightly re-worked and then considerably expanded the Idea section (here).

In particular I have added the following discussion:

But aspects of the proposal of O’Hearn & Pym (1999) and Pym (2002) have remained unsatisfactory, see Pym (2008), Errata to Pym (2002) and Riley(2022), pp. 19 and Rem. 1.4.1 (p. 64):

Riley 2022, pp. 19: [Since] context manipulations are not recorded in the terms, typechecking a term can be difficult. First, it is not always obvious when and how the contraction rule has to be applied, and secondly, it is not always obvious how the context has to be split into two pieces to apply $\multimap$-ELIM. Besides the challenge of typechecking, the combination of the weakening rule and the rules for the monoidal unit also breaks soundness for the intended semantics.

The various extensions of the αλ-calculus that have since appeared [BO06; CPR08; SS04; Atk04] do not resolve these issues. It is also not so clear how to add dependent types to this system and how dependency should behave between bunches.

In reaction to this, Riley (2022) proposes an enhanced form of bunched type theory which is claimed to fix all these problems at least in the case that the second structural connective $\otimes$ is a multiplicative conjunction in a linear type theory, hence for a form of dependent linear type theory. The key new ingredients in Riley (2022) to make this work are (1.) a classical modality $\natural$ which from any “parameterized linear type” projects out the underlying classical type and (2.) a decoration of bunched contexts by “color palettes” which keep explicit track of the bunching/tree structure. (On the other hand, especially the second point leads to a proliferation of inference rules, but maybe that’s what it takes.)

]]>

Gave the References-section a new subsection “Geometric refinement” (now here)

]]>added pointer to today’s:

- Hyungrok Kim, Christian Saemann,
*T-duality as Correspondences of Categorified Principal Bundles with Adjusted Connections*[arXiv:2303.16162]

The main link given

does not work for me: it gives me the “Potential Security Risk Ahead”-thing. I am sure somebody will tell me that I can work around this using a VPN or something, but is there a link which would just work?

The one alterntive (?) I could find is

which I have added. But as with most github pages, this doesn’t serve as a landing page for outsiders.

]]>added pointer to:

- Lukas Heidemann, David Reutter, Jamie Vicary,
*Zigzag normalisation for associative $n$-categories*, Proceedings of the Thirty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022) [arXiv:2205.08952, doi:10.1145/3531130.3533352]

Incidentally, most of the references listed do mention `homotopy.io`

(though not the first ones, which seem to be included just as background on associative $n$-categories?) but none of the references seems to be really *about* `homotopy.io`

as such.

brief `category:people`

-entry for hyperlinking references

added some “Selected writings”

]]>I have touched the formatting and hyperlinking of the list of “Selected writings”.

Notice that in the item

- Christoph Dorn,
*Associative $n$-categories*, talk at*103rd Peripatetic Seminar on Sheaves and Logic*(pdf).

(which appears in several other entries)

both links are broken: They both end up on Fosco Loregian’s home page.

]]>Deep down in this entry was a line saying that Globular “will soon be followed by a succesor tool *homotopy.io*”. I don’t really know about any of this, but it looks like *homotopy.io* long exists and may be preferred by users, so I moved that line to the very top of the entry.

In the process I noticed that there was not a single mention of “associative n-categories” on this page, while *homotopy.io* claims it’s all about that notion. So I added the pointer to “associative n-categories” also to the first sentence of “Overview” here.