# Pre-∞-categories (Segal types) These formalisations correspond to Section 5 of the RS17 paper. !!! info "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: ```rzk #lang rzk-1 ``` ## 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 on `#!rzk is-equiv-projection-contractible-fibers` and `#!rzk total-space-projection` in 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: ```rzk #assume funext : FunExt #assume extext : ExtExt ``` ## Hom types Extension types are used to define the type of arrows between fixed terms: x y ```rzk title="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: x y z f g h ```rzk title="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` ``` ```rzk #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. ```rzk title="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 `#!rzk is-pre-∞-category`. ```rzk #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$. x y z f g h α = x y z f g comp-is-pre-∞-category witness-comp-is-pre-∞-category ```rzk #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 `#!rzk horn-restriction` map, defined below, is an equivalence. x y z f g A pair of composable arrows form a horn. ```rzk #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: ```rzk #def horn-restriction ( A : U) : ( Δ² → A) → (Λ → A) := \ f t → f t ``` This provides an alternate definition of pre-∞-categories. ```rzk #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). ```rzk #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))) ``` ```rzk title="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 `#!rzk equiv-horn-restriction-is-pre-∞-category A is-pre-∞-category-A` is exactly `#!rzk horn-restriction A`. ```rzk #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 ``` ```rzk title="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) ``` ```rzk title="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. ```rzk title="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. ```rzk title="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. ```rzk title="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: ```rzk #def arr ( A : U) : U := Δ¹ → A ``` For later use, an equivalent characterization of the arrow type. ```rzk #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) ``` ```rzk title="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) ``` ```rzk title="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. x x x ```rzk title="RS17, Definition 5.7" #def id-hom ( A : U) ( x : A) : hom A x x := \ t → x ``` Witness for the right identity law: x y y f y f f ```rzk title="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: x x y x f f f ```rzk title="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. ```rzk title="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) ``` ```rzk title="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. • • • • ```rzk #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: x y z y f g comp-is-pre-∞-category g f ```rzk #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 `#!rzk witness-square-comp-is-pre-∞-category` as an arrow in the arrow type: x y z y f g ```rzk #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) ``` w x x y y z f g h ```rzk #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) ``` w x y z g f h The `#!rzk witness-associative-is-pre-∞-category` curries to define a diagram $Δ²×Δ¹ → A$. The `#!rzk tetrahedron-associative-is-pre-∞-category` is extracted via the middle-simplex map $((t , s) , r) ↦ ((t , r) , s)$ from $Δ³$ to $Δ²×Δ¹$. ```rzk #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 ``` w x y z g f h The diagonal composite of three arrows extracted from the `#!rzk tetrahedron-associative-is-pre-∞-category`. ```rzk #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) ``` w x y z g f h ```rzk #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: w x y z g f h ```rzk #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) ``` ```rzk #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. ```rzk title="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 `#!rzk hom2` types involving an identity arrow. ```rzk #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) ``` ```rzk title="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. ```rzk #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) ``` ```rzk title="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. ```rzk #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) ``` ```rzk title="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: ```rzk title="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: ```rzk #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: ```rzk #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 ``` ```rzk title="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) ``` ```rzk title="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 ```