Ok, thank you. I think I will just have to sit down and write up what these conditions mean explicitly as axioms in my logic.
In general I feel category theory is a somewhat clumsy way of encoding higher-order things in a first-order way, but on the other hand I think the various type theories are not the right way to declumsify this. But that's just an impression, hopefully I will know more soon.
Comments
Ok, thank you. I think I will just have to sit down and write up what these conditions mean explicitly as axioms in my logic.
In general I feel category theory is a somewhat clumsy way of encoding higher-order things in a first-order way, but on the other hand I think the various type theories are not the right way to declumsify this. But that's just an impression, hopefully I will know more soon.