Inverted representation of dependent types

Category theory represents dependent types through pullbacks. I haven't understood this one, but exploring into it I noticed something else. There would seem to be an inverted way to represent dependent types.

You may have heard of dependent sum and wonder why they're called that when they are pairs? It can be explained with the following sequence of isomorphisms.

a     ≃ a
a+a   ≃ a*2
a+a+a ≃ a*3
...

Lets start with an usual dependent type:

Σx:3. F x

You could think that the another type is an indexer for a disjunctive clause:

(Σx:3. F x) ≃ (F 0 ∨ F 1 ∨ F 2)

'x' is an index of the disjunctive clause and you obtain that from the structure. That way it seems like a pair, although it is this kind of a disjunction.

Finding a point

There would seem to be a problem that arises when you try to map a dependent type to category theory.

Types describe points and all valid proofs become morphisms between these points. The points become described through the structure their morphisms have.

However it's not clear how the point Σ(F) should behave exactly. There seem to be a different way to describe it though. A term of that type can be treated as an index to some structure: (x, F x).

So lets say we'd have a way to use types as indexes to structures. We can describe a map from [x](F x) to x. It's a projection function that just extracts the indexer, lets call it f.

Now if this function f commutes with some term, it forms a following equivalence:

x = f y

You can drop 'y' outside from the equation with the terminal morphism, ! : F x → 1.

x.! = f.id

You can construct a structure that has such a commutativity rule. Those are called pullbacks.

Conclusions

I guess that to model a dependent product you need a function that selects pieces from some larger structure with a given index. That behavior also seem to resemble lenses and prisms.

The inverse function is a trivial map for dependent sums. To get into sum/product types that's probably where the slice categories and pullback functors come into play.

If you think of a turnstile representation like this:

x:3 ⊢ y:F x

You could think of it as a dependent sum or dependent product depending on whether you interpret that 'x' is present or not.

Maybe I'll get to point-free representation of dependent types from here. The pullback-model seems interesting although it doesn't tell anything about dependent sum introduction rules at first sight.

Similar posts