A model of a dependent linear calculus
Résumé
We present a full categorical account, based on Grothendieck fibrations, of what it means for a linear calculus to have dependent types, and we give a term assignment system which merges well with this axiomatization. We construct a model that obeys these categorical axioms, based on the category of graphs.