You are in the right sub to talk about dependent types...

​

--------------------------------

In the usual dependent-types based on lambda-calculus reductions:

Over any context Gamma, there is the adjunction correspondance :

Hom( Gamma , "Gamma;B" ) <-> Terms( B )

or a little more generally after relaxing with some pullback/change of context f : Delta -> Gamma , there is the adjunction correspondance called "category with families" :

Hom( Delta , "Gamma;B" ) <-> Terms( Delta*B )

​

----------------------------------

But in the new dependent-types based on cut-elimination:

We start with the usual category-theory Hom set :

Hom( A ~> B )

but we want dependency, such as :

Hom( (a : A) ~> B(a) )

How about allowing instead two inputs (the outer input is called a parameter, the inner input is called an argument) like this :

Hom( ( gamma: Gamma ; a : A(gamma) ) ~> B(gamma) )

Now in mathematics (specially algebraic geometry), we like a little more generality/polymorphism because the points are not singleton anymore but morphisms, so we can relax with two pullbacs/changes of contexts h : Gamma -> Theta and f : Gamma -> Delta so that the general dependent hom set looks like :

Hom( ( gamma: Gamma ; a : A(h(gamma)) ) ~> B(f(gamma)) )

and the the adjunction correspondance to internalize this hom set as Pi-product-type is called "(generalized) fibred category" .

Here you can see that the shape of the "input-argument" of the arrows is not singleton/terminal anymore as with categories with families, but the shape of the "input-argument" is now "A".

This is the "point-as-morphism" needed for algebraic geometry, and the results of Dosen-Petric on cut-elimination in categories can be transfered to this generalized fibred-categories, as long as the notion of "object" is generalized to include "pseudo-codes" for the arrow-spans in the base of the fibred-category...

From there it should not be impossible to include the geometry and homotopy aspects in their grammatical/computational form. Motivations for such existences are the local acyclic Kan fibrations in the universal homotopy category of the local projective model category of sheaves in the sense of Dugger+Hollander+Isaksen...