Segal Types

These formalisations correspond to Section 5 of the RS17 paper.

This is a literate rzk file:

#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 is-equiv-projection-contractible-fibers and 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:

#assume funext : FunExt
#assume extext : ExtExt

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 Segal 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-segal
  ( 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))

Segal types have a composition functor and witnesses to the composition relation. Composition is written in diagrammatic order to match the order of arguments in is-segal.

#def comp-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y z : A)
  ( f : hom A x y)
  ( g : hom A y z)
  : hom A x z
  := first (first (is-segal-A x y z f g))

#def witness-comp-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y z : A)
  ( f : hom A x y)
  ( g : hom A y z)
  : hom2 A x y z f g (comp-is-segal A is-segal-A x y z f g)
  := second (first (is-segal-A x y z f g))

Composition in a Segal type 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-segal
  ( A : U)
  ( is-segal-A : is-segal 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-segal A is-segal-A x y z f g) = h
  :=
    first-path-Σ
      ( hom A x z)
      ( hom2 A x y z f g)
      ( comp-is-segal A is-segal-A x y z f g
      , witness-comp-is-segal A is-segal-A x y z f g)
      ( h , alpha)
      ( homotopy-contraction
        ( Σ ( k : hom A x z) , (hom2 A x y z f g k))
        ( is-segal-A x y z f g)
        ( h , alpha))

Characterizing Segal types

Our aim is to prove that a type is Segal 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 Segal types.

#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-segal
  ( A : U)
  ( is-segal-A : is-segal 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-segal-A
              ( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
              ( \ t → k (t , 0₂)) (\ t → k (1₂ , t)))))

We verify that the mapping in Segal-equiv-horn-restriction A is-segal-A is exactly horn-restriction A.

#def test-equiv-horn-restriction-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  : ( first (equiv-horn-restriction-is-segal A is-segal-A)) = (horn-restriction A)
  := refl

Segal types are types that are local at the horn inclusion

#def is-local-horn-inclusion-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  : is-local-horn-inclusion A
  := second (equiv-horn-restriction-is-segal A is-segal-A)

Types that are local at the horn inclusion are Segal types

#def is-segal-is-local-horn-inclusion
  ( A : U)
  ( is-local-horn-inclusion-A : is-local-horn-inclusion A)
  : is-segal 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 Segal types are logically equivalent.

RS17, Theorem 5.5

#def is-segal-iff-is-local-horn-inclusion
  ( A : U)
  : iff (is-segal A) (is-local-horn-inclusion A)
  := ( is-local-horn-inclusion-is-segal A , is-segal-is-local-horn-inclusion A)

Segal function and extension types

Using the new characterization of Segal types, we can show that the type of functions or extensions into a family of Segal types is again a Segal type. For instance if $X$ is a type and $A:X\to U$ is such that $Ax$ is a Segal type for all $x$ then $(x:X)\to Ax$ is a Segal type.

RS17, Corollary 5.6(i)

#def is-segal-function-type uses (funext)
  ( X : U)
  ( A : X → U)
  ( fiberwise-is-segal-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-segal-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\to U$ is such that $Ax$ is a Segal type for all $x$ then $(x:X)\to Ax$ is a Segal type.

RS17, Corollary 5.6(ii)

#def is-segal-extension-type' uses (extext)
  ( I : CUBE)
  ( ψ : I → TOPE)
  ( A : ψ → U)
  ( fiberwise-is-segal-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-segal-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-segal-extension-type uses (extext)
  ( I : CUBE)
  ( ψ : I → TOPE)
  ( A : ψ → U)
  ( fiberwise-is-segal-A : (s : ψ) → is-segal (A s))
  : is-segal ((s : ψ) → A s)
  :=
    is-segal-is-local-horn-inclusion
      ( ( s : ψ) → A s)
      ( is-segal-extension-type'
        ( I) (ψ) (A)
        ( \ s → is-local-horn-inclusion-is-segal (A s) (fiberwise-is-segal-A s)))

In particular, the arrow type of a Segal type is Segal. 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-segal-A : is-local-horn-inclusion A)
  : is-local-horn-inclusion (arr A)
  :=
    is-segal-extension-type'
      ( 2)
      ( Δ¹)
      ( \ _ → A)
      ( \ _ → is-segal-A)

RS17, Corollary 5.6(ii), special case for the Segal condition

#def is-segal-arr uses (extext)
  ( A : U)
  ( is-segal-A : is-segal A)
  : is-segal (arr A)
  :=
    is-segal-extension-type
      ( 2)
      ( Δ¹)
      ( \ _ → A)
      ( \ _ → is-segal-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 Segal type, 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 Segal types.

If A is Segal then the right unit law holds

#def comp-id-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y : A)
  ( f : hom A x y)
  : ( comp-is-segal A is-segal-A x y y f (id-hom A y)) = f
  :=
    uniqueness-comp-is-segal
      ( A)
      ( is-segal-A)
      ( x) (y) (y)
      ( f)
      ( id-hom A y)
      ( f)
      ( comp-id-witness A x y f)

If A is Segal then the left unit law holds

#def id-comp-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y : A)
  ( f : hom A x y)
  : ( comp-is-segal A is-segal-A x x y (id-hom A x) f) =_{hom A x y} f
  :=
    uniqueness-comp-is-segal
      ( A)
      ( is-segal-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 Segal type is associative, by using the fact that the type of arrows in a Segal type is itself a Segal type.

#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-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y z : A)
  ( f : hom A x y)
  ( g : hom A y z)
  : Δ¹×Δ¹ → A
  := unfolding-square A (witness-comp-is-segal A is-segal-A x y z f g)

The witness-square-comp-is-segal as an arrow in the arrow type:

#def arr-in-arr-is-segal
  ( A : U)
  ( is-segal-A : is-segal 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-segal A is-segal-A x y z f g (t , s)

#def witness-asociative-is-segal uses (extext)
  ( A : U)
  ( is-segal-A : is-segal 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-segal A is-segal-A w x y f g)
      ( arr-in-arr-is-segal A is-segal-A x y z g h)
      ( comp-is-segal (arr A) (is-segal-arr A is-segal-A)
      f g h
      ( arr-in-arr-is-segal A is-segal-A w x y f g)
      ( arr-in-arr-is-segal A is-segal-A x y z g h))
  :=
    witness-comp-is-segal
      ( arr A)
      ( is-segal-arr A is-segal-A)
      f g h
      ( arr-in-arr-is-segal A is-segal-A w x y f g)
      ( arr-in-arr-is-segal A is-segal-A x y z g h)

The witness-associative-is-segal curries to define a diagram $\Delta ²\times \Delta ¹\to A$. The tetrahedron-associative-is-segal is extracted via the middle-simplex map $((t,s),r)\mapsto ((t,r),s)$ from $\Delta ³$ to $\Delta ²\times \Delta ¹$.

#def tetrahedron-associative-is-segal uses (extext)
  ( A : U)
  ( is-segal-A : is-segal 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-segal A is-segal-A w x y z f g h) (t , r) s

The diagonal composite of three arrows extracted from the tetrahedron-associative-is-segal.

#def triple-comp-is-segal uses (extext)
  ( A : U)
  ( is-segal-A : is-segal 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-segal A is-segal-A w x y z f g h
      ( ( t , t) , t)

#def left-witness-asociative-is-segal uses (extext)
  ( A : U)
  ( is-segal-A : is-segal 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-segal A is-segal-A w x y f g)
    h
    ( triple-comp-is-segal A is-segal-A w x y z f g h)
  :=
    \ ( t , s) →
    tetrahedron-associative-is-segal A is-segal-A w x y z f g h
      ( ( t , t) , s)

The front face:

#def right-witness-asociative-is-segal uses (extext)
  ( A : U)
  ( is-segal-A : is-segal 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-segal A is-segal-A x y z g h)
    ( triple-comp-is-segal A is-segal-A w x y z f g h)
  :=
    \ ( t , s) →
    tetrahedron-associative-is-segal A is-segal-A w x y z f g h
      ( ( t , s) , s)

#def left-associative-is-segal uses (extext)
  ( A : U)
  ( is-segal-A : is-segal A)
  ( w x y z : A)
  ( f : hom A w x)
  ( g : hom A x y)
  ( h : hom A y z)
  : ( comp-is-segal A is-segal-A w y z (comp-is-segal A is-segal-A w x y f g) h)
  = ( triple-comp-is-segal A is-segal-A w x y z f g h)
  :=
    uniqueness-comp-is-segal
      A is-segal-A w y z (comp-is-segal A is-segal-A w x y f g) h
      ( triple-comp-is-segal A is-segal-A w x y z f g h)
      ( left-witness-asociative-is-segal A is-segal-A w x y z f g h)

#def right-associative-is-segal uses (extext)
  ( A : U)
  ( is-segal-A : is-segal A)
  ( w x y z : A)
  ( f : hom A w x)
  ( g : hom A x y)
  ( h : hom A y z)
  : ( comp-is-segal A is-segal-A w x z f (comp-is-segal A is-segal-A x y z g h))
  = ( triple-comp-is-segal A is-segal-A w x y z f g h)
  :=
    uniqueness-comp-is-segal
      ( A) (is-segal-A) (w) (x) (z) (f) (comp-is-segal A is-segal-A x y z g h)
      ( triple-comp-is-segal A is-segal-A w x y z f g h)
      ( right-witness-asociative-is-segal A is-segal-A w x y z f g h)

We conclude that Segal composition is associative.

RS17, Proposition 5.9

#def associative-is-segal uses (extext)
  ( A : U)
  ( is-segal-A : is-segal A)
  ( w x y z : A)
  ( f : hom A w x)
  ( g : hom A x y)
  ( h : hom A y z)
  : ( comp-is-segal A is-segal-A w y z (comp-is-segal A is-segal-A w x y f g) h)
  = ( comp-is-segal A is-segal-A w x z f (comp-is-segal A is-segal-A x y z g h))
  :=
    zig-zag-concat
    ( hom A w z)
    ( comp-is-segal A is-segal-A w y z (comp-is-segal A is-segal-A w x y f g) h)
    ( triple-comp-is-segal A is-segal-A w x y z f g h)
    ( comp-is-segal A is-segal-A w x z f (comp-is-segal A is-segal-A x y z g h))
    ( left-associative-is-segal A is-segal-A w x y z f g h)
    ( right-associative-is-segal A is-segal-A w x y z f g h)


#def postcomp-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y : A)
  ( f : hom A x y)
  : ( z : A) → (hom A z x) → (hom A z y)
  := \ z g → comp-is-segal A is-segal-A z x y g f

#def precomp-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y : A)
  ( f : hom A x y)
  : ( z : A) → (hom A y z) → (hom A x z)
  := \ z → comp-is-segal A is-segal-A x y z f

Homotopies

We may define a "homotopy" to be a path between parallel arrows. In a Segal type, 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-segal
  ( A : U)
  ( is-segal-A : is-segal 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-segal-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-segal
  ( A : U)
  ( is-segal-A : is-segal 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-segal A is-segal-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-segal
  ( A : U)
  ( is-segal-A : is-segal 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-segal-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-segal
  ( A : U)
  ( is-segal-A : is-segal 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-segal A is-segal-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-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y z : A)
  ( f : hom A x y)
  ( g : hom A y z)
  ( h : hom A x z)
  ( p : (comp-is-segal A is-segal-A x y z f g) = h)
  : ( hom2 A x y z f g h)
  :=
    ind-path
      ( hom A x z)
      ( comp-is-segal A is-segal-A x y z f g)
      ( \ h' p' → hom2 A x y z f g h')
      ( witness-comp-is-segal A is-segal-A x y z f g)
      ( h)
      ( p)

#def map-total-hom2-eq-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y z : A)
  ( f : hom A x y)
  ( g : hom A y z)
  : ( Σ ( h : hom A x z) , (comp-is-segal A is-segal-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-segal A is-segal-A x y z f g h p)

#def is-equiv-map-total-hom2-eq-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y z : A)
  ( f : hom A x y)
  ( g : hom A y z)
  : is-equiv
      ( Σ ( h : hom A x z) , (comp-is-segal A is-segal-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-segal A is-segal-A x y z f g)
  :=
    is-equiv-are-contr
      ( Σ ( h : hom A x z) , (comp-is-segal A is-segal-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-segal A is-segal-A x y z f g))
      ( is-segal-A x y z f g)
      ( map-total-hom2-eq-is-segal A is-segal-A x y z f g)

RS17, Proposition 5.12

#def equiv-hom2-eq-comp-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y z : A)
  ( f : hom A x y)
  ( g : hom A y z)
  ( k : hom A x z)
  : Equiv ((comp-is-segal A is-segal-A x y z f g) = k) (hom2 A x y z f g k)
  :=
    ( ( map-hom2-eq-is-segal A is-segal-A x y z f g k)
    , ( total-equiv-family-of-equiv
        ( hom A x z)
        ( \ m → ( comp-is-segal A is-segal-A x y z f g) = m)
        ( hom2 A x y z f g)
        ( map-hom2-eq-is-segal A is-segal-A x y z f g)
        ( is-equiv-map-total-hom2-eq-is-segal A is-segal-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-segal
  ( A : U)
  ( is-segal-A : is-segal 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-segal A is-segal-A x y z f h)
  = ( comp-is-segal A is-segal-A x y z g k)
  :=
    ind-path
      ( hom A y z)
      ( h)
      ( \ k' q' →
        ( comp-is-segal A is-segal-A x y z f h)
      = ( comp-is-segal A is-segal-A x y z g k'))
      ( ind-path
        ( hom A x y)
        ( f)
        ( \ g' p' →
          ( comp-is-segal A is-segal-A x y z f h)
        = ( comp-is-segal A is-segal-A x y z g' h))
        ( refl)
        ( g)
        ( p))
      ( k)
      ( q)

As a special case of the above:

#def postwhisker-homotopy-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y z : A)
  ( f g : hom A x y)
  ( h : hom A y z)
  ( p : f = g)
  : ( comp-is-segal A is-segal-A x y z f h) = (comp-is-segal A is-segal-A x y z g h)
  := congruence-homotopy-is-segal A is-segal-A x y z f g h h p refl

As a special case of the above:

#def prewhisker-homotopy-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( w x y : A)
  ( k : hom A w x)
  ( f g : hom A x y)
  ( p : f = g)
  : ( comp-is-segal A is-segal-A w x y k f)
  = ( comp-is-segal A is-segal-A w x y k g)
  := congruence-homotopy-is-segal A is-segal-A w x y k k f g refl p

RS17, Proposition 5.14(a)

#def compute-postwhisker-homotopy-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( x y z : A)
  ( f g : hom A x y)
  ( h : hom A y z)
  ( p : f = g)
  : ( postwhisker-homotopy-is-segal A is-segal-A x y z f g h p)
  = ( ap (hom A x y) (hom A x z) f g (\ k → comp-is-segal A is-segal-A x y z k h) p)
  :=
    ind-path
      ( hom A x y)
      ( f)
      ( \ g' p' →
        ( postwhisker-homotopy-is-segal A is-segal-A x y z f g' h p')
      = ( ap
          ( hom A x y) (hom A x z)
          ( f) (g') (\ k → comp-is-segal A is-segal-A x y z k h) (p')))
      ( refl)
      ( g)
      ( p)

RS17, Proposition 5.14(b)

#def prewhisker-homotopy-is-ap-is-segal
  ( A : U)
  ( is-segal-A : is-segal A)
  ( w x y : A)
  ( k : hom A w x)
  ( f g : hom A x y)
  ( p : f = g)
  : ( prewhisker-homotopy-is-segal A is-segal-A w x y k f g p)
  = ( ap (hom A x y) (hom A w y) f g (comp-is-segal A is-segal-A w x y k) p)
  :=
    ind-path
      ( hom A x y)
      ( f)
      ( \ g' p' →
        ( prewhisker-homotopy-is-segal A is-segal-A w x y k f g' p')
      = ( ap (hom A x y) (hom A w y) f g' (comp-is-segal A is-segal-A w x y k) p'))
      ( refl)
      ( g)
      ( p)

#section is-segal-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-segal-Unit uses (extext)
  : is-segal 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-segal-Unit