We introduce fibred type-theoretic fibration categories which are fibred categories between categorical models of Martin-Lof type theory. Fibred type-theoretic fibration categories give a categorical description of logical predicates for identity …
We introduce fibred type-theoretic fibration categories which are fibred categories between categorical models of Martin-Lof type theory. Fibred type-theoretic fibration categories give a categorical description of logical predicates for identity types. As an application, we show a relational parametricity result for homotopy type theory. As a corollary, it follows that every closed term of type of polymorphic endofunctions on a loop space is homotopic to some iterated concatenation of a loop.
We introduce fibred type-theoretic fibration categories which are fibred categories between categorical models of Martin-Löf type theory. Fibred type-theoretic fibration categories give a categorical description of logical predicates for identity …
We introduce fibred type-theoretic fibration categories which are fibred categories between categorical models of Martin-Löf type theory. Fibred type-theoretic fibration categories give a categorical description of logical predicates for identity types. As an application, we show a relational parametricity result for homotopy type theory. As a corollary, it follows that every closed term of type of polymorphic endofunctions on a loop space is homotopic to some iterated concatenation of a loop.
We now proceed to set up a suitable abstract framework which contains all ingredients for constructing and describing algebraic models of homotopy theory. We aim at an axiomatization of the …
We now proceed to set up a suitable abstract framework which contains all ingredients for constructing and describing algebraic models of homotopy theory. We aim at an axiomatization of the minimal properties used to develop a homotopy theory. The category Top introduced in chapter 1 is a typical example of a cofibration category; actually, the axiomatization given below originated from the study of this category.
Cofibration categories are a formalization of homotopy theory useful for dealing with homotopy colimits that exist on the level of models as colimits of cofibrant diagrams. In this paper, we …
Cofibration categories are a formalization of homotopy theory useful for dealing with homotopy colimits that exist on the level of models as colimits of cofibrant diagrams. In this paper, we deal with their enriched version. Our main result claims that the category $[\mathcal{C},\mathcal{M}]$ of enriched diagrams equipped with the projective structure inherits a structure of a cofibration category whenever $\mathcal{C}$ is locally cofibrant (or, more generally, locally flat).
We generalise the usual notion of fibred category; first to fibred 2-categories and then to fibred bicategories. Fibred 2-categories correspond to 2-functors from a 2-category into 2-Cat. Fibred bicategories correspond …
We generalise the usual notion of fibred category; first to fibred 2-categories and then to fibred bicategories. Fibred 2-categories correspond to 2-functors from a 2-category into 2-Cat. Fibred bicategories correspond to trihomomorphisms from a bicategory into Bicat. We describe the Grothendieck construction for each kind of fibration and present a few examples of each. Fibrations in our sense, between bicategories, are closed under composition and are stable under equiv-comma. The free such fibration on a homomorphism is obtained by taking an oplax comma along an identity.
We generalise the usual notion of fibred category; first to fibred 2-categories and then to fibred bicategories. Fibred 2-categories correspond to 2-functors from a 2-category into 2-Cat. Fibred bicategories correspond …
We generalise the usual notion of fibred category; first to fibred 2-categories and then to fibred bicategories. Fibred 2-categories correspond to 2-functors from a 2-category into 2-Cat. Fibred bicategories correspond to trihomomorphisms from a bicategory into Bicat. We describe the Grothendieck construction for each kind of fibration and present a few examples of each. Fibrations in our sense, between bicategories, are closed under composition and are stable under equiv-comma. The free such fibration on a homomorphism is obtained by taking an oplax comma along an identity.
Synopsis The purpose of this paper is to introduce a fibrewise generalisation of category, in the sense of Lusternik–Schnirelmann. This reduces to the classical concept when the space is a …
Synopsis The purpose of this paper is to introduce a fibrewise generalisation of category, in the sense of Lusternik–Schnirelmann. This reduces to the classical concept when the space is a point. Fibrewise category may be compared with equivariant category, which has been the subject of some recent research [1,7,8]. Many variations on the basic idea of category have been discussed in the literature, for example the concept of category of a map, but since the generalisations to the fibrewise case are fairly routine they are not considered here.
These are notes about the theory of Fibred Categories as I have learned it from Jean B\'enabou. I also have used results from the Thesis of Jean-Luc Moens's from 1982 …
These are notes about the theory of Fibred Categories as I have learned it from Jean B\'enabou. I also have used results from the Thesis of Jean-Luc Moens's from 1982 in those sections when I discuss the fibered view of geometric morphisms. Thus, almost all of the contents is not due to me but most of it cannot be found in the literature since B\'enabou has given many talks on it but most of his work on fibered categories is unpublished.
But I am solely responsible for the mistakes and for misrepresentations of his views. And certainly these notes do not cover all the work he has done on fibered categories.
I just try to explain the most important notions he has come up with in a way trying to be as close as possible to his intentions and intuitions.
I started these notes in 1999 when I gave a course on some of the material at a workshop in Munich. They have developed quite a lot over the years and I have tried to include most of the things I want to remember.
In this article we shall show another proof of Iitaka-Viehweg conjecture([I],[Vieh]), on some part of which is the way that Mochizuki’s theory is applied. Secondly([Mch]), we consider global manifolds and …
In this article we shall show another proof of Iitaka-Viehweg conjecture([I],[Vieh]), on some part of which is the way that Mochizuki’s theory is applied. Secondly([Mch]), we consider global manifolds and a surjective morphism over a scheme from a product manifold onto a manifold with the automorphism group of general generic fibre algebraic. We apply Poincare-Segal n-groupoid to the situation above to prove that the latter manifold is also a product after a certain base-change([S3]).
We construct a flagged ∞-category Corr of ∞-categories and bimodules among them. We prove that Corr classifies exponentiable fibrations. This representability of exponentiable fibrations extends that established by Lurie of …
We construct a flagged ∞-category Corr of ∞-categories and bimodules among them. We prove that Corr classifies exponentiable fibrations. This representability of exponentiable fibrations extends that established by Lurie of both coCartesian fibrations and Cartesian fibrations, as they are classified by the ∞-category of ∞-categories and its opposite, respectively. We introduce the flagged ∞-subcategories LCorr and RCorr of Corr , whose morphisms are those bimodules which are left-final and right-initial , respectively. We identify the notions of fibrations these flagged ∞-subcategories classify, and show that these ∞-categories carry universal left/right fibrations.
We introduce a fibre homotopy relation for maps in a category of cofibrant objects equipped with a choice of cylinder objects.Weak fibrations are defined to be those morphisms having the …
We introduce a fibre homotopy relation for maps in a category of cofibrant objects equipped with a choice of cylinder objects.Weak fibrations are defined to be those morphisms having the weak right lifting property with respect to weak equivalences.We prove a version of Dold's fibre homotopy equivalence theorem and give a number of examples of weak fibrations.If the category of cofibrant objects comes from a model category, we compare fibrations and weak fibrations, and we compare our fibre homotopy relation, which is defined in terms of left homotopies and cylinders, with the fibre homotopy relation defined in terms of right homotopies and path objects.We also dualize our notion of weak fibration in a category of cofibrant objects to a notion of weak cofibration in a category of fibrant objects, and give examples of these weak cofibrations.A section is devoted to the case of chain complexes in an abelian category.
We construct a flagged $\infty$-category ${\sf Corr}$ of $\infty$-categories and bimodules among them. We prove that ${\sf Corr}$ classifies exponentiable fibrations. This representability of exponentiable fibrations extends that established by …
We construct a flagged $\infty$-category ${\sf Corr}$ of $\infty$-categories and bimodules among them. We prove that ${\sf Corr}$ classifies exponentiable fibrations. This representability of exponentiable fibrations extends that established by Lurie of both coCartesian fibrations and Cartesian fibrations, as they are classified by the $\infty$-category of $\infty$-categories and its opposite, respectively. We introduce the flagged $\infty$-subcategories ${\sf LCorr}$ and ${\sf RCorr}$ of ${\sf Corr}$, whose morphisms are those bimodules which are \emph{left final} and \emph{right initial}, respectively. We identify the notions of fibrations these flagged $\infty$-subcategories classify, and show that these $\infty$-categories carry universal left/right fibrations.
We construct a flagged $\infty$-category ${\sf Corr}$ of $\infty$-categories and bimodules among them. We prove that ${\sf Corr}$ classifies exponentiable fibrations. This representability of exponentiable fibrations extends that established by …
We construct a flagged $\infty$-category ${\sf Corr}$ of $\infty$-categories and bimodules among them. We prove that ${\sf Corr}$ classifies exponentiable fibrations. This representability of exponentiable fibrations extends that established by Lurie of both coCartesian fibrations and Cartesian fibrations, as they are classified by the $\infty$-category of $\infty$-categories and its opposite, respectively. We introduce the flagged $\infty$-subcategories ${\sf LCorr}$ and ${\sf RCorr}$ of ${\sf Corr}$, whose morphisms are those bimodules which are \emph{left final} and \emph{right initial}, respectively. We identify the notions of fibrations these flagged $\infty$-subcategories classify, and show that these $\infty$-categories carry universal left/right fibrations.
For spaces with a group action, we introduce Bredon cohomology with local (or twisted) coefficients and show that it is invariant under weak equivariant homotopy equivalence. We use this new …
For spaces with a group action, we introduce Bredon cohomology with local (or twisted) coefficients and show that it is invariant under weak equivariant homotopy equivalence. We use this new cohomology to construct a Serre spectral sequence for equivariant fibrations.
We prove Steinebrunner's conjecture on the biequivalence between (colored) properads and labelled cospan categories. The main part of the work is to establish a 1-categorical, strict version of the conjecture, …
We prove Steinebrunner's conjecture on the biequivalence between (colored) properads and labelled cospan categories. The main part of the work is to establish a 1-categorical, strict version of the conjecture, showing that the category of properads is equivalent to a category of strict labelled cospan categories via the symmetric monoidal envelope functor.
Proofs are traditionally syntactic, inductively generated objects. This paper reformulates first-order logic (predicate calculus) with proofs which are graph-theoretic rather than syntactic. It defines a combinatorial proof of a formula …
Proofs are traditionally syntactic, inductively generated objects. This paper reformulates first-order logic (predicate calculus) with proofs which are graph-theoretic rather than syntactic. It defines a combinatorial proof of a formula $ϕ$ as a lax fibration over a graph associated with $ϕ$. The main theorem is soundness and completeness: a formula is a valid if and only if it has a combinatorial proof.
Much Australian work on categories is part of, or relevant to, the development of higher categories and their theory. In this note, I hope to describe some of the origins …
Much Australian work on categories is part of, or relevant to, the development of higher categories and their theory. In this note, I hope to describe some of the origins and achievements of our efforts that they might perchance serve as a guide to the development of aspects of higher-dimensional work.
Higher Homotopy van Kampen Theorems allow some colimit calculations of certain homotopical invariants of glued spaces. One corollary is to describe homo- topical excision in critical dimensions in terms of …
Higher Homotopy van Kampen Theorems allow some colimit calculations of certain homotopical invariants of glued spaces. One corollary is to describe homo- topical excision in critical dimensions in terms of induced modules and crossed modules over groupoids. This paper shows how bred and cobred
In this study, we mainly show that the functor from the category X 2 Mod of 2‐crossed modules of groups to the category Groups of groups assigning to each 2‐crossed …
In this study, we mainly show that the functor from the category X 2 Mod of 2‐crossed modules of groups to the category Groups of groups assigning to each 2‐crossed module the group P , and to each 2‐crossed module morphism the group homomorphism f 0 is a fibration. In addition, we study some related properties.
Proofs Without Syntax [Hughes, D.J.D. Proofs Without Syntax. Annals of Mathematics 2006 (to appear), http://arxiv.org/abs/math/0408282 (v3). August 2004 submitted version also available: [35]] introduced polynomial-time checkable combinatorial proofs for classical …
Proofs Without Syntax [Hughes, D.J.D. Proofs Without Syntax. Annals of Mathematics 2006 (to appear), http://arxiv.org/abs/math/0408282 (v3). August 2004 submitted version also available: [35]] introduced polynomial-time checkable combinatorial proofs for classical propositional logic. This sequel approaches Hilbert's 24th Problem with combinatorial proofs as abstract invariants for sequent calculus proofs, analogous to homotopy groups as abstract invariants for topological spaces. The paper lifts a simple, strongly normalising cut elimination from combinatorial proofs to sequent calculus, factorising away the mechanical commutations of structural rules which litter traditional syntactic cut elimination. Sequent calculus fails to be surjective onto combinatorial proofs: the paper extracts a semantically motivated closure of sequent calculus from which there is a surjection, pointing towards an abstract combinatorial refinement of Herbrand's theorem.
The main purpose of this paper is, among other things, to study cotriple (co) homology defined on a fibred category, which includes a unified account of introducing products of various …
The main purpose of this paper is, among other things, to study cotriple (co) homology defined on a fibred category, which includes a unified account of introducing products of various derived functors, known or unknown, in a categorical setting.This approach is motivated by an attempt to find a suitable way, in relative homological algebra, of discussing the derived functors of a functor of two variables.In fact, this is done in this paper by considering cotriple (co) homology defined on a fibred product which is a subcategory of a product category.More precisely speaking, we introduce first a category 3e= (2), 31, Q)@,»,P) of fibred functors (T,0): (£, S3, P )->(?), 21, Q), which inherits the fibre wise properties of (2), 21, Q).Since a cotriple on the fibred category (£, S3, P) induces a cotriple on the category £?<? in the usual sense, relative homological algebra can be applied to 3 9 .Consider the situation where a fibred functor (T, 0) is defined on a fibred category (£, S3, P) into an abelian category (2), 21, Q) and a cotriple (G, E, A) is given on (3t, 93, P).Then the cotriple (co) homology Jt^(TG) can be defined as an object in £?$.Moreover, if the fibred categories are both multiplicative and if the functors G, T satisfy certain conditions involved in the multiplicative functors, then an external product can be defined on H*(TG).For applications, T is
Extract The first author dedicates this book to his wife, Nemili. The second author dedicates this book to Eun Soo and Jacqueline.
Extract The first author dedicates this book to his wife, Nemili. The second author dedicates this book to Eun Soo and Jacqueline.
Extract 2-Dimensional Categories The theory of 2-dimensional categories, which includes 2-categories and bicategories, is a fundamental part of modern category theory with a wide range of applications not only in …
Extract 2-Dimensional Categories The theory of 2-dimensional categories, which includes 2-categories and bicategories, is a fundamental part of modern category theory with a wide range of applications not only in mathematics but also in physics [BN96, KV94a, KV94b, KTZ20, Par18, SP∞], computer science [PL07], and linguistics [Lam04, Lam11]. The basic definitions and properties of 2-categories and bicategories were introduced by Bénabou in [Bén65] and [Bén67], respectively. The one-object case is illustrative: a monoid, which is a set with a unital and associative multiplication, is a one-object category. A monoidal category, which is a category with a product that is associative and unital up to coherent isomorphisms, is a one-object bicategory. The definition of a bicategory is obtained from that of a category by replacing the hom sets with hom categories, the composition and identities with functors,...
For spaces with a group action, we introduce Bredon cohomology with local (or twisted) coefficients and show that it is invariant under weak equivariant homotopy equivalence. We use this new …
For spaces with a group action, we introduce Bredon cohomology with local (or twisted) coefficients and show that it is invariant under weak equivariant homotopy equivalence. We use this new cohomology to construct a Serre spectral sequence for equivariant fibrations.
Abstract In this chapter, 2-categories and bicategories are defined, along with basic examples. Several useful unity properties in bicategories, generalizing those in monoidal categories and underlying many fundamental results in …
Abstract In this chapter, 2-categories and bicategories are defined, along with basic examples. Several useful unity properties in bicategories, generalizing those in monoidal categories and underlying many fundamental results in bicategory theory, are discussed. In addition to well-known examples, the 2-categories of multicategories and of polycategories are constructed. This chapter ends with a discussion of duality of bicategories.
Abstract We study the Yoneda lemma for arbitrary simplicial spaces. We do that by introducing left fibrations of simplicial spaces and studying their associated model structure, the covariant model structure …
Abstract We study the Yoneda lemma for arbitrary simplicial spaces. We do that by introducing left fibrations of simplicial spaces and studying their associated model structure, the covariant model structure . In particular, we prove a recognition principle for covariant equivalences over an arbitrary simplicial space and invariance of the covariant model structure with respect to complete Segal space equivalences.