Towards a directed homotopy type theory
Paige Randall North
=1






decorations.markings








thmTheorem[section]
prop[thm]Proposition
example[thm]Example
definition
lemma[thm]Lemma
prob[thm]Problem
constrInternal[thm]Construction
construction[1]
      [for Problem <ref>]
      
notn[thm]Notation















































Towards a directed homotopy type theory
    Paige Randall North
    December 30, 2023
=======================================




In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories, directed homotopy theory, and its applications to concurrency. 

We specify a new `homomorphism' type former for Martin-Löf type theory which is roughly analogous to the identity type former originally introduced by Martin-Löf. The homomorphism type former is meant to capture the notions of morphism (from the theory of categories) and directed path (from directed homotopy theory) just as the identity type former is known to capture the notions of isomorphism (from the theory of groupoids) and path (from homotopy theory). 

Our main result is an interpretation of these homomorphism types into , the category of small categories. There, the interpretation of each homomorphism type _(a,b) is indeed the set of morphisms between the objects a and b of the category .

We end the paper with an analysis of the interpretation in  with which we argue that our homomorphism types are indeed the directed version of Martin-Löf's identity types. 
 


§ INTRODUCTION


Martin-Löf type theory, together with its identity type, is now often described as a synthetic theory of higher groupoids. This rich structure of the identity type was first discovered by Hofmann and Streicher in their disproof of the uniqueness of identity proofs <cit.>. There, the authors construct an interpretation of Martin-Löf's identity type into the category of groupoids where for any terms a,b in a type 𝒢, the identity type _𝒢(a,b) is interpreted to be the set of morphisms a → b in the groupoid interpreting 𝒢.

The full extent of this structure was later made explicit in Voevodsky's interpretation of Martin-Löf type theory with the identity type (amongst other types) into the category of Kan complexes, the objects of which represent spaces or ∞-groupoids <cit.>. In this interpretation, the identity type _K(a,b) of any two points a,b in a Kan complex K is itself a Kan complex, or space.

Following these concrete interpretations, others (e.g. <cit.>) have compared Martin-Löf's specification of the identity types with the part of Quillen's axiomatization of homotopy theory that is today called the theory of weak factorization systems <cit.>. In <cit.>, the author has shown that in any finitely complete category, models of Martin-Löf's identity type are in correspondence with weak factorization systems with two stability properties.

Such results describe a fascinating perspective on the theory of higher groupoids. However, one might argue that this theory is very well understood already by topologists since it has concrete models which have been studied for the better part of a century.
However, if one thinks of the theory of higher groupoids as being a theory of (reversible) paths, then one might wonder whether there is also a type theory which describes a theory of irreversible, or directed, paths. One might hope that such a type theory would shed light on the less well understood theories of higher categories and directed spaces. Both of these theories have a notion of directed paths at their core, and for both of these theories, there are many competing concrete models. Thus, having a synthetic theory of directed paths might shed light on this situation. 

In this paper, we present the core of such a type theory. Our long-term goal is to use this type theory to prove and verify theorems about higher categories, directed homotopy theory, and concurrency.



 §.§ Previous work


Several other type theories with semantics in category theories have been proposed. In <cit.>, the authors construct a type theory that gives a synthetic theory of 1-categories. In <cit.>, the authors construct a type theory that gives a theory of (∞, 1)-categories. Other works-in-progress <cit.> do hope to give a theory of ∞-categories. 

In this paper, we aim to give a syntax which not only describes ∞-categories but also directed spaces. We have three design criteria: (1) that our notion of directed paths is introduced via a type former and not as a judgement, so that it can be iterated as Martin-Löf's identity type can be, (2) that our theory allows us to transport terms of dependent types along directed paths, and (3) that our theory does not always allow us to transport terms of the type of directed paths along identities, since such a transportation does not hold in categories of directed spaces. 

The syntaxes of <cit.> and <cit.> do not meet our first criterion since their directed paths are introduced as a judgement and not as a type former. This seems to make the theory somewhat unwieldy: in <cit.>, only the theory of 1-categories is introduced and <cit.> includes no semantics. The theory of <cit.> does not meet our second criterion, and the theory of <cit.> does not meet our third criterion.



 §.§ Organization


In Section <ref>, we present the syntax for our type theory, which consists of one new type former  within Martin-Löf type theory. In Section <ref>, we interpret the rules of this new type former  within a comprehension category derived from the category  of small categories. Even though the objects of  are simpler than those of our intended semantics (higher categories and directed spaces), we see this as an important test case since its theory is much better understood than those of of our intended semantics.
In Section <ref>, we briefly describe directed homotopy theory and its connection with concurrency, and we sketch an interpretation of our type former  in a category of directed spaces.



§ THE SYNTAX



In this section, we define a type of homomorphisms within standard Martin-Löf type theory <cit.>. We only work in the bare type theory. That is, we assume that we have all the `general rules' of <cit.>, but none of the type-forming rules given there.

First, we require that for every type T, there are two new types

    Γ⊢ T  Γ⊢ T^ Γ⊢ T  Γ⊢ T^

 together with functions.

    Γ⊢ T  
    Γ⊢ t: T^Γ⊢ (t): TΓ⊢ T  
    Γ⊢ t: T^Γ⊢^ (t): T^



Now we can define our type of homomorphisms.


    formation:        introduction:  
         Γ⊢ T  
    Γ⊢ s : T^
    Γ⊢ t : TΓ⊢_T(s,t)          Γ⊢ T  
    Γ⊢ t : T^Γ⊢ 1_t : _T(^ t, t)


    right  elimination: 
         Γ⊢ T  
    Γ, s: T^⊢Θ(s)  
    Γ, s: T^, t: T , f: _T(^ s, t), θ: Θ(s) ⊢ D(f,θ)  
    Γ, s:  T^, θ : Θ(s) ⊢ d(θ) : D(1_s, θ) 
    Γ, s: T^, t: T , f: _T(^ s, t), θ:Θ(s) ⊢(d,f,θ) : D(f,θ)


    left  elimination: 
         Γ⊢ T  
    Γ, s: T^⊢Θ(s)  
    Γ, s: T^, t: T^ , f: _T( s,  t), θ: Θ(t) ⊢ D(f, θ)  
    Γ, s:  T^, θ: Θ(s) ⊢ d(θ) : D(1_s, θ) 
    Γ, s: T^, t: T^ , f: _T( s, t) , θ: Θ(t) ⊢(d,f,θ) : D(f,θ)


    right  computation: 
         Γ⊢ T  
    Γ, s: T^⊢Θ(s)  
    Γ, s: T^, t: T , f: _T(^ s, t), θ: Θ(s) ⊢ D(f,θ)  
    Γ, s:  T^, θ : Θ(s) ⊢ d(θ) : D(1_s, θ) 
    Γ, s:  T^, θ : Θ(s)  ⊢(d,1_s,θ ) ≡ d(θ) : D(1_s,θ)


    left  computation: 
         Γ⊢ T  
    Γ, s: T^⊢Θ(s)  
    Γ, s: T^, t: T^ , f: _T( s,  t), θ: Θ(t) ⊢ D(f, θ)  
    Γ, s:  T^, θ: Θ(s) ⊢ d(θ) : D(1_s, θ) 
    Γ, s:  T^,  θ: Θ(s)  ⊢(d,1_s,θ) ≡ d(θ) : D(1_s,θ )




 §.§ Transportation and composition


Before we develop semantics for these rules, we prove some illustrative results in the syntax. 

First, we show that we can transport types along homomorphisms, which is analogous to the transportation along identities in homotopy type theory.


For any type Γ, t:T ⊢ S(t), we have a dependent term as follows.

    Γ, t:T^, t':T, f: _T(^ t,t'), s:S( t) ⊢𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍_𝖱(s,f):S(t')

 

By plugging the data


  * Γ, ⊢ T

  * Γ, t: T^⊢ s:S( t)

  * Γ, t:T^, t':T, f: _T(^ t,t'), s:S( t) ⊢ S(t')

  * Γ, t: T^, s:S( t)  ⊢ s:S( t)

into the right  computation rule, we find a term 

    Γ, t:T^, t':T, f: _T(^ t,t'), s:S( t) ⊢(λ s. s, f,s):S(t')

which we abbreviate by 𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍_𝖱(s,f) (where that λ s. s is merely abbreviation for the dependent term Γ, t: T^, s:S( t)  ⊢ s:S( t), and not a term constructor in our language.)


Now using this transportation, we can show that we can compose two homomorphisms.


For any type ⊢ T, we have a dependent term as follows.

    r:T^, s:T^,t:T, f: _T(r, s), g: _T(^ s, t)
    ⊢𝖼𝗈𝗆𝗉_𝖱(f,g):_T(r,t)



Using Proposition <ref>, we obtain a dependent term

    r:T^, s:T^,t:T, f: _T(r, s), g: _T(^ s, t)
    ⊢𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍_𝖱(f,g):_T(r,t)

which we rename 𝖼𝗈𝗆𝗉_𝖱(f,g).


By the right  computation rule, we find that for any f: _T(r, s), the composition 𝖼𝗈𝗆𝗉_𝖱(f,1_s) is strictly equal to f: _T(r, s). Using left  elimination, we could analogously construct a left transportation 𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍_𝖫 and a left composition 𝖼𝗈𝗆𝗉_𝖫 such that for any g: _T(^ s,t), the composition 𝖼𝗈𝗆𝗉_𝖫(1_s,g) is strictly equal to g in the type _T(^ s,t).





§ THE SEMANTICS IN 



In this section, we construct an interpretation in the category of categories.

We work in a set theory with two uncountable inaccessible cardinals κ < λ. Let  denote the category of κ-small categories, and let  denote the 2-category of λ-small categories. We have arranged this so that  contains  and all the objects of . Note that there are no universes in our syntax, so this is as much of a tower of universes in the semantics as we need.



 §.§ Grothendieck (op)fibrations


The notions of Grothendieck fibrations and opfibrations play a central role in this interpretation, so we briefly review it here. See <cit.> for more details.

Consider a functor P: ℰ→ℬ in . We say that a morphism e: E' → E in ℰ is cartesian if for any other morphism e': E”→ E in ℰ, any factorization of P(e') through P(e) (that is, a morphism b: P(E”) → P(E') such that P(e) ∘ b = P(e')) uniquely lifts to a factorization of e' through e (that is, there is a unique morphism ℓ: E”→ E' such that e ∘ℓ = e' and P(ℓ) = b).

    ℰ[d]^-P     E”@–>[r]_∃ ! ℓ@/^7pt/[rr]^e'    E' [r]_-e     E 
    ℬ    P(E”) [r]^b@/_7pt/[rr]_P(e')    P(E') [r]^-P(e)    E


The archetypical cartesian morphisms are pullback squares, in the following sense. First, let  denote the poset 0 ≤ 1. Then ^ is the category of morphisms of a category . Let :^→ be the functor which sends each morphism to its codomain. Now consider any category  in  with all pullbacks. Then a morphism in ^ whose underlying diagram in  is a pullback square is a cartesian morphism with respect to the functor .
 
A functor P: ℰ→ℬ in  is a Grothendieck fibration if for any object E of , any morphism b: B → P(E) in ℬ can be lifted to a cartesian morphism e: E' → E (so that P(e) = b).

The archetypical Grothendieck fibration is a functor of the form :^→ for any category  with all pullbacks. This is because for any object f in ^ (which is a morphism f: X → Y in ) and  morphism g: Z →(f), the pullback square π: g^*f → f is a cartesian morphism in ^ which is a lift of g.

Dually, we can define cocartesian morphisms and Grothendieck opfibrations. For a functor P: ℰ→ℬ in , a cocartesian morphism in ℰ is a cartesian morphism in ℰ^ with respect to the functor P^. Then our archetypical cocartesian morphisms are pushout squares in any ^ with respect to the functor :^→. A Grothendieck opfibration is a functor P: ℰ→ℬ in  such that P^ is a Grothendieck fibration. Our archetypical Grothendieck opfibration is :^→ for any category  with all pushouts.

One reason that Grothendieck fibrations have been of interest is that they are equivalent to pseudofunctors into . However, we will not make full use of that equivalence here, but we will make use of the Grothendieck construction. Consider any category  in , and any functor F: →. We can construct, following Grothendieck, a new category .F as follows. The objects of .F are pairs (X, Y) such that X is an object of  and Y is an object of F(X). Morphisms (X, Y) → (X',Y') in .F are pairs (f,g) such that f: X → X' is a morphism in  and g: F(f)(Y) → Y' is a morphism in F(X'). Then there is a projection functor π_: .F → which takes each pair (X, Y) to X. The functor π_ is a Grothendieck opfibration since given any (X,Y) in .F, we can lift any morphism f: X → X' in  to the cocartesian morphism (f,1_F(Y)):(X,Y) → (X', F(Y)) in .F. 

Dually, given any functor of the form F: ^→, one can construct a Grothendieck fibration π_: .F →. The objects of .F are still pairs (X, Y) such that X is an object of  and Y is an object of F(X), but the morphisms (X, Y) → (X',Y') of .F are pairs (f,g) such that f: X → X' is a morphism in  and g: Y → F(f)(Y') is a morphism in F(X). 



 §.§ The comprehension category


A comprehension category over  (following <cit.>) consists of a category , a functor χ: →^, and a Grothendieck fibration G: → in  making the following diagram commute and such that χ sends to cartesian morphisms in ℰ to cartesian morphisms in ^ (that is, pullback squares).

    [rr]^χ[rd]_G      ^[dl]^


When interpreting a type theory into this framework, we take the objects of  to be our collection of contexts, the morphisms of  to be context morphisms, and each fiber G^-1 (Γ) to be the collection of types dependent on the context Γ. The terminal category * is the interpretation of the empty context.
By applying the functor χ to an object T of G^-1 (Γ), we obtain a morphism χ(T) in  with codomain Γ; the domain of χ(T) is the context extension (or comprehension) of Γ by T. Thus, terms in a type T dependent on a context Γ are interpreted by sections of χ(T). 


To construct a comprehension category over .



Before we construct the comprehension category, we indicate what G^-1 (*) (the types in the empty context) will be. This will be the category of functors * →, which is isomorphic to  itself. The comprehension functor χ will take a functor of the form : * → to a functor which is isomorphic to the unique functor (*) → *.
Thus, terms of  are functors * →(*), which are just objects of the category (*).


compcat
Consider the functor 

    [-,]: ^→

 which takes each object Γ in  to the category [Γ,] of functors Γ→ in  and natural transformations between them. Performing the Grothendieck construction on this functor, we get the Grothendieck fibration 
 
    π_:  .[-, ] →.

The objects of . [-, ] are pairs (Γ, T ) where Γ is a category in  and T: Γ→ is a functor. The morphisms (Γ, T) → (Γ', T') are pairs (F,τ) such that F: Γ→Γ' is a functor and τ: T ⇒ T' ∘ F is a natural transformation. 

    @=>^τ (5,-2)*; (5,-5)*Γ[r]^T [d]_F     
    Γ '  [ur]_T'


Now we define the functor χ : . [-, ] →^ to be the Grothendieck construction. That is, for any object (Γ, T) in . [-, ], we have 
    χ(Γ, T)  :=   π_Γ: Γ.T →Γ.
 
For any morphism (F,τ): (Γ, T) → (Γ', T') we have that χ(F,τ) is the morphism in ^ with the following underlying commutative square in 

    Γ.T [d]^π_Γ[rr]^χ(F,τ)        Γ'.T' [d]^π_Γ'
    Γ[rr]^F       Γ'

where χ(F,τ) is the functor which sends each (X,Y) in Γ.T to (F(X), τ_X(Y)) in Γ'.T'.

By Lemma <ref> below, the functor χ preserves cartesian morphisms.

Now it is straight-forward to check that the following diagram commutes.

    .[-,] [rr]^χ[rd]_π_      ^[dl]^

In particular, on objects, we have χ (Γ, T) = (π_Γ: Γ.T →Γ) = Γ
and π_(Γ, T) = Γ.


 
The functor χ preserves cartesian morphisms.


Consider a cartesian morphism (F, τ): (Γ, T) → (Γ, T') in .[-,].

    @=>^τ (5,-2)*; (5,-5)*Γ[r]^T [d]_F     
    Γ '  [ur]_T'

Applying χ to this functor, we obtain the following morphism in ^, which is a commutative square in . 

    Γ.T [d]^π_Γ[rr]^χ(F,τ)        Γ'.T' [d]^π_Γ'
    Γ[rr]^F       Γ'

We want to show that this is cartesian with respect to : ^→.

So consider a morphism ⟨α, β⟩: Z →π_Γ' in ^ and a morphism γ: Z_1 →Γ in  such that F γ = β as illustrated below.

    Z_0 @–>[r]^δ[d]^Z  @/^20pt/[rrr]^α   Γ.T [d]^π_Γ[rr]^χ(F,τ)        Γ'.T' [d]^π_Γ'
    
    Z_1 @/_20pt/[rrr]_β[r]^γ   Γ[rr]^F       Γ'
    *

We need to show that there is a unique δ: Z_0 →Γ.T which makes the diagram commute.

Consider the object (Z_0, c_*,Z_0) in .[-,] (where c_*,Z_0 is the functor Z_0 → which sends everything to the terminal category).
Then there is a morphism (β Z, α):
(Z_0, c_*,Z_0) → (Γ', T') where α_z is the functor * → T'Fβ Z(z) which picks out the object α(z) for any object z ∈ Z_0.

    @C=6em@=>^τ (12,-16)*; (12,-20)*@=>^δ (12,-6)*; (12,-10)*@=>^<<<<α (5,-5)*; (5,-21)*
    Z_0 @/^/[dr]^c_*,Z_0[d]_β Z
    Γ[r]|<<<<^>>>>>>>T [d]_F     
    Γ '  @/_/[ur]_T'

Since (F,τ) is cartesian, there is a unique natural transformation δ: c_*,Z_0⇒ Tβ Z such that α= τδ. This gives rise to the functor δ: Z_0 →Γ.T by setting δ(z) := (Γ, δ_z(*)). This makes the diagram (*) above commute. 

If there were another such functor δ' making the diagram (*) commute, by making an analogous argument, we would find a natural transformation δ'. But then δ' = δ, and so δ' = δ. Thus, δ is the unique functor making the diagram (*) commute.

Thus, χ(F, τ) is cartesian for every cartesian (F, τ) so χ is cartesian.



This comprehension category has a unit η: →.[-,] which takes a category Γ to (Γ, *_Γ: Γ→) where *_Γ is the functor which is constant at the terminal category *. Then χ (Γ, *_Γ) is an isomorphism π_Γ : Γ. *_Γ→Γ. Recall that for any (Γ, T) in .[-,], we interpret the terms of T as sections of χ(Γ, T). These are in bijection with functors Γ. *_Γ→χ(Γ, T) over Γ (where the functor  sends a functor to its domain). These are in bijection with morphisms (Γ, *_Γ) → (Γ, T) in the fiber π_^-1Γ which are just morphisms *_Γ→  T in the category [Γ, ]. 

In the sections that follow, we will interpret contexts as categories Γ in , we will interpret types in context Γ as objects of the category [Γ, ] (which are functors Γ→), and we will interpret terms of such an object T in [Γ, ] as morphisms from *_Γ→ T in [Γ, ] (which are natural transformations *_Γ⇒ T). 



 §.§  and 


In this section, we interpret the type formers  and  and the functions  and ^ into our comprehension category. 


To construct functorially, from each functor : Γ→, functors ^: Γ→ and ^: Γ→, natural transformations i: ^⇒ T and i^ : ^⇒^.



Before we give the construction, we describe what it will be in the empty context.

Consider a type  in the empty context, which is just a category. Then ^ will be just the set[In this note, we will often talk about a set X in the category . To be clear, we mean the category whose objects are the elements of X and whose morphisms are only identity morphisms.] of objects of  and ^ will be the usual opposite category of . Then i: ^→ and i^: ^→^ will be the injections which are the identity on objects.


coreop
Recall the two oft-encountered endofunctors (-)^ and (-)^ on . For any category , the category  ^ is the set ().
The objects of ^ are the objects of , and for all objects X, Y of 𝒞^, the homomorphisms X → Y in ^ are the homomorphisms Y → X in . There are moreover natural transformations i: (-)^⇒ id_ and i^: (-)^⇒ (-)^ induced by the identity function on objects. 

Postcomposition with the functors (-)^ and (-)^ gives two functors which take any : Γ→ to ^: Γ→ and ^: Γ→, respectively. 

Whiskering with i (resp. i^) gives a functor which takes any : Γ→ to the natural transformation i: ^⇒ (resp. i^: ^⇒^).







 §.§  formation

In this section, we interpret the  formation rule.

To functorially construct for each functor : Γ→ and natural transformations s: *_Γ⇒^ , t: *_Γ⇒, a functor _(s,t): Γ→.



In the empty context, our problem reduces to finding for each category  and object (x,y) ∈^×, a category _(x,y). Our construction will produce the usual homset _(x,y).


formation
Let (-)^× id_: → denote the functor which takes any ∈ to ^× in . Then let c_: → be the constant functor at , the category of κ-small sets. 

There is a lax natural transformation : (-)^× id_⇒ c_ which at each ∈ is the usual functor _: ^×⇒ (which maps an object (X,Y) ∈^× to the set _(X,Y) of morphisms X → Y in ). This transformation is not natural since for a functor F: →, the square of functors might not commute. It is however a lax natural transformation since there is a natural transformation _F: _→_(F^× F) which at each (X, Y) ∈^× is the function _(X,Y) →_(F^ X , FY), the morphism part of the functor F.

    ^×[d]__^>>>>>>     _F[r]^F^× F   ^×[d]^_
    @=[r]


Now for any functor : Γ→ and natural transformations s: *_Γ⇒^ , t: *_Γ⇒, we have the following diagram of functors and (lax) natural transformations.

    @=5emΓ<10>^ *_Γ (s,t)          [r]_-   [r]^(-)^× id   <-10>_c_      
    *



By pasting together the natural transformation (s,t) and the lax natural transformation  in the diagram above, we obtain a lax natural transformation _(s,t): *_Γ⇒ c_. 
At every object γ∈Γ, this gives a functor _(s,t)γ: * → which is just a set _(s,t)γ(*). For every morphism ϕ: γ→γ' in Γ, this produces a natural transformation  

    @C=5em*[d]__(s,t)γ^   _(s,t)ϕ@=[r]    *[d]^_(s,t)γ'
    @=[r]

which is just a function _(s,t)ϕ_*: _(s,t)γ(*) →_(s,t)γ'(*). In other words, _(s,t) is a functor Γ→.



 §.§  introduction


In this section, we interpret the  introduction rule.



To functorially construct for each functor : Γ→ and natural transformation t: *_Γ⇒^, a natural transformation 1_t: *_Γ⇒_(i^ t,i t).


In the empty context, our problem reduces to finding for each category  and object t ∈^, an object 1_t ∈_T( t, t). Our construction will produce the usual identity morphism t → t.

introduction
For every category  and for every t ∈^ (that is, an object t of ), there is an element 1^_t ∈_(t,t), the identity morphism t → t. Since this is (vacuously) natural in t, it assembles into the natural transformation shown below

    @C=5em^^c_*__(i^× i) 1_∙^

where c_* is the constant functor at the terminal set. 

This is furthermore natural in , so it assembles into the following modification.

    @C=10em@/^20pt/[rr]^(-)^@/_20pt/[rr]_c_      @=@/^-15pt/_c_* (36,5)*; (36,-5)*@=>@/^-15pt/ (36,5)*; (37,-5.7)*@=@/^15pt/^_(i^× i) (45,5)*; (45,-5)*@=>@/^15pt/ (45,5)*; (44,-5.7)*@3^1_∙ (37,0)*; (46,0)*



Now, consider a functor : Γ→ and a natural transformation t: *_Γ⇒^. We obtain a diagram 

    @C=10emΓ[r]^@<10pt>@/^30pt/[rrr]^*_Γ   @/^20pt/[rr]^(-)^@/_20pt/[rr]_c_      @=@/^-15pt/_c_* (76,5)*; (76,-5)*@=>@/^-15pt/ (76,5)*; (77,-5.7)*@=@/^15pt/^_(i^× i) (85,5)*; (85,-5)*@=>@/^15pt/ (85,5)*; (84,-5.7)*@=>^t (50,12)*; (50,6)*@3^1_∙ (77,0)*; (86,0)*

Then pasting together this diagram, we obtain 
a modification c_* ⇛_(i^ t, i t) which unfolds into a natural transformation 1_t: * ⇒(ι^ t,ι t). This natural transformation has at each γ∈Γ the component 1_t γ: * →( t γ, t γ) which picks out the identity morphism t γ→ t γ.




 §.§ Right  elimination and computation


In this section, we interpret the right  elimination rule so that it satisfies the strict equality required by the right  computation rule.


To functorially construct for 
each functor : Γ→, each functor Θ: Γ.^→,
each functor : Γ.^ . . _ (i^× 1).Θ→, and 
each natural transformation 

    d: *_Γ.^.Θ⇒∘ 1_∙.Θ:Γ.^.Θ→,
 a natural transformation 

    e_r(d): *_Γ.^ . . _ (i^× 1).Θ⇒:  Γ.^ . . _ (i^× 1).Θ→,
 such that e_r(d)∘ 1_∙.Θ = d.



Where Γ and Θ are both empty contexts, our problem reduces to finding for 
each category , 
each functor 
: ^.._(i^× 1) →,
and each natural transformation 
d: *_^⇒∘ 1_∙: ^→, a natural transformation 

    e_r(d): *_^.._(i^× 1)⇒:   ^.._(i^× 1) →,
 
such that e_r(d) 1_∙ = d.

The objects of ^.._(i^× 1) are triples (X,Y,f) such that f: X → Y is a morphism in . Its morphisms are of the form g: (X,Y,f) → (X,Y',g ∘ f) where g:Y → Y' is a morphism of .  

Since e_r(d) 1_∙ must be d, we know that e_r(d)_(X,X,1_X) must be d(X) for any object X of ^.
Now for any other object (X,Y,f) of ^.._(i^× 1), there is a morphism f: (X,X,1_X) → (X,Y,f).
Then we get a morphism (f) : (X,X,1_X) →(X,Y,f). We apply this functor to d(X) to obtain e_r(d)_f. That is, we set

    e_r(d)_f := (f) ( dX ).


rightelim
Consider the data given in the Problem.
The objects of the category Γ.^ . . _ (i^× 1).Θ are quintuples (γ, s,t, f, θ) where γ is an object of Γ, f: s → t is a morphism in the category (γ), and θ is an object of Θ(γ, s).
Morphisms in Γ.^ . . _ (i^× 1).Θ are of the form 

    (ϕ, α, β) : (γ, s,t, f, θ) → (γ',  (ϕ)(s) , t',  α∘(ϕ)(f), θ') *

where ϕ: γ→γ' is a morphism in Γ, α : (ϕ)(t) → t' is a morphism in (γ'), and β: Θ(ϕ)(θ) →θ' is a morphism in Θ(γ', (ϕ)(s)).

The objects of the category Γ.^.Θ are triples (γ, t, θ) where γ∈Γ, t ∈^(γ), and θ∈Θ(γ,t). The morphisms are of the form (ϕ,β): (γ, t,θ) → (γ', T(ϕ)(t) ,θ') where ϕ: γ→γ' is a morphism in Γ and β: Θ(ϕ)θ→θ' is a morphism in Θ(γ', T(ϕ)(t)).

The functor 1_∙.Θ: Γ.T^.Θ→Γ.^ . . _ (i^× 1).Θ takes a triple (γ, t, θ) to the quintuple (γ, t,t, 1_t, θ).

Now, to construct the natural transformation

    e_r(d): * ⇒:  Γ.^ . . _ (i^× 1).Θ→,

we need to first specify all of its components e_r(d)_(γ, s,t, f,θ): * →(γ, s,t, f,θ).

So fix an object (γ, s,t, f,θ) of the category Γ.^ . . _ (i^× 1).Θ. To construct a functor 
e_r(d)_(γ, s,t, f,θ): * →(γ, s,t, f,θ) is to find an object of the category (γ, s,t, f,θ).
Consider the morphism (1_γ, f,1_θ): (γ, s,s, 1_s,θ) → (γ, s,t, f,θ) in Γ.^ . . _ (i^× 1).Θ. By applying the functor , we get a functor  

    (1_γ, f,1_θ): ∘ 1_∙ (s).Θ = (γ, s,s, 1_s,θ) → (γ, s,t, f,θ).

Now we apply this functor to the object d(γ,s,θ)(*) of ∘ 1_∙ (γ, s,θ) to get e_r(d)_(γ, s,t, f, θ) as follows:

    e_r(d)_(γ, s,t, f, θ)(*) := (1_γ,f,1_θ) d(γ, s,θ)(*).


We need to check that this choice is natural, which amounts to showing that for any morphism in Γ.^ . . _ (i^× 1).Θ as in line (*) above, we have the equality

    (ϕ, α,β) e_r(d)_(γ, s,t, f,θ) =   e_r(d)_(γ', T(ϕ)( s) ,t', α  T(ϕ)(f),θ') .

But we have 
 
    (ϕ, α,β) e(d)_(γ, s,t, f,θ)   =   (ϕ, α,β)  (1_γ,f,1_θ)d(γ, s,θ) 
       =  (ϕ, α T(ϕ)(f), β)d(γ, s, θ)
       =  (1_γ',α  T(ϕ)(f),1_θ')   (ϕ, 1_T(ϕ)s,β) d(γ,s,θ)
       =  (1_γ',α  T(ϕ)(f),1_θ')d(γ', T(ϕ)(s),θ') 
       =  e_r(d)_(γ', T(ϕ)( s) ,t', α  T(ϕ)(f),θ')
 
where the first equality and last equality come from our definition of e_r(d), the second and third from composition in the category Γ.^ . . _ (i^× 1).Θ, and the forth from the naturality of d.

Now we only need to check that e_r(d)∘ 1_∙.Θ = d. For any (γ, t,θ) of Γ.T^.Θ, we have that 

    e_r(d) 1_∙.Θ(γ,t.θ)   = e_r(d) (γ, t,t,1_t,θ)
       =  (1_γ, 1_t,1_θ)d(γ, t,θ) 
       = d(γ,t,θ)
 
where the first equality is the definition of 1_∙, the second is the definition of e_r(d), and the third is the functoriality of .
Therefore, we have that e_r(d) 1_∙ = d.





 §.§ Left  elimination and computation


In this section, we interpret the left  elimination rule so that it satisfies the strict equality required by the left  computation rule. However, it just takes an application of right  elimination and computation.


To functorially construct for 
each functor : Γ→, each functor Θ: Γ.^→,
each functor : Γ.^ . ^. _ (1 × i).Θ→, and 
each natural transformation 

    d: *_Γ.^.Θ⇒∘ 1_∙.Θ:Γ.^.Θ→,
 a natural transformation 

    e_r(d): *_Γ.^ . ^. _ (1 × i).Θ⇒:  Γ.^ . ^. _ (1 × i).Θ→,
 such that e_r(d)∘ 1_∙.Θ = d.


leftelim
Note that (^)^ = ^,
and 
    Γ.(^)^ . ^. _^ (i × 1).Θ≅Γ.^ . ^. _ (1 × i).Θ

 and (T^)^ = T^. Then by substituting T^ in for T everywhere in the statement of the Problem <ref>, we find that our problem has already been solved.




 §.§ The homotopy theory

In this section, we describe the (directed) homotopy theory that this interpretation inhabits in .


To understand this homotopy theory in , first recall that there are two weak factorization systems on  <cit.>. We begin with the following two factorizations of the fold map

    * + * [r]^-0 + 1   [r]^!    *
    →

    * + * [r]^-0 + 1   𝕀[r]^!    *
    ≅

where  is the category generated by one morphism 0 → 1, 𝕀 is the category generated by one isomorphism 0 ≅ 1. This gives us, by exponentiation, two functorial factorizations of the diagonal →× of any category .

    @C=4em[r]^-^!   ^[r]^-^0 ×^1   ×^→


    @C=4em[r]^-^!   ^𝕀[r]^-^0 ×^1   ×^≅

Then, we can functorially factor any functor F: → in two ways.

    @C=4em[r]^-1 ×^! F   ×_^0^[r]^-^1   ℓ^→, r^→


    @C=4em[r]^-1 ×^! F   ×_^0^𝕀[r]^-^1   ℓ^≅, r^≅

This gives the factorizations of two functorial weak factorization systems (ℒ^→, ℛ^→) and (ℒ^≅, ℛ^≅) on .

We can characterize the right maps of these weak factorization systems in another way. The maps in ℛ^→ are exactly those maps which have the enriched right lifting property against the inclusion of the domain into the generic morphism: 0:* →. The maps in ℛ^≅ are exactly those maps which have the enriched right lifting property against the inclusion of the domain into the generic isomorphism: 0: * →𝕀.

While the usual identity type of Martin-Löf type theory has an interpretation into the weak factorization system (ℒ^≅, ℛ^≅) <cit.>, we claim that we have constructed in the preceding sections an interpretation into the weak factorization system (ℒ^→, ℛ^→). By this, we just mean that (1) given any interpretation of a dependent type : Γ→, its comprehension π_Γ: Γ .T →Γ is in ℛ^→, and (2) the elimination property can be seen as the existence of a lift between a map of ℒ^→ and a map of ℛ^→.

To show that any comprehension π_Γ: Γ.→Γ is in ℛ^→, note first that it is a Grothendieck opfibration.

Any Grothendieck opfibration p: E → B is in ℛ^→.


We need to show that there is a lift ℓ in the following square.

    E [d]_1 × B^!p@=[r]    E [d]^p 
    
    E ×_B^0 B^@–>[ur]^ℓ[r]_-B^1    B



An object of E ×_B^0 B^ is a pair (e, f) where e is an object of E and f:pe → b is a morphism in B. By the definition of Grothendieck opfibration, there is a lift of f, which we will denote (e,f): e →ℓ(e,f) such that p (e,f) = p. We will choose (e,1_e) to always be 1_e.

A morphism (e_0, f_0) → (e_1, f_1) of E ×_B^0 B^ is a pair (ϵ, ϕ) where ϵ: e_0 → e_1 is morphism of E and ϕ: b_0 → b_1 is a morphism of B which makes the following square commute in B.

    pe_0 [d]^f_0[r]^p ϵ   pe_1  [d]^f_1
    
    b_0  [r]^ϕ    b_1

Now, in E we have the following diagram of solid arrows.

    e_0 [d]_(e_0,f_0)[r]^ϵ   e_1  [d]^(e_1,f_1)
    ℓ(e_0,f_0) @–>[r]     ℓ(e_1,f_1)

By the definition of Grothendieck opfibration, we obtain a unique morphism ℓ(e_0,f_0) →ℓ(e_1,f_1), which we will denote ℓ(ϵ, ϕ), which makes the above diagram into a commutative square. 

It is straightforward to check that ℓ is a functor which makes the first diagram of this proof commute.


Now the right elimination property (in the empty context) says that for any category , any functor : ^.._→, and any functor d: ^→^.._. making the following square commute, there is a lift ℓ making both triangles commute.

    ^[r]^-d [d]^1_∙   ^.._.[d]^π
    ^.._@=[r] @–>[ur]^ℓ   ^.._

We want to see that this arises as the solution of a lifting problem between a left map and a right map of our weak factorization system. We just saw that π is a right map, so now we prove that 1_∙ is a left map.


For any category , the functor 

    1_∙ : ^→^.._

is in ℒ^→.


Factor the functor i: ^→. 

    ^[r]^-1 ×^! i   ^×_^0^[r]^-^1

 
 We claim that the middle object, ^×_^0^, is isomorphic to ^.._ and this makes 1_∙ isomorphic to 1 ×^! i, the left factor of the factorization for the weak factorization system (ℒ^→, ℛ^→). Thus, 1_∙ will be in ℒ^→.
 
 The objects of ^.._ are pairs ((x,y),f) where (x,y) is an object of ^× and f is morphism x → y. 
 
 The objects of ^×_^0^ are pairs (x, f) where x is an object of ^ (that is, x is an object of ) and f is morphism with domain x.
 
On objects, define the functor α: ^.._→^×_^0^ by α((x,y),f) := (x,f) and its inverse by α^-1 (x,f) := ((x,  f), f).

 The morphisms ((x,y),f) → ((x,y'),f') of ^.._ are morphisms (1_x,g): (x,y) → (x,y') of ^× such that gf = f'.
 
      The morphisms (x,f) → (x,f') of ^×_^0^ are morphisms  (1_x,g): f → f' of ^ (so that gf = f').
      
      On morphisms, define the functor α and its inverse both by (1_x,g) ↦ (1_x,g).
      
      This gives an isomorphism α: ^.._≅^×_^0^.

Now, we just check that α 1_∙  = 1 × C^! i. For any object x of ^, we have that α 1_∙ (x) and 1 × C^! i(x) are both (x,1_x) (and ^ has no nonidentity morphisms).
 
 
 

§ DIRECTED HOMOTOPY THEORY AND CONCURRENCY
 
 
 In this section, we briefly describe some aspects of directed homotopy theory and its application to concurrency and indicate how our  types can be intepreted in a category of directed spaces.
 
 

 §.§ Background

 In brief, directed homotopy theory is the study of spaces for which certain paths are singled out and given a direction <cit.>. For example, one might want to consider the circle S^1 in the category of topological spaces together with the information that any clockwise path is `allowed', but counter-clockwise paths are `not allowed'. 


Such directed spaces appear in many applications, but perhaps most notably in the study of concurrent processes. A system of concurrent processes can be represented by a space whose points represent states of the system and whose directed paths represent possible executions of the system. For example, we might consider two processes A and B which both need to access the same two memory locations m and n in succession <cit.>. In order to avoid a conflict, we allow each process to `lock' (L) and `unlock' (U) each memory location, and while one memory location is locked by one process, we disallow the other process to lock it. Then the set of allowed states in such a system can be seen to form a directed space S (shaded in gray in Figure <ref>) whose underlying topological space is a subspace of the square [0,1]^2 and whose directed paths are those paths which are monotonically non-decreasing in both A and B.


Now we can ask which states (x,y) are reachable by these two processes starting from the origin (0,0) and which states (x,y) are safe, meaning that the end state (1,1) can be reached from (x,y). In this example, we see that the whole space but the square [U_n^A, U_m^A] × [U_m^B, U_n^B] is reachable and the whole space but the square [L_m^A, L_n^A] × [L_n^B, L_m^B] is safe.



 §.§ Future work: semantics in directed spaces


In future work, we hope to construct an interpretation of -types into a suitable category of directed spaces (see e.g., <cit.>). We roughly sketch that interpretation here.

For any directed space X, we let X^ and X^ have the same underlying space as X, we let X^ have only trivial directed paths, and we reverse the directed paths of X to get the directed paths of X^. Then we let the underlying space of _X(x,y) be the space of directed paths from x to y in X, and we let a directed path of paths 
from p to q in _X(x,y) be a homotopy of paths from p to q which is directed in the homotopy coordinate. The difficult and interesting part of establishing such an interpretation will lie in constructing a universe in this category.

We end by demonstrating that in such an interpretation of -types into a category of directed spaces, together with an interpretation of Martin-Löf's Σ-types, we will be easily able to express the notions of reachable and safe states. Indeed, given a type X and two terms i,f meant to represent the initial and final state, we can define

    𝚁𝚎𝚊𝚌𝚑𝚊𝚋𝚕𝚎(X):= Σ_x ∈ X_X(i,x)


    𝚂𝚊𝚏𝚎(X):= Σ_x ∈ X^_X(x,f).

Then, for our directed space S shown above in Figure <ref>, we would have that 𝚁𝚎𝚊𝚌𝚑𝚊𝚋𝚕𝚎(S) is the directed space of reachable states each with a witness that that state is reachable and 𝚂𝚊𝚏𝚎(X) would be the directed space of safe states each with a witness that that state is safe.



alpha



