Constructing Parametricity Gel Type as Pushout

I slapped together some agda code so I could ask the following question:

Is it a workable strategy to define a Gel type as a pushout of copies of an internalized parametricity interval, rather than postulate its existence, or otherwise bake it into the type theory one is working in?

The agda code is part of an attempt at convincing myself the answer might be "yes", but it's not a complete answer. If anyone knows if the literature already has a "yes" or "no" answer, I'd love to hear!

Axioms

The idea is to try to only axiomatize some things about the interval type itself. I don't have confidence I understand typical model-construction arguments well enough to avoid having made a mistake here or there in thinking these axioms are justified. I have a vague picture of the presheaf category of reflexive graphs in my head, and the axioms seem plausible to me in that light.

So let's take a look at what's going on in Interval/Axioms.agda.

We first postulate the interval type itself. I'm writing it a binary operator that takes two Set arguments. The argument $S$ is its "shape". We can take $S = 2$ as a running example. In this case the interval is the "walking binary relation". It has two points, and some kind of cohesion between them. The argument $D$ is a notion of color in the sense of Bernardy-Moulin's "Type Theory in Color". We have as many colors as there are types.

postulate
  -- D ▻ S is an interval type of "direction" D and "shape S"
  _▻_ : {ℓ1 ℓ2 : Level} (D : Set ℓ1) (S : Set ℓ2) → Set (ℓ-max ℓ1 ℓ2)

Next we abbreviate $T = D \triangleright S$ and postulate that the endpoints of the interval are included in the interval itself.

module _ {ℓ1 ℓ2 : Level} {D : Set ℓ1} {S : Set ℓ2} where
  private
    ℓ = ℓ-max ℓ1 ℓ2
    T = D ▻ S
  postulate
    end : S → T

In the running example of $S = 2$, we can picture this as:

What's more, we suppose this map is an embedding, (i.e. although there is more bridge-like cohesion in the interval, we obtain no new equality paths after traversing the map) and that it isn't an equivalence.

    endIsEmbed : isEmbedding end
    endNonTriv : ¬ (isEquiv end)

Next we suppose that the type $D$ really is discrete for $T$. This is defined as meaning the constant map $D \to (T \to D)$ is an equivalence.

    ▻Discrete : bridgeDiscrete T D

Commuting with Discrete Pushouts

Finally — and this is the postulate I'm least confident in, because I made some other attempts that took me a minute to realize they were inconsistent — we assume that maps out of the interval commute with certain pushouts.

  pushMap : {k1 k2 k3 : Level}
            {A : T → Type k1} {B : T → Type k2} {C : T → Type k3}
            (f : {t : T} → C t → A t) (g : {t : T} → C t → B t)
            (p : Push (λ k (t' : T) → f (k t')) (λ k → g ∘ k)) (t : T)
              → Push (f {t}) (g {t})
  pushMap f g (pinl a) t = pinl (a t)
  pushMap f g (pinr b) t = pinr (b t)
  pushMap f g (ppath c i) t = ppath (c t) i

    ▻Commute : {k1 k2 k3 : Level}
            {A : T → Type k1} {B : T → Type k2} {C : T → Type k3}
            (Adisc : (t : T) → bridgeDiscrete T (A t))
            (Bdisc : (t : T) → bridgeDiscrete T (B t))
            (Cdisc : (t : T) → bridgeDiscrete T (C t))
            (f : {t : T} → C t → A t) (g : {t : T} → C t → B t)
            → isEquiv (pushMap {A = A} f g)

This is expressing something about the fact that the interval should be a "tiny object". I'm vaguely aware that this can't be fully captured internally without using modalities, but I'm curious whether this special case is acceptable.

What this postulate is saying is the following. If we have three types $A, B, C$ indexed over $T$, and some maps \[f : (t : T) \to C\ t \to A\ t\] \[g : (t : T) \to C\ t \to B\ t\] then there definitely at least exists a map (called pushMap above) from the pushout of global elements of these types to the global elements of the pushout of these types. That is, in the below diagram, there is a map \[P \to (t : T) \to Q\ t\] which comes directly from the pushout UMP.

The postulate is that this map is an equivalence. My intuition for why this is "safe" is that the set of edges in a pushout of some graphs is never any bigger than the set of edges in the components being glued together.

There are some subtleties about the internal hom, but I think they might be addressed by the assumptions that all the components of the pushout are (fibrewise) bridge-discrete to start with.

Consequences

Keeping with the running example of $S = 2$, suppose I have a relation defined as a set $R$ with two projections $\pi_0 : R \to A_0$ and $\pi_1 : R \to A_1$. I can think of my sets $A_0$ and $A_1$ equivalently as one unified object \[A : (t : T) (e : E\ t) \to \rset\] where $E$ is the mere proposition on $t$ that says whether $t$ is an endpoint. And I can think of my projects equivalently as a function \[f : (t : T) (e : E\ t) \to R \to A\ t\ e\] From these I can define a gel type \[ \mathsf{Gel} : T \to \rset \] by saying that, for each $t : T$, it is the pushout of $R$ with $(e : E\ t) \x A\ t\ e$.

At each endpoint we glue a copy of the appropriate $A\ t\ e$ along $f$. Because of the assumption that $T \Rightarrow {-}$ commutes with pushouts — as long as $R$ and $A$ are bridge-discrete — we have that the only global elements of $(t: T) \to \mathsf{Gel}\ t$ are elements of the $R$ component, and in fact correspond to mere points in $R$ and not bridges on $R$. So we can define \[\mathsf{gel} : R \to ((t: T) \to \mathsf{Gel}\ t)\] \[\mathsf{ungel} : ((t: T) \to \mathsf{Gel}\ t) \to R \] and can prove that they compose to identities both ways, and appropriately commute with taking endpoints. This is shown in Interval/Gel.agda.

Functoriality

One can also prove that maps between Gel types uniform in $T$ are the same thing as relation homomorphisms, cf. the postulate Ωfunctor in this toot.

This is because the Gel type being a pushout lets us do case analysis to any term of it. By the pushout UMP, we know that \[(t : T) \to \mathsf{Gel}_{R_1}\ t \to \mathsf{Gel}_{R_2}\ t \tag{\dag}\] is the same thing as a pair of maps, one living in \[(t : T) \to R_1 \to \mathsf{Gel}_{R_2}\ t \tag{*}\] and one living in \[(t : T) \to ((e : E\ t) \x A_1\ t\ e) \to \mathsf{Gel}_{R_2}\ t \tag{**}\] satisfying a compatibility condition. But (*) is equivalent to \[ R_1 \to (t : T) \to \mathsf{Gel}_{R_2}\ t \] and therefore also to \[ R_1 \to R_2 \tag{*'}\] and (**) is equivalent to \[(t : T) (e : E\ t) (a : A_1\ t\ e) \to \mathsf{Gel}_{R_2}\ t \] and therefore also to \[(t : T) (e : E\ t) (a : A_1\ t\ e) \to A_2\ t\ e \tag{**'}\] So a uniform map $(\dag)$ is the same thing as a map $(*')$ between relations, with a map $(**')$ saying how it behaves on endpoints, which are suitably compatible, i.e. a relation homomorphism. This is proved in Interval/Functoriality.agda.