2-truncated quasicategories and homotopy relations #
We define 2-truncated quasicategories Quasicategory₂ by three horn-filling properties,
and the left and right homotopy relations HomotopicL and HomotopicR on the edges in a
2-truncated simplicial set.
We prove that for 2-truncated quasicategories, both homotopy relations are equivalence relations, and that the left and right homotopy relations coincide.
For a 2-truncated quasicategory X, we define a category HomotopyCategory₂ X whose
morphisms are given by (left) homotopy classes of edges. The construction of this category
is different from HomotopyCategory X in AlgebraicTopology.SimplicialSet.HomotopyCat:
HomotopyCategory₂ Xhas morphisms given by homotopy classes of edgesHomotopyCategory Xhas morphisms given by equivalence classes of paths in the underlying reflexive quiver ofX.
The two constructions agree for 2-truncated quasicategories (TODO: handled by future PR).
Implementation notes #
Throughout this file, we make use of Edge and CompStruct to conveniently deal with
edges and triangles in a 2-truncated simplicial set.
A 2-truncated quasicategory is a 2-truncated simplicial set with the properties:
- (2, 1)-filling: given two consecutive
Edgese₀₁ande₁₂, there exists aCompStructwith (0, 1)-edgee₀₁and (0, 2)-edgee₁₂. - (3, 1)-filling: given three
CompStructsf₃,f₀andf₂which form a (3, 1)-horn, there exists a fourthCompStructsuch that the four faces form the boundary ∂Δ[3] of a 3-simplex. - (3, 2)-filling: given three
CompStructsf₃,f₀andf₁which form a (3, 2)-horn, there exists a fourthCompStructsuch that the four faces form the boundary ∂Δ[3] of a 3-simplex.
- fill31 {x₀ x₁ x₂ x₃ : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₂₃ : Edge x₂ x₃} {e₀₂ : Edge x₀ x₂} {e₁₃ : Edge x₁ x₃} {e₀₃ : Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₂ : e₀₁.CompStruct e₁₃ e₀₃) : Nonempty (e₀₂.CompStruct e₂₃ e₀₃)
- fill32 {x₀ x₁ x₂ x₃ : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₂₃ : Edge x₂ x₃} {e₀₂ : Edge x₀ x₂} {e₁₃ : Edge x₁ x₃} {e₀₃ : Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₁ : e₀₂.CompStruct e₂₃ e₀₃) : Nonempty (e₀₁.CompStruct e₁₃ e₀₃)
Instances
A left homotopy between two edges f and g is a CompStruct f (id _) g.
(See HomotopicL for the Prop-valued version.)
Equations
- f.HomotopyL g = f.CompStruct (SSet.Truncated.Edge.id x₁) g
Instances For
A right homotopy between two edges f and g is a CompStruct (id _) f g.
(See HomotopicL for the Prop-valued version.)
Equations
- f.HomotopyR g = (SSet.Truncated.Edge.id x₀).CompStruct f g
Instances For
Two edges f and g are left homotopic if there is a CompStruct with
(0, 1)-edge f, (1, 2)-edge Edge.id and (0, 2)-edge g. We use Nonempty to
have a Prop valued HomotopicL.
Equations
- SSet.Truncated.HomotopicL f g = Nonempty (f.HomotopyL g)
Instances For
Two edges f and g are right homotopic if there is a CompStruct with
(0, 1)-edge Edge.id, (1, 2)-edge f, and (0, 2)-edge g. We use Nonempty to
have a Prop valued HomotopicR.
Equations
- SSet.Truncated.HomotopicR f g = Nonempty (f.HomotopyR g)
Instances For
The left homotopy relation on the edges of a 2-truncated simplicial set is reflexive.
Instances For
The right homotopy relation on the edges of a 2-truncated simplicial set is reflexive.
Instances For
The associativity of the composition in a 2-truncated quasicategory.
Equations
- SSet.Truncated.Edge.assoc h₀₂ h₁₃ h = ⋯.some
Instances For
The associativity of the composition in a 2-truncated quasicategory.
Equations
- SSet.Truncated.Edge.assoc' h₀₂ h₁₃ h = ⋯.some
Instances For
In a 2-truncated quasicategory, the left homotopy relation on edges
is symmetric.
Equations
Instances For
In a 2-truncated quasicategory, the right homotopy relation on edges
is symmetric.
Equations
Instances For
In a 2-truncated quasicategory, the left homotopy relation on edges
is transitive.
Equations
- h₁.trans h₂ = SSet.Truncated.Edge.assoc' h₁ (SSet.Truncated.Edge.CompStruct.idCompId x₁) h₂
Instances For
In a 2-truncated quasicategory, the right homotopy relation on edges
is transitive.
Equations
- h₁.trans h₂ = SSet.Truncated.Edge.assoc (SSet.Truncated.Edge.CompStruct.idCompId x₀) h₁ h₂
Instances For
In a 2-truncated quasicategory, two left homotopic edges are
also right homotopic.
Equations
Instances For
In a 2-truncated quasicategory, two right homotopic edges are
also left homotopic.
Equations
Instances For
The left homotopy relation is reflexive.
The left homotopy relation is symmetric.
The left homotopy relation is transitive.
The right homotopy relation is reflexive.
The right homotopy relation is symmetric.
The right homotopy relation is transitive.
In a 2-truncated quasicategory, left homotopy implies right homotopy.
In a 2-truncated quasicategory, right homotopy implies left homotopy.
In a 2-truncated quasicategory, the right and left homotopy relations coincide.
Assume we have structures CompStruct f g h and CompStruct f' g' h'.
If f and f' are left homotopic, and g and g' are left homotopic,
then h and h' are left homotopic.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given CompStruct f g h and CompStruct f' g' h' with the same vertices and edges such
that f ≃ f' and g ≃ g', then the long diagonal edges h and h' are also homotopic.
Given two consecutive edges f, g in a 2-truncated quasicategory, nonconstructively choose
an edge that is the diagonal of a 2-simplex with spine given by f and g. The CompStruct
witnessing this property is given by Edge.compStruct.
Instances For
See Edge.comp
Equations
- f.compStruct g = ⋯.some.snd
Instances For
The homotopy category of a 2-truncated quasicategory X has as objects the vertices of X
- pt : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
An object of the homotopy category is a vertex of
X.
Instances For
Left homotopy is an equivalence relation on the edges of X.
Remark: We could have equivalently chosen right homotopy, as shown by homotopicL_iff_homotopicR.
Equations
- SSet.Truncated.instSetoidEdge x y = { r := SSet.Truncated.HomotopicL, iseqv := ⋯ }
The morphisms between two vertices x, y in HomotopyCategory₂ X are homotopy classes
of edges between x and y.
Instances For
Composition of morphisms in HomotopyCategory₂ X is given by lifting the edge
chosen by composeEdges.
Equations
- One or more equations did not get rendered due to their size.
The function HomotopyCategory₂.mk taking a vertex of A and sending it to the corresponding
object of HomotopyCategory₂ A is surjective.
Any edge in the 2-truncated simplicial set X defines a morphism in the homotopy category
by taking its equivalence class.
Equations
Instances For
Every morphism in the homotopy category HomotopyCategory₂ X is the equivalence class of
an edge of A.
The trivial (degenerate) edge at a vertex x is a representative for the
identity morphism x ⟶ x.
Left homotopic edges represent the same morphism in the homotopy category.
Right homotopic edges represent the same morphism in the homotopy category.
A CompStruct f g h is a witness for the fact that the morphisms represented by
f and g compose to the morphism represented by h.
If we have a factorization homMk f ≫ homMk g = homMk h, this is the choice
of a structure CompStruct f g h.
Equations
Instances For
Given edges f, g and h of a 2-truncated quasicategory,
there exists a structure CompStruct f g h iff
homMk f ≫ homMk g = homMk h holds in the homotopy category.
Equations
- SSet.Truncated.instCategoryHomotopyCategory₂ = { toCategoryStruct := SSet.Truncated.HomotopyCategory₂.instCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }
Auxiliary definition for SSet.Truncated.HomotopyCategory₂.desc.
Equations
- SSet.Truncated.HomotopyCategory₂.descMap obj map map_id map_comp f = Quot.lift map ⋯ f
Instances For
Constructor for functors from SSet.Truncated.HomotopyCategory₂.
Equations
- One or more equations did not get rendered due to their size.