Thoughts About a Directed Interval

I started wondering what happens if you try to define a directed interval type that only has one closed, global, describable point --- the final point --- and bind your own hands and say that the only way you can talk about the "initial point" is indirectly, via global sections.

Functions as Spaces over the Interval

Here's a picture of what I'm thinking about:

Consider some function $f : A \to B$, for example $A = 3$ and $B = 4$ and $f$ is the map pictured. My goal is that we should be able to equivalently think of this as a space $X$ that lies over a directed interval $\I$, via a projection map $p$. Axiomatically, the directed interval has one point $i_1$. I'm picturing agda code like

postulate
    𝕀 : Set
    i₁ : 𝕀

and intuitively the interval has a single directed feature that we call a "transition" somewhere away from $i_1$. I'm drawing it in the diagram as a tick mark with directed arrows. The type $\I$ has no other closed points. We think of time as having an end, but no beginning.

Now the type $X$ (over $\I$) is supposed to capture structure of $f$ as a directed type. Over the pre-transition part of $\I$, it looks like $A$, and over the post-transition part of $\I$, it looks like $B$.

Functions from Fibered Spaces

So here's a putative recipe for recovering the types $A, B$ and the map $f : A \to B$, given a type $X$ a map $X \to \I$ We say $A$ is the set of global sections of the projection $p$.

The intuition is that each global section of $p$ has to be a path through $X$ with a "transition" inside $X$ lying over the single transition in $\I$. So it uniquely picks out a blob of $X$ to the left of a transition.

record func : Set₁ where
 constructor
  cfunc
 field
  A B : Set
  f : A → B

funcOfFibered : (X : Set) (p : X → 𝕀) → func
funcOfFibered X p = record { A = Σ[ g : 𝕀 → X ] p ∘ g ≡ id , … }

Then $B$ is simply the set of points of $X$ lying in the fiber of $p$ over $i_1$.

funcOfFibered : (X : Set) (p : X → 𝕀) → func
funcOfFibered X p = record { A = Σ[ g : 𝕀 → X ] p ∘ g ≡ id ,
                               B = Σ[ y : X ] p y ≡ i₁ , … }

Finally, the function $f : A → B$ can be computed as the evaluation at $i_1$. Given a $g$ such that $pg = \rid$, we can compute $g(i_1)$, and observe that this is in the fiber of $p$ over $i_1$, because $p(g(i_1)) = (p \o g) (i_1) = \rid(i_1) = i_1$.

Fibered Spaces from Functions

We could also go in the opposite direction. Given a function $f : A \to B$, it seems plausible to piece together the space $X$ as a pushout.

For each point of $A$, we add in a copy of $\I$, so $A \x \I$ is one arm of the pushout. We also want to make sure that $B$ is included in $X$, so $B$ is the other arm. We then want to glue the endpoint of each copy of $\I$ in $A \x \I$ to the point of $B$ that $f$ carries it to. This means that we want to take the pushout of the morphism $\langle id, i_1 \rangle : A \to A \x \I$ that takes each point of $A$ to the endpoint of its interval-copy, and the morphism $f : A \to B$ that takes each point of $A$ to its image under $B$.

Subsequently we can arrive at the projection $p$ by using the pushout UMP. The composite of the constant-$i_1$ map $i_1 : B\to \I$ with $f : A \to B$ gives us the constantly-$i_1$ map $i_1 \o f : A \to \I$, and the map $\pi_2 \langle id, i_1 \rangle$ is also constantly-$i_1$. So we get a unique map $p : X \to \I$ making the diagram commute.

What Can Be Proven?

Given postulated $\I : Set$ and $i_1 : \I$, I can definitely at this point write down constructions

funcOfFibered : (Σ[ X : Set ] X → 𝕀) → (Σ[ A : Set ] Σ[ B : Set ] A → B)
fiberedOfFunc : (Σ[ A : Set ] Σ[ B : Set ] A → B) → (Σ[ X : Set ] X → 𝕀)

but I tried for a little bit and I failed to prove that either composite of them is the identity. The next best move I assume would be to take one and postulate it is an equivalence. But is one or the other more useful to take as a primitive equivalence? Not sure what the consequences are.

I would also hope that a map $X \to \I \x \I$ would correspond to a commutative square, but tentative thinking in that direction suggests that might not easily follow from any of the proposed postulates above either.