Table of contents:
- A. Universe of left fibrations as higher category of spaces
- B. Finite completeness of universe of left fibrations
- C. Finite limits from terminal objects and pullbacks
A. Universe of left fibrations as higher category of spaces
===========================================================
The universe of left fibrations should model the higher category of spaces.
To see this, we prove a series of useful facts.
Recall the universe U = U_left : SSet_m of left fibratons.
It comes with left fibrant El : Ty_{SSet_m,rf}(U).
It can be defined by restricting the universe of Reedy fibrations as follows.
At level n, given matching data A : M_n U, we keep only those A_n : (M_n El)(A) → ty for which the composite projection
(a : (M_n El)(A)) × A(a) → (M_n El)(A) → A_0
induced by {0} → ∂Δ^n → Δ^n is an equivalence (trivial fibration).
Lemma A.1.
The universe U of left fibrant objects is a complete Segal type.
Proof.
We first show that it is a Segal type, i.e. inner fibrant.
Let us not worry about special outer horns here and only consider inner horns.
We check Λ^n_k → Δ^n ⊥ U for 0 < k < n.
That is, given X : Λ^n_k → U, want (hom)(Λ^n_k → Δ^n, U)(X) contractible.
We compute
(hom)(Λ^n_k → Δ^n, U)(X)
= (A : U_{n-1}(X|∂Δ^{[n]-k})) × (B : U_n(X, A))
= [ A : (M_{n-1} El)(X|∂Δ^{[n]-k}) → ty
, (a₀ : El(X|0)) → is-contr (hom)({0} → Δ^{[n]-k}, El)((X|Δ^{[n]-k}, A), a)
, B : (M_n El)(X, A) → ty
, (a₀ : El(X|0)) → is-contr (hom)({0} → Δ^n, El)((X, A, B), a)
]
= (a₀ : El(X|0)) →
[ A : (hom)({0} → ∂Δ^{[n]-k}, El)(X|∂Δ^{[n]-k}, a₀) → ty
, A representable
, B : (hom)({0} → ∂Δ^n, El)((X, A), a) → ty
, B representable
]
where P : C → ty is said to be representable if (c : C) × P(c) is contractible.
Note that we have used k > 0 in the above chain of equations to ensure that the initial vertices of Δ^{[n]-k} and Δ^n coincide.
It suffices to show given a₀ : El(X|0) that the inner expression is contractible.
We compute
[ A : (hom)({0} → ∂Δ^{[n]-k}, El)(X|∂Δ^{[n]-k}, a₀) → ty
, A representable
, B : (hom)({0} → ∂Δ^n, El)((X, A), a) → ty
, B representable
]
= [ A : (hom)({0} → ∂Δ^{[n]-k}, El)(X|Δ∂^{[n]-k}, a₀) → ty
, A representable
, B : [ M : (hom)({0} → ∂Δ^{[n]-k}, El)(X|∂Δ^{[n]-k}, a₀)
, N : (hom)(∂Δ^{[n]-k} → Δ^{[n]-k}, El)((X|∂Δ^{[n]-k}, A), (a₀, M))
, O : (hom)(∂Δ^{[n]-k} → Λ^n_k, El)(X, (a₀, M))
] → ty
, B representable
].
Note that the Σ-type of M and O as above, given by
(hom)({0} → Λ^n_k, El)(X, a₀),
is contractible.
Indeed, since k < n, we have {0} → Λ^n_k ∈ Cell(J_left) and J_left ⊥ El.
The claim now follows from Lemma A.2 below.
To finish the check that U is a complete Segal type, it remains to identify the invertible edges and check completeness.
For this, we use a more explicit description of the lowest levels of U.
Consider the following Reedy fibrant type over Δ_+^{≤2}:
- V₀ = ty
- V₁(A₀, A₁)
≃ A₀ → A₁
- V₂( A_i for 0 ≤ i ≤ 2,
, f_ij : A_i → A_j for 0 ≤ i < j ≤ 2
) ≃ (a₀ : A₀) → f₁₂(f₀₁(a₀)) = f₀₂(a₀).
It is straightforward to check that V ≃ U|^{≤2}.
In V, the invertible edges are given by equivalences:
V₁^inv(A₀, A₁, f : A₀ → A₁) = is-equiv f.
Completeness is thus exactly univalence.
□
Lemma A.2.
Let B : A → U be representable.
Then the dependent sum of
P : A → U representable
and
Q : (a : A) (p : P(a)) (b : B(a)) → U representable
is contractible.
Proof.
Since P is representable, the type of (P, Q) as above is equivalent to
P : A → U representable
Q : (b : B()) → U representable.
By Yoneda applied to P, this is equivalent to
a : A
Q : (b : B(a)) → U representable.
By Yoneda applied to Q, this is equivalent to
a : A
b : B(a).
This is contractible since B is representable.
□
The universe ty of fibrant types has the structure of a semicategory:
- the fibrant types of objects is ty
- the fibrant type of morphisms from X to Y is X → Y.
(If fibrant exponentials have η, then this has the structure of a category.)
We take the nerve N ty of this semicategory, resulting in a levelwise fibrant semisimplicial type.
It thus makes sense to talk about Reedy fibrant replacements of N ty.
Lemma A.3.
Any fibrant replacement V of N ty is inner fibrant.
Proof.
Consider 0 < a < n.
Recall that {0, …, n} is the pushout of {a} → {0, …, a} and {a} → {a, …, n} in Δ_+.
This pushout is not preserved under Yoneda.
Let instead D → Δ^n denote the pushout corner map in its image under Yoneda, i.e.
D = Δ^{0,…,a} +_{Δ^{a}} Δ^{a, …, n}.
To show that V is inner fibrant, it suffices to prove that D ⊥ V.
This means that
V_{0, …, n} --> V_{0, …, a}
| |
V_{a, …, n} --> V_{a}
should be a homotopy pullback in fibrant types.
Since V was constructed as a Reedy fibrant replacement, this square is equivalent to
(N ty)_{0, …, n} --> (N ty)_{0, …, a}
| |
(N ty)_{a, …, n} --> (N ty)_{a}.
As for any nerve, this is a strict pullback.
Since the maps into (N ty)_{a} are additionally fibrations, it is also a homotopy pullback.
The claim now follows by invariance of homotopy pullbacks under equivalence.
□
Lemma A.4.
Let e : N ty → V be a Reedy fibrant replacement.
Then V\e₀(1) → V is a left fibration.
Its classifying map c : V → U is an equivalence.
Proof.
Lemma A.3 showed that V is inner fibrant.
It follows that V\e₀(1) → V is a left fibration.
It thus has a classifying map c : V → U that witnesses V\e₀(1) → V as a strict pullback of U.El → U.
To show that c : V → U is an equivalence, it thus suffices to verify this on levels 0 and 1.
This means to check that the following maps are equivalences:
- c₀ : V₀ → U₀
c₀(X) = V₁(e₀(1), X),
- c₁ : V₁(X, Y) → U₁(c₀(X), c₀(Y))
c₁(f)(x, y) = V₂(f, y, x).
Since N ty → V is a Reedy fibrant replacement, we have equivalences.
e₀ : ty ≃ V₀,
e₁ : A → B ≃ V₁(e₀ A, e₀ B),
e₂ : (a : A) → g(f(a)) = h(a) ≃ V₂(e₀ A, e₀ B, e₀ C, e₁ f, e₁ g, e₁ h).
Under these equivalences, the previous maps become
- c₀ : ty → U₀
c₀(X) = 1 → X,
- c₁ : (X → Y) → U₁(1 → X, 1 → Y)
c₁(f)(x, y) = (* : 1) → f (x ⋆) = y ⋆.
Under the equivalence 1 → X ≃ X, these become:
- c₀ : V₀ → U₀
c₀(X) = X,
- c₁ : V₁(X, Y) → U₁(X, Y)
c₁(f)(x, y) = f x = y.
These are clearly equivalences.
□
Lemma A.5.
The universe U of left fibrant objects is a Reedy fibrant replacement of N ty.
Proof.
Let N ty → V be an arbitrary Reedy fibrant replacement.
By Lemma A.4, we have an equivalence V → U.
This shows that U is a Reedy fibrant replacement of N ty as well.
□
Remark A.6.
Note that the induced map N ty → U sends the object 1 to a contractible type.
Using Lemma A.4, it thus follows that U\1 → U is a strict pullback U.El → U along an equivalence.
In particular, the maps U\1 → U and U.El → U are equivalent.
Since U is univalent, one may use U\1 → U just as well as a classifying map (in the sense of complete Segal types) for left fibrations.
□
B. Finite completeness of universe of left fibrations
=====================================================
We present two approaches to the following claim.
Lemma B.1.
The universe U of left fibrations is finitely complete.
The first approach one is self-contained.
The second one depends on Section F (which is general, not depending on this section).
Recollection: finite limits in complete Segal types
---------------------------------------------------
We recall the cone operation on complete Segal types.
Fix a simplicial type K.
Let first X just be a simplicial type.
Given a diagram d : K → X, we have a simplicial type X/d.
This is the action of the right adjoint to - * K : SSet → SSet\K.
In particular, an n-simplex in X/d is a map Δ^n ⋆ K → X that restricts to d on K.
This operation lifts to types in the cwf SSet.
Given X : SSet, d : K → X, Y : Ty_SSet(X), and e : Tm_SSet(K, Y d), we have
Y/e : Ty_SSet(X/d)
defined as
(Y/e)_n(x : Δ^n ⋆ K → X restricting to d on K)
= Tm_SSet(Δ^n ⋆ K, Y x) restricting to e on K
= (hom)(K → Δ^n ⋆ K, Y)(x, e)
If you think of types Y in SSet via their comprehension X.Y → X, this is the functorial action of the cone operation SSet\K → SSet.
Note that t : Tm_SSet(X, Y) gives rise to Tm_SSet(X/d, Y/(t d)).
We have the same operation in SSet_m for marked semisimplicial types K.
Let K now be finite (meaning that 0 → K is in Cell(I)).
In that case, the cone operation interacts well with Reedy fibrancy:
- if X is Reedy fibrant, then so is X/d,
- if Y is Reedy fibrant, then so is Y/e,
- if X is a complete Segal type, then so is X/d,
- if Y is inner fibrant, then so is Y/e.
A complete Segal space X is said to be /finitely complete/ (i.e. have finite limits) if X/d has a terminal object for each finite diagram d : K → X.
First approach
--------------
Proof of Lemma B.1.
We verify that U has finite limits.
For this, let d : K → U be a finite diagram.
We have to find a terminal object in U/d.
We have El d : Ty_{SSet_m,rf}(K).
Since K is finite, L = Tm_{SSet_m}(K, El d) is fibrant.
In the remainder, we will construct an equivalence U/d ≃ U/L.
Since U/L is a slice category, it has a terminal object.
Then U/d does as well, and we will be finished.
Both U/d and U/L come with a forgetful map to U.
We construct a map f : U/d → U/L over U.
On level 0, we are given A : Δ⁰ ⋆ K → U restricting to d on K.
We take
f₀(A)₁ = A|Δ⁰
f₀(A)₂(a, l)
= λ(a, l). (hom)(Δ⁰ + K → Δ⁰ ⋆ K, El)(A, (a, l))
= λ(a, l). .
Note that fixing a : A|0, the Σ-type of l and f₀(A)₂(a, l) is contractible as required.
This is an instance of Δ⁰ → Δ⁰ ⋆ K ⊥ El, which holds since Δ⁰ → Δ⁰ ⋆ K ∈ Cell(J_left).
On level 1, we are given A : Δ¹ ⋆ K → U restricting to d on K.
We define
f₁(A)₁(a₀, a₁) = A|Δ¹(a₀, a₁)
f₁(A)₂(a₀, a₁, a₀₁, l, r₀, r₁)
= (hom)(∂Δ¹ ⋆ K ∪ Δ¹ → Δ¹ ⋆ K, El)(A, a₀, a₁, a₀₁, l, r₀, r₁)
=
Note that fixing a₀ : A|0, the Σ-type of a₁, a₀₁, l, r₀, r₁ and f₁(A)₂(a₁, a₀₁, l, r₀, r₁) is contractible as required.
This is an instance of {0} → Δ¹ ⋆ K ⊥ El, which holds since
- {0} → {0} ⋆ K ∈ Cell(J_left),
- {0} ⋆ K → Δ¹ ⋆ K ∈ Cell(J_left) (J_left is stable under - ⋆ K).
In general, on level n, we are given A : Δ^n ⋆ K → U restricting to d on K.
We define
f_n(A)₁(a : Tm(∂Δ^n, El A)) = A|Δ^n(a)
f_n(A)₂(a : Tm(∂Δ^n ⋆ K ∪ Δ^n, El A))
= (hom)(∂Δ^n ⋆ K ∪ Δ^n → Δ^n ⋆ K)(A, a)
= B
| |[f]
C --[g]-> D
be a (strict) pullback of complete Segal types.
Assume that:
- B and C have terminal objects,
- D has binary products,
- B → D and C → D are right fibrations.
Then A has a terminal object.
Think of right fibrations over D as presheaves over D.
The pullback A models the product of the presheaves B and C.
The lemma then says that if the base D has binary products, then representable presheaves are closed under binary products.
This can be seen as a special case of the fact that the higher Yoneda functor preserves limits.
Proof of Lemma C.1.
Without loss of generality, we identify
A₀ = [d : D₀ , b : B₀ , c : C₀ , f b = d , g c = d]
(with all equalities strict) and similarly for higher cells.
We take terminal objects
t_B : B₀
t_C : C₀.
We take the product of f t_B and g t_c in D:
d : D₀
u : D₁(d, f t_B)
v : D₁(d, g t_C)
Since B → D and C → D are right fibrations, we have lifts
b : B₀ with f b = d
u' : B₁(b, t_B) with f u' = u
and
c : C₀ with g c = d
v' : C₁(c, t_C) with g v' = v.
We claim that (d, b, c) : A₀ is terminal.
Let (d', b', c') : A₀ be arbitrary.
We compute via insertions and deletions of contractible singletons
A₁((d', b', c'), (d, b, c))
= [ d₀₁ : D₁(d', d)
, b₀₁ : B₁(b', b) over d₀₁ via f
, c₀₁ : C₁(c', c) over d₀₁ via g
]
≃ (taking the composite of d₀₁ with the span in D (insertion))
[ d₀₁ : D₁(d', d)
, x : D₁(d', f t_B)
, x-coh : D₂(d₀₁, u, x)
, y : D₁(d', g t_C)
, y-coh : D₂(d₀₁, v, y)
, b₀₁ : B₁(b', b) over d₀₁ via f
, c₀₁ : C₁(c', c) over d₀₁ via g
]
≃ (using that f and g are right fibrations (insertion then deletion))
[ d₀₁ : D₁(d', d)
, x : D₁(d', f t_B)
, x-coh : D₂(d₀₁, u, x)
, y : D₁(d', g t_C)
, y-coh : D₂(d₀₁, v, y)
, b₀₁ : B₁(b', t_B) over x via f
, c₀₁ : C₁(c', t_C) over y via g
]
≃ (using the universal property of the product in D, we contract d₀₁ with the coh-terms (deletion))
[ x : D₁(d', f t_B)
, y : D₁(d', g t_C)
, b₀₁ : B₁(b', t_B) over x via f
, c₀₁ : C₁(c', t_C) over y via g
]
=
[ b₀₁ : B₁(b', t_B)
, c₀₁ : C₁(c', t_C)
]
≃ (since t_B and t_C are terminal)
1.
□
Lemma C.1b.
Let X be a complete Segal type.
If X has pullbacks and terminal objects, it has binary products.
Proof.
We compute the product of a, b : X₀.
Let t : X₀ be terminal.
From terminality, we get
f : X₁(a, t)
g : X₁(b, t).
We take the pullback
p : X₀
u : X₁(p, a)
v : X₁(p, b)
w : X₁(p, t)
α : X₂(u, f, w)
β : X₂(v, g, w).
We claim that (p, u, v) : (X/(a, b))₀ is terminal
Let (p', u', v') : (X/(a, b))₀, that is
p' : X₀
u' : X₁(p', a)
v' : X₁(p', b),
be arbitrary.
Since t is terminal, we have
w' : X₁(p', t)
α' : X₂(u', f, w')
β' : X₂(v', g, w').
We compute via insertions and deletions of contractible singletons
(X/(a, b))₁((p', u', v'), (p, u, v))
= [ p₀₁ : X₁(p', p)
, u₀₁ : X₂(p₀₁, u, u')
, v₀₁ : X₂(p₀₁, v, v')
]
≃ (since t is terminal)
[ p₀₁ : X₁(p', p)
, u₀₁ : X₂(p₀₁, u, u')
, v₀₁ : X₂(p₀₁, v, v')
, w₀₁ : X₂(p₀₁, w, w')
, α₀₁ : X₃(α, α', w₀₁, u₀₁)
, β₀₁ : X₃(β, β', w₀₁, v₀₁)
]
≃ (using the universal property of the pullback)
1.
□
Lemma C.2.
Let j : A → B be in Cell(J_{left,m}).
Let X be a complete Segal type.
Then for any map d : B → X, the induced map X/d → X/dj is an equivalence.
Proof.
A standard adjointness argument using the join.
□
Lemma C.3.
Let X be a complete Segal type.
For any finite diagram d : K → X, the forgetful map p : X/d → X lifts pullbacks.
In particular, if X has pullbacks, then so does X/d.
Proof.
Let D = (Δ⁰ + Δ⁰) ⋆ Δ⁰ be the shape for pullbacks.
Consider a diagram f : D → X/d.
Assume that the induced diagram pf : D → X has a limit.
We will show that it extends to a limit of f.
By functoriality, p : X/d → X induces p/f : (X/d)/f → X/pf.
We wish to show that p/f lifts terminal objects.
Note that (X/d)/f is isomorphic to X/f where f is seen as f : D ⋆ K → X.
The map p/f corresponds under this to the map X/i : X/f → X/pf induced functorially from i : D → D ⋆ K.
We claim that X/i is an equivalence.
This follows Lemma C.2 and i ∈ J_left.
Indeed, in augmented semisimplicial types, the map i : D → D ⋆ K decomposes as the Leibniz join of
- 0 → Δ⁰ + Δ⁰
- 0 → Δ⁰
- Δ^{-1} → K.
Maps in J_left are stable under Leibniz join with monomorphisms on either side.
Thus, it will be enough to justify that the Leibniz join of 0 → Δ⁰ and Δ^{-1} → K is in J_left.
This holds by saturation: for any boundary inclusion ∂Δ^n → Δ^n with n ≥ 0, the Leibniz join of 0 → Δ⁰ and ∂Δ^n → Δ^n is Λ^{n+1}_0 → Δ^n, a map in J_left.
□
Recall that a marked semisimplicial type K is /finite/ if the map 0 → K lies in Cell(I) where I_m is the family of boundary inclusions (and the marking inclusion Δ¹ → Δ¹_m).
We call a marked semisimplicial type K /loop-free/ if any map Δ^n → K is monic.
We can give an explicit description of what it means for a finite marked semisimplicial type K to be loop-free.
In the cell complex presentation
0 = K₀ → K₁ → … -> K_n = K
of K with pushouts
A_i --> K_i
| |
B_i --> K_{i+1}
for all 0 ≤ i < n where A_i → B_i is in I_m, the attaching maps A_i → K_i have to be monic.
With Lemmas C.1, C.1b, and C.3 in hand, we can now show a preliminary version of the claim of the section.
Lemma C.4.
Let X be a complete Segal type with terminal object and pullbacks.
Then X has limits of loop-free finite shapes.
Proof.
We show by induction on m that d : K → X has a limit for K finite and loop-free and dim K < m.
Note that it does not matter here if K is a marked semisimplicial type or just a semisimplicial type.
The base case m = 0 is given by the terminal object in X.
In the induction step, we induct on the cellular presentation of K given by finiteness.
The base case is covered by the case m = 0.
In the successor case, we consider a pushout
∂Δ^n --> K
| |
Δ^n ---> K'
and a diagram d : K' → X.
By loop-freeness, the top map is monic (hence so are all maps).
The above pushout induces a pullback
X/d -------> X/{d|Δ^n}
| (1) |
X/{d|K} ---> X/{d|∂Δ^n}.
where all maps are right fibrations.
By induction hypothesis, X has limits of d|∂Δ^n (outer induction) and d|K (inner induction).
Note that X/{d|Δ^n} → X/{d|0} is an equivalence.
A slice complete Segal space always has a terminal object.
Thus, also d|Δ^n has a limit.
We thus get terminal objects in all but the top left corner in (1).
The map X/{d|∂Δ^n} → X lifts pullbacks by Lemma C.3.
From this, we get products in X/{d|∂Δ^n} by Lemma C.1b.
The claim then follows by Lemma C.1.
□
Lemma C.4.
Every finite marked semisimplicial type K has a finite loop-free replacement.
Explicitly, there is loop-free K' and a cospan of maps K → • ← K' in Cell(J_{inner,m}).
Proof.
We take K' = N ∫ K.
Here:
- ∫ X denotes the marked semicategory of elements of a marked semisimplicial type X.
It produces the marked semicategory as follows.
The objects are the elements of X.
The maps from x : X_m to y : X_n are maps f : [m] → [n] such that x = y.
A map f as above is marked if:
* f preserves the terminal object,
* or else the induced edge y|{f(m), n} is marked.
- N C denotes the marked semisimplicial nerve of a marked semicategory C.
Its underlying semisimplicial type is the nerve of C.
An edge is marked if the morphism in C it came from is marked.
Note that ∫ K is a finite semicategory, hence N ∫ K is a finite marked semisimplicial type.
One can produce a finite marked semisimplicial type Q with maps K → Q and N ∫ K → Q that both lie in Cell(J_{inner,m}).
For details on this construction, see [1]:
- [1] Constructive homotopy theory of marked semisimplicial sets
https://arxiv.org/abs/1809.11168.
Call a semicategory /loop-free/ if it does not have any loops.
Since Δ_+ is loop-free, so is ∫ K.
Evidently, the nerve of a loop-free marked semisimplicial category is a loop-free marked semisimplicial type.
□
Now we can finally show the main claim.
Lemma C.5.
Let X be a complete Segal type.
Assume that X has a terminal object and pullbacks.
Then X has finite limits.
Proof.
Let d : K → X be a finite diagram.
By Lemma C.4, we have a loop-free replacement of K by a finite marked semisimplicial type K', related to K by maps
u : K → Q
v : K' → Q
in J_{inner,m}.
Since X is inner fibrant, d extends to d' : Q → X such that d' u = d.
Applying Lemma C.2 twice, we have
X/d ≃ X/d' ≃ X/(d'v).
Thus, d has a limit if d'v has a limit.
But the latter is a diagram of loop-free finite shape K'.
Thus, it has a limit by Lemma C.4.