Pre-∞-categories (Segal types)¶
These formalisations correspond to Section 5 of the RS17 paper.
Segal types vs pre-∞-categories
Riehl and Shulman refer to "Segal types" in RS17, but here we call them "pre-∞-categories".
This is a literate rzk file:
Prerequisites¶
hott/1-paths.md- We require basic path algebra.hott/2-contractible.md- We require the notion of contractible types and their data.hott/total-space.md— We rely onis-equiv-projection-contractible-fibersandtotal-space-projectionin the proof of Theorem 5.5.3-simplicial-type-theory.md— We rely on definitions of simplicies and their subshapes.4-extension-types.md— We use the fubini theorem and extension extensionality.
Some of the definitions in this file rely on function extensionality and extension extensionality:
Hom types¶
Extension types are used to define the type of arrows between fixed terms:
RS17, Definition 5.1
#def hom
( A : U)
( x y : A)
: U
:=
( t : Δ¹)
→ A [ t ≡ 0₂ ↦ x , -- the left endpoint is exactly x
t ≡ 1₂ ↦ y] -- the right endpoint is exactly y
Extension types are also used to define the type of commutative triangles:
RS17, Definition 5.2
#def hom2
( A : U)
( x y z : A)
( f : hom A x y)
( g : hom A y z)
( h : hom A x z)
: U
:=
( ( t₁ , t₂) : Δ²)
→ A [ t₂ ≡ 0₂ ↦ f t₁ , -- the top edge is exactly `f`,
t₁ ≡ 1₂ ↦ g t₂ , -- the right edge is exactly `g`, and
t₂ ≡ t₁ ↦ h t₂] -- the diagonal is exactly `h`
#def long-edge-2-simplex
( A : U)
( α : Δ² → A)
: Δ¹ → A
:= \ t → α (t , t)
The Segal condition¶
A type is a pre-∞-category if every composable pair of arrows has a unique composite. Note this is a considerable simplification of the usual Segal condition, which also requires homotopical uniqueness of higher-order composites.
RS17, Definition 5.3
#def is-pre-∞-category
( A : U)
: U
:=
( x : A) → (y : A) → (z : A)
→ ( f : hom A x y) → (g : hom A y z)
→ is-contr (Σ (h : hom A x z) , (hom2 A x y z f g h))
Pre-∞-categories have a composition functor and witnesses to the composition
relation. Composition is written in diagrammatic order to match the order of
arguments in is-pre-∞-category.
#def comp-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y z : A)
( f : hom A x y)
( g : hom A y z)
: hom A x z
:= first (first (is-pre-∞-category-A x y z f g))
#def witness-comp-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y z : A)
( f : hom A x y)
( g : hom A y z)
: hom2 A x y z f g (comp-is-pre-∞-category A is-pre-∞-category-A x y z f g)
:= second (first (is-pre-∞-category-A x y z f g))
Composition in a pre-∞-category is unique in the following sense. If there is a witness that an arrow \(h\) is a composite of \(f\) and \(g\), then the specified composite equals \(h\).
#def uniqueness-comp-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y z : A)
( f : hom A x y)
( g : hom A y z)
( h : hom A x z)
( alpha : hom2 A x y z f g h)
: ( comp-is-pre-∞-category A is-pre-∞-category-A x y z f g) = h
:=
first-path-Σ
( hom A x z)
( hom2 A x y z f g)
( comp-is-pre-∞-category A is-pre-∞-category-A x y z f g
, witness-comp-is-pre-∞-category A is-pre-∞-category-A x y z f g)
( h , alpha)
( homotopy-contraction
( Σ ( k : hom A x z) , (hom2 A x y z f g k))
( is-pre-∞-category-A x y z f g)
( h , alpha))
Characterizing pre-∞-categories¶
Our aim is to prove that a type is a pre-∞-category if and only if the
horn-restriction map, defined below, is an equivalence.
A pair of composable arrows form a horn.
#def horn
( A : U)
( x y z : A)
( f : hom A x y)
( g : hom A y z)
: Λ → A
:=
\ (t , s) →
recOR
( s ≡ 0₂ ↦ f t
, t ≡ 1₂ ↦ g s)
The underlying horn of a simplex:
#def horn-restriction
( A : U)
: ( Δ² → A) → (Λ → A)
:= \ f t → f t
This provides an alternate definition of pre-∞-categories.
#def is-local-horn-inclusion
( A : U)
: U
:= is-equiv (Δ² → A) (Λ → A) (horn-restriction A)
Now we prove this definition is equivalent to the original one. Here, we prove the equivalence used in [RS17, Theorem 5.5]. However, we do this by constructing the equivalence directly, instead of using a composition of equivalences, as it is easier to write down and it computes better (we can use refl for the witnesses of the equivalence).
#def compositions-are-horn-fillings
( A : U)
( x y z : A)
( f : hom A x y)
( g : hom A y z)
: Equiv
( Σ ( h : hom A x z) , (hom2 A x y z f g h))
( ( t : Δ²) → A [Λ t ↦ horn A x y z f g t])
:=
( \ hh t → (second hh) t
, ( ( \ k → (\ t → k (t , t) , \ (t , s) → k (t , s))
, \ hh → refl)
, ( \ k → (\ t → k (t , t) , \ (t , s) → k (t , s))
, \ hh → refl)))
#def equiv-horn-restriction
( A : U)
: Equiv
( Δ² → A)
( Σ ( k : Λ → A)
, ( Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂)))
, ( hom2 A
( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
( \ t → k (t , 0₂)) (\ t → k (1₂ , t))
( h))))
:=
( \ k →
( ( \ t → k t)
, ( \ t → k (t , t) , \ t → k t))
, ( ( \ khh t → (second (second khh)) t , \ k → refl)
, ( \ khh t → (second (second khh)) t , \ k → refl)))
RS17, Theorem 5.5 (the hard direction)
#def equiv-horn-restriction-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
: Equiv (Δ² → A) (Λ → A)
:=
equiv-comp
( Δ² → A)
( Σ ( k : Λ → A)
, ( Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂)))
, ( hom2 A
( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
( \ t → k (t , 0₂)) (\ t → k (1₂ , t))
( h))))
( Λ → A)
( equiv-horn-restriction A)
( total-space-projection
( Λ → A)
( \ k →
Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂)))
, ( hom2 A
( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
( \ t → k (t , 0₂)) (\ t → k (1₂ , t))
( h)))
, ( is-equiv-projection-contractible-fibers
( Λ → A)
( \ k →
Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂)))
, ( hom2 A
( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
( \ t → k (t , 0₂)) (\ t → k (1₂ , t))
( h)))
( \ k →
is-pre-∞-category-A
( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
( \ t → k (t , 0₂)) (\ t → k (1₂ , t)))))
We verify that the mapping in equiv-horn-restriction-is-pre-∞-category A is-pre-∞-category-A
is exactly horn-restriction A.
#def test-equiv-horn-restriction-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
: ( first (equiv-horn-restriction-is-pre-∞-category A is-pre-∞-category-A)) = (horn-restriction A)
:= refl
Pre-∞-categories are types that are local at the horn inclusion
#def is-local-horn-inclusion-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
: is-local-horn-inclusion A
:= second (equiv-horn-restriction-is-pre-∞-category A is-pre-∞-category-A)
Types that are local at the horn inclusion are pre-∞-categories
#def is-pre-∞-category-is-local-horn-inclusion
( A : U)
( is-local-horn-inclusion-A : is-local-horn-inclusion A)
: is-pre-∞-category A
:=
\ x y z f g →
contractible-fibers-is-equiv-projection
( Λ → A)
( \ k →
Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂)))
, ( hom2 A
( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
( \ t → k (t , 0₂))
( \ t → k (1₂ , t))
( h)))
( second
( equiv-comp
( Σ ( k : Λ → A)
, Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂)))
, ( hom2 A
( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
( \ t → k (t , 0₂))
( \ t → k (1₂ , t))
( h)))
( Δ² → A)
( Λ → A)
( inv-equiv
( Δ² → A)
( Σ ( k : Λ → A)
, Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂)))
, ( hom2 A
( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
( \ t → k (t , 0₂))
( \ t → k (1₂ , t))
( h)))
( equiv-horn-restriction A))
( horn-restriction A , is-local-horn-inclusion-A)))
( horn A x y z f g)
We have now proven that both notions of pre-∞-categories are logically equivalent.
RS17, Theorem 5.5
#def is-pre-∞-category-iff-is-local-horn-inclusion
( A : U)
: iff (is-pre-∞-category A) (is-local-horn-inclusion A)
:= (is-local-horn-inclusion-is-pre-∞-category A , is-pre-∞-category-is-local-horn-inclusion A)
Function and extension types into pre-∞-categories¶
Using the new characterization of pre-∞-categories, we can show that the type of functions or extensions into a family of pre-∞-categories is again a pre-∞-category. For instance if \(X\) is a type and \(A : X → U\) is such that \(A x\) is a pre-∞-category for all \(x\) then \((x : X) → A x\) is a pre-∞-category.
RS17, Corollary 5.6(i)
#def is-pre-∞-category-function-type uses (funext)
( X : U)
( A : X → U)
( fiberwise-is-pre-∞-category-A : (x : X) → is-local-horn-inclusion (A x))
: is-local-horn-inclusion ((x : X) → A x)
:=
is-equiv-triple-comp
( Δ² → ((x : X) → A x))
( ( x : X) → Δ² → A x)
( ( x : X) → Λ → A x)
( Λ → ((x : X) → A x))
( \ g x t → g t x) -- first equivalence
( second (flip-ext-fun
( 2 × 2)
( Δ²)
( \ t → BOT)
( X)
( \ t → A)
( \ t → recBOT)))
( \ h x t → h x t) -- second equivalence
( second (equiv-function-equiv-family
( funext)
( X)
( \ x → (Δ² → A x))
( \ x → (Λ → A x))
( \ x → (horn-restriction (A x) , fiberwise-is-pre-∞-category-A x))))
( \ h t x → (h x) t) -- third equivalence
( second (flip-ext-fun-inv
( 2 × 2)
( Λ)
( \ t → BOT)
( X)
( \ t → A)
( \ t → recBOT)))
If \(X\) is a shape and \(A : X → U\) is such that \(A x\) is a pre-∞-category for all \(x\) then \((x : X) → A x\) is a pre-∞-category.
RS17, Corollary 5.6(ii)
#def is-pre-∞-category-extension-type' uses (extext)
( I : CUBE)
( ψ : I → TOPE)
( A : ψ → U)
( fiberwise-is-pre-∞-category-A : (s : ψ) → is-local-horn-inclusion (A s))
: is-local-horn-inclusion ((s : ψ) → A s)
:=
is-equiv-triple-comp
( Δ² → (s : ψ) → A s)
( ( s : ψ) → Δ² → A s)
( ( s : ψ) → Λ → A s)
( Λ → (s : ψ) → A s)
( \ g s t → g t s) -- first equivalence
( second
( fubini
( 2 × 2)
( I)
( Δ²)
( \ t → BOT)
( ψ)
( \ s → BOT)
( \ t s → A s)
( \ u → recBOT)))
( \ h s t → h s t) -- second equivalence
( second (equiv-extension-equiv-family extext I ψ
( \ s → Δ² → A s)
( \ s → Λ → A s)
( \ s → (horn-restriction (A s) , fiberwise-is-pre-∞-category-A s))))
( \ h t s → (h s) t) -- third equivalence
( second
( fubini
( I)
( 2 × 2)
( ψ)
( \ s → BOT)
( Λ)
( \ t → BOT)
( \ s t → A s)
( \ u → recBOT)))
#def is-pre-∞-category-extension-type uses (extext)
( I : CUBE)
( ψ : I → TOPE)
( A : ψ → U)
( fiberwise-is-pre-∞-category-A : (s : ψ) → is-pre-∞-category (A s))
: is-pre-∞-category ((s : ψ) → A s)
:=
is-pre-∞-category-is-local-horn-inclusion
( ( s : ψ) → A s)
( is-pre-∞-category-extension-type'
( I) (ψ) (A)
( \ s → is-local-horn-inclusion-is-pre-∞-category (A s) (fiberwise-is-pre-∞-category-A s)))
In particular, the arrow type of a pre-∞-category is a pre-∞-category. First, we define the arrow type:
#def arr
( A : U)
: U
:= Δ¹ → A
For later use, an equivalent characterization of the arrow type.
#def arr-Σ-hom
( A : U)
: ( arr A) → (Σ (x : A) , (Σ (y : A) , hom A x y))
:= \ f → (f 0₂ , (f 1₂ , f))
#def is-equiv-arr-Σ-hom
( A : U)
: is-equiv (arr A) (Σ (x : A) , (Σ (y : A) , hom A x y)) (arr-Σ-hom A)
:=
( ( \ (x , (y , f)) → f , \ f → refl)
, ( \ (x , (y , f)) → f , \ xyf → refl))
#def equiv-arr-Σ-hom
( A : U)
: Equiv (arr A) (Σ (x : A) , (Σ (y : A) , hom A x y))
:= (arr-Σ-hom A , is-equiv-arr-Σ-hom A)
RS17, Corollary 5.6(ii), special case for locality at the horn inclusion
#def is-local-horn-inclusion-arr uses (extext)
( A : U)
( is-pre-∞-category-A : is-local-horn-inclusion A)
: is-local-horn-inclusion (arr A)
:=
is-pre-∞-category-extension-type'
( 2)
( Δ¹)
( \ _ → A)
( \ _ → is-pre-∞-category-A)
RS17, Corollary 5.6(ii), special case for the Segal condition
#def is-pre-∞-category-arr uses (extext)
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
: is-pre-∞-category (arr A)
:=
is-pre-∞-category-extension-type
( 2)
( Δ¹)
( \ _ → A)
( \ _ → is-pre-∞-category-A)
Identity¶
All types have identity arrows and witnesses to the identity composition law.
RS17, Definition 5.7
#def id-hom
( A : U)
( x : A)
: hom A x x
:= \ t → x
Witness for the right identity law:
RS17, Proposition 5.8a
#def comp-id-witness
( A : U)
( x y : A)
( f : hom A x y)
: hom2 A x y y f (id-hom A y) f
:= \ (t , s) → f t
Witness for the left identity law:
RS17, Proposition 5.8b
#def id-comp-witness
( A : U)
( x y : A)
( f : hom A x y)
: hom2 A x x y (id-hom A x) f f
:= \ (t , s) → f s
In a pre-∞-category, where composition is unique, it follows that composition with an identity arrow recovers the original arrow. Thus, an identity axiom was not needed in the definition of pre-∞-categorys.
If A is a pre-∞-category then the right unit law holds
#def comp-id-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y : A)
( f : hom A x y)
: ( comp-is-pre-∞-category A is-pre-∞-category-A x y y f (id-hom A y)) = f
:=
uniqueness-comp-is-pre-∞-category
( A)
( is-pre-∞-category-A)
( x) (y) (y)
( f)
( id-hom A y)
( f)
( comp-id-witness A x y f)
If A is a pre-∞-category then the left unit law holds
#def id-comp-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y : A)
( f : hom A x y)
: ( comp-is-pre-∞-category A is-pre-∞-category-A x x y (id-hom A x) f) =_{hom A x y} f
:=
uniqueness-comp-is-pre-∞-category
( A)
( is-pre-∞-category-A)
( x) (x) (y)
( id-hom A x)
( f)
( f)
( id-comp-witness A x y f)
Associativity¶
We now prove that composition in a pre-∞-category is associative, by using the fact that the type of arrows in a pre-∞-category is itself a pre-∞-category.
#def unfolding-square
( A : U)
( triangle : Δ² → A)
: Δ¹×Δ¹ → A
:=
\ (t , s) →
recOR
( t ≤ s ↦ triangle (s , t)
, s ≤ t ↦ triangle (t , s))
For use in the proof of associativity:
#def witness-square-comp-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y z : A)
( f : hom A x y)
( g : hom A y z)
: Δ¹×Δ¹ → A
:= unfolding-square A (witness-comp-is-pre-∞-category A is-pre-∞-category-A x y z f g)
The witness-square-comp-is-pre-∞-category as an arrow in the arrow type:
#def arr-in-arr-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y z : A)
( f : hom A x y)
( g : hom A y z)
: hom (arr A) f g
:= \ t s → witness-square-comp-is-pre-∞-category A is-pre-∞-category-A x y z f g (t , s)
#def witness-asociative-is-pre-∞-category uses (extext)
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( w x y z : A)
( f : hom A w x)
( g : hom A x y)
( h : hom A y z)
: hom2 (arr A) f g h
( arr-in-arr-is-pre-∞-category A is-pre-∞-category-A w x y f g)
( arr-in-arr-is-pre-∞-category A is-pre-∞-category-A x y z g h)
( comp-is-pre-∞-category (arr A) (is-pre-∞-category-arr A is-pre-∞-category-A)
f g h
( arr-in-arr-is-pre-∞-category A is-pre-∞-category-A w x y f g)
( arr-in-arr-is-pre-∞-category A is-pre-∞-category-A x y z g h))
:=
witness-comp-is-pre-∞-category
( arr A)
( is-pre-∞-category-arr A is-pre-∞-category-A)
f g h
( arr-in-arr-is-pre-∞-category A is-pre-∞-category-A w x y f g)
( arr-in-arr-is-pre-∞-category A is-pre-∞-category-A x y z g h)
The witness-associative-is-pre-∞-category curries to define a diagram
\(Δ²×Δ¹ → A\). The tetrahedron-associative-is-pre-∞-category is extracted via the
middle-simplex map \(((t , s) , r) ↦ ((t , r) , s)\) from \(Δ³\) to \(Δ²×Δ¹\).
#def tetrahedron-associative-is-pre-∞-category uses (extext)
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( w x y z : A)
( f : hom A w x)
( g : hom A x y)
( h : hom A y z)
: Δ³ → A
:=
\ ((t , s) , r) →
( witness-asociative-is-pre-∞-category A is-pre-∞-category-A w x y z f g h) (t , r) s
The diagonal composite of three arrows extracted from the
tetrahedron-associative-is-pre-∞-category.
#def triple-comp-is-pre-∞-category uses (extext)
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( w x y z : A)
( f : hom A w x)
( g : hom A x y)
( h : hom A y z)
: hom A w z
:=
\ t →
tetrahedron-associative-is-pre-∞-category A is-pre-∞-category-A w x y z f g h
( ( t , t) , t)
#def left-witness-asociative-is-pre-∞-category uses (extext)
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( w x y z : A)
( f : hom A w x)
( g : hom A x y)
( h : hom A y z)
: hom2 A w y z
( comp-is-pre-∞-category A is-pre-∞-category-A w x y f g)
h
( triple-comp-is-pre-∞-category A is-pre-∞-category-A w x y z f g h)
:=
\ (t , s) →
tetrahedron-associative-is-pre-∞-category A is-pre-∞-category-A w x y z f g h
( ( t , t) , s)
The front face:
#def right-witness-asociative-is-pre-∞-category uses (extext)
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( w x y z : A)
( f : hom A w x)
( g : hom A x y)
( h : hom A y z)
: hom2 A w x z
( f)
( comp-is-pre-∞-category A is-pre-∞-category-A x y z g h)
( triple-comp-is-pre-∞-category A is-pre-∞-category-A w x y z f g h)
:=
\ (t , s) →
tetrahedron-associative-is-pre-∞-category A is-pre-∞-category-A w x y z f g h
( ( t , s) , s)
#def left-associative-is-pre-∞-category uses (extext)
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( w x y z : A)
( f : hom A w x)
( g : hom A x y)
( h : hom A y z)
: ( comp-is-pre-∞-category A is-pre-∞-category-A w y z (comp-is-pre-∞-category A is-pre-∞-category-A w x y f g) h)
= ( triple-comp-is-pre-∞-category A is-pre-∞-category-A w x y z f g h)
:=
uniqueness-comp-is-pre-∞-category
A is-pre-∞-category-A w y z (comp-is-pre-∞-category A is-pre-∞-category-A w x y f g) h
( triple-comp-is-pre-∞-category A is-pre-∞-category-A w x y z f g h)
( left-witness-asociative-is-pre-∞-category A is-pre-∞-category-A w x y z f g h)
#def right-associative-is-pre-∞-category uses (extext)
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( w x y z : A)
( f : hom A w x)
( g : hom A x y)
( h : hom A y z)
: ( comp-is-pre-∞-category A is-pre-∞-category-A w x z f (comp-is-pre-∞-category A is-pre-∞-category-A x y z g h))
= ( triple-comp-is-pre-∞-category A is-pre-∞-category-A w x y z f g h)
:=
uniqueness-comp-is-pre-∞-category
( A) (is-pre-∞-category-A) (w) (x) (z) (f) (comp-is-pre-∞-category A is-pre-∞-category-A x y z g h)
( triple-comp-is-pre-∞-category A is-pre-∞-category-A w x y z f g h)
( right-witness-asociative-is-pre-∞-category A is-pre-∞-category-A w x y z f g h)
We conclude that composition in pre-∞-categories is associative.
RS17, Proposition 5.9
#def associative-is-pre-∞-category uses (extext)
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( w x y z : A)
( f : hom A w x)
( g : hom A x y)
( h : hom A y z)
: ( comp-is-pre-∞-category A is-pre-∞-category-A w y z (comp-is-pre-∞-category A is-pre-∞-category-A w x y f g) h)
= ( comp-is-pre-∞-category A is-pre-∞-category-A w x z f (comp-is-pre-∞-category A is-pre-∞-category-A x y z g h))
:=
zig-zag-concat
( hom A w z)
( comp-is-pre-∞-category A is-pre-∞-category-A w y z (comp-is-pre-∞-category A is-pre-∞-category-A w x y f g) h)
( triple-comp-is-pre-∞-category A is-pre-∞-category-A w x y z f g h)
( comp-is-pre-∞-category A is-pre-∞-category-A w x z f (comp-is-pre-∞-category A is-pre-∞-category-A x y z g h))
( left-associative-is-pre-∞-category A is-pre-∞-category-A w x y z f g h)
( right-associative-is-pre-∞-category A is-pre-∞-category-A w x y z f g h)
#def postcomp-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y : A)
( f : hom A x y)
: ( z : A) → (hom A z x) → (hom A z y)
:= \ z g → comp-is-pre-∞-category A is-pre-∞-category-A z x y g f
#def precomp-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y : A)
( f : hom A x y)
: ( z : A) → (hom A y z) → (hom A x z)
:= \ z → comp-is-pre-∞-category A is-pre-∞-category-A x y z f
Homotopies¶
We may define a "homotopy" to be a path between parallel arrows.
In a pre-∞-category, homotopies are equivalent to terms in hom2 types involving an identity arrow.
#def map-hom2-homotopy
( A : U)
( x y : A)
( f g : hom A x y)
: ( f = g) → (hom2 A x x y (id-hom A x) f g)
:=
ind-path
( hom A x y)
( f)
( \ g' p' → (hom2 A x x y (id-hom A x) f g'))
( id-comp-witness A x y f)
( g)
#def map-total-hom2-homotopy
( A : U)
( x y : A)
( f : hom A x y)
: ( Σ ( g : hom A x y) , (f = g))
→ ( Σ ( g : hom A x y) , (hom2 A x x y (id-hom A x) f g))
:= \ (g , p) → (g , map-hom2-homotopy A x y f g p)
#def is-equiv-map-total-hom2-homotopy-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y : A)
( f : hom A x y)
: is-equiv
( Σ ( g : hom A x y) , f = g)
( Σ ( g : hom A x y) , (hom2 A x x y (id-hom A x) f g))
( map-total-hom2-homotopy A x y f)
:=
is-equiv-are-contr
( Σ ( g : hom A x y) , (f = g))
( Σ ( g : hom A x y) , (hom2 A x x y (id-hom A x) f g))
( is-contr-based-paths (hom A x y) f)
( is-pre-∞-category-A x x y (id-hom A x) f)
( map-total-hom2-homotopy A x y f)
RS17, Proposition 5.10
#def equiv-homotopy-hom2-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y : A)
( f h : hom A x y)
: Equiv (f = h) (hom2 A x x y (id-hom A x) f h)
:=
( ( map-hom2-homotopy A x y f h)
, ( total-equiv-family-of-equiv
( hom A x y)
( \ k → (f = k))
( \ k → (hom2 A x x y (id-hom A x) f k))
( map-hom2-homotopy A x y f)
( is-equiv-map-total-hom2-homotopy-is-pre-∞-category A is-pre-∞-category-A x y f)
( h)))
A dual notion of homotopy can be defined similarly.
#def map-hom2-homotopy'
( A : U)
( x y : A)
( f g : hom A x y)
( p : f = g)
: ( hom2 A x y y f (id-hom A y) g)
:=
ind-path
( hom A x y)
( f)
( \ g' p' → (hom2 A x y y f (id-hom A y) g'))
( comp-id-witness A x y f)
( g)
( p)
#def map-total-hom2-homotopy'
( A : U)
( x y : A)
( f : hom A x y)
: ( Σ ( g : hom A x y) , (f = g))
→ ( Σ ( g : hom A x y) , (hom2 A x y y f (id-hom A y) g))
:= \ (g , p) → (g , map-hom2-homotopy' A x y f g p)
#def is-equiv-map-total-hom2-homotopy'-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y : A)
( f : hom A x y)
: is-equiv
( Σ ( g : hom A x y) , f = g)
( Σ ( g : hom A x y) , (hom2 A x y y f (id-hom A y) g))
( map-total-hom2-homotopy' A x y f)
:=
is-equiv-are-contr
( Σ ( g : hom A x y) , (f = g))
( Σ ( g : hom A x y) , (hom2 A x y y f (id-hom A y) g))
( is-contr-based-paths (hom A x y) f)
( is-pre-∞-category-A x y y f (id-hom A y))
( map-total-hom2-homotopy' A x y f)
RS17, Proposition 5.10
#def equiv-homotopy-hom2'-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y : A)
( f h : hom A x y)
: Equiv (f = h) (hom2 A x y y f (id-hom A y) h)
:=
( ( map-hom2-homotopy' A x y f h)
, ( total-equiv-family-of-equiv
( hom A x y)
( \ k → (f = k))
( \ k → (hom2 A x y y f (id-hom A y) k))
( map-hom2-homotopy' A x y f)
( is-equiv-map-total-hom2-homotopy'-is-pre-∞-category A is-pre-∞-category-A x y f)
( h)))
More generally, a homotopy between a composite and another map is equivalent to the data provided by a commutative triangle with that boundary.
#def map-hom2-eq-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y z : A)
( f : hom A x y)
( g : hom A y z)
( h : hom A x z)
( p : (comp-is-pre-∞-category A is-pre-∞-category-A x y z f g) = h)
: ( hom2 A x y z f g h)
:=
ind-path
( hom A x z)
( comp-is-pre-∞-category A is-pre-∞-category-A x y z f g)
( \ h' p' → hom2 A x y z f g h')
( witness-comp-is-pre-∞-category A is-pre-∞-category-A x y z f g)
( h)
( p)
#def map-total-hom2-eq-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y z : A)
( f : hom A x y)
( g : hom A y z)
: ( Σ ( h : hom A x z) , (comp-is-pre-∞-category A is-pre-∞-category-A x y z f g) = h)
→ ( Σ ( h : hom A x z) , (hom2 A x y z f g h))
:= \ (h , p) → (h , map-hom2-eq-is-pre-∞-category A is-pre-∞-category-A x y z f g h p)
#def is-equiv-map-total-hom2-eq-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y z : A)
( f : hom A x y)
( g : hom A y z)
: is-equiv
( Σ ( h : hom A x z) , (comp-is-pre-∞-category A is-pre-∞-category-A x y z f g) = h)
( Σ ( h : hom A x z) , (hom2 A x y z f g h))
( map-total-hom2-eq-is-pre-∞-category A is-pre-∞-category-A x y z f g)
:=
is-equiv-are-contr
( Σ ( h : hom A x z) , (comp-is-pre-∞-category A is-pre-∞-category-A x y z f g) = h)
( Σ ( h : hom A x z) , (hom2 A x y z f g h))
( is-contr-based-paths (hom A x z) (comp-is-pre-∞-category A is-pre-∞-category-A x y z f g))
( is-pre-∞-category-A x y z f g)
( map-total-hom2-eq-is-pre-∞-category A is-pre-∞-category-A x y z f g)
RS17, Proposition 5.12
#def equiv-hom2-eq-comp-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y z : A)
( f : hom A x y)
( g : hom A y z)
( k : hom A x z)
: Equiv ((comp-is-pre-∞-category A is-pre-∞-category-A x y z f g) = k) (hom2 A x y z f g k)
:=
( ( map-hom2-eq-is-pre-∞-category A is-pre-∞-category-A x y z f g k)
, ( total-equiv-family-of-equiv
( hom A x z)
( \ m → (comp-is-pre-∞-category A is-pre-∞-category-A x y z f g) = m)
( hom2 A x y z f g)
( map-hom2-eq-is-pre-∞-category A is-pre-∞-category-A x y z f g)
( is-equiv-map-total-hom2-eq-is-pre-∞-category A is-pre-∞-category-A x y z f g)
( k)))
Homotopies form a congruence, meaning that homotopies are respected by composition:
RS17, Proposition 5.13
#def congruence-homotopy-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y z : A)
( f g : hom A x y)
( h k : hom A y z)
( p : f = g)
( q : h = k)
: ( comp-is-pre-∞-category A is-pre-∞-category-A x y z f h)
= ( comp-is-pre-∞-category A is-pre-∞-category-A x y z g k)
:=
ind-path
( hom A y z)
( h)
( \ k' q' →
( comp-is-pre-∞-category A is-pre-∞-category-A x y z f h)
= ( comp-is-pre-∞-category A is-pre-∞-category-A x y z g k'))
( ind-path
( hom A x y)
( f)
( \ g' p' →
( comp-is-pre-∞-category A is-pre-∞-category-A x y z f h)
= ( comp-is-pre-∞-category A is-pre-∞-category-A x y z g' h))
( refl)
( g)
( p))
( k)
( q)
As a special case of the above:
#def postwhisker-homotopy-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y z : A)
( f g : hom A x y)
( h : hom A y z)
( p : f = g)
: ( comp-is-pre-∞-category A is-pre-∞-category-A x y z f h) = (comp-is-pre-∞-category A is-pre-∞-category-A x y z g h)
:= congruence-homotopy-is-pre-∞-category A is-pre-∞-category-A x y z f g h h p refl
As a special case of the above:
#def prewhisker-homotopy-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( w x y : A)
( k : hom A w x)
( f g : hom A x y)
( p : f = g)
: ( comp-is-pre-∞-category A is-pre-∞-category-A w x y k f)
= ( comp-is-pre-∞-category A is-pre-∞-category-A w x y k g)
:= congruence-homotopy-is-pre-∞-category A is-pre-∞-category-A w x y k k f g refl p
RS17, Proposition 5.14(a)
#def compute-postwhisker-homotopy-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( x y z : A)
( f g : hom A x y)
( h : hom A y z)
( p : f = g)
: ( postwhisker-homotopy-is-pre-∞-category A is-pre-∞-category-A x y z f g h p)
= ( ap (hom A x y) (hom A x z) f g (\ k → comp-is-pre-∞-category A is-pre-∞-category-A x y z k h) p)
:=
ind-path
( hom A x y)
( f)
( \ g' p' →
( postwhisker-homotopy-is-pre-∞-category A is-pre-∞-category-A x y z f g' h p')
= ( ap
( hom A x y) (hom A x z)
( f) (g') (\ k → comp-is-pre-∞-category A is-pre-∞-category-A x y z k h) (p')))
( refl)
( g)
( p)
RS17, Proposition 5.14(b)
#def prewhisker-homotopy-is-ap-is-pre-∞-category
( A : U)
( is-pre-∞-category-A : is-pre-∞-category A)
( w x y : A)
( k : hom A w x)
( f g : hom A x y)
( p : f = g)
: ( prewhisker-homotopy-is-pre-∞-category A is-pre-∞-category-A w x y k f g p)
= ( ap (hom A x y) (hom A w y) f g (comp-is-pre-∞-category A is-pre-∞-category-A w x y k) p)
:=
ind-path
( hom A x y)
( f)
( \ g' p' →
( prewhisker-homotopy-is-pre-∞-category A is-pre-∞-category-A w x y k f g' p')
= ( ap (hom A x y) (hom A w y) f g' (comp-is-pre-∞-category A is-pre-∞-category-A w x y k) p'))
( refl)
( g)
( p)
#section is-pre-∞-category-Unit
#def is-contr-Unit
: is-contr Unit
:= (unit , \ _ → refl)
#def is-contr-Δ²→Unit uses (extext)
: is-contr (Δ² → Unit)
:=
( \ _ → unit
, \ k →
eq-ext-htpy extext
( 2 × 2) Δ² (\ _ → BOT)
( \ _ → Unit) (\ _ → recBOT)
( \ _ → unit) k
( \ _ → refl))
#def is-pre-∞-category-Unit uses (extext)
: is-pre-∞-category Unit
:=
\ x y z f g →
is-contr-is-retract-of-is-contr
( Σ ( h : hom Unit x z) , (hom2 Unit x y z f g h))
( Δ² → Unit)
( ( \ (_ , k) → k)
, ( \ k → ((\ t → k (t , t)) , k) , \ _ → refl))
( is-contr-Δ²→Unit)
#end is-pre-∞-category-Unit