Author: jonatan Format: TextI am reading The Book about homotopical type theory http://homotopytypetheory.org/book/ and I have idea - can homotopical type theory be use as the real model of logic something like usual set theory is used as the model for the standard logics. Are such models already construcuted. If multiple types (sorts) are allowed then combination of logics can come naturally. What else new results can be gained from such new kinds of models? Can they allow to prove completeness and soundness more easily, can they be used to faster arrive at the computable semantics that can be used for building reasoners (solvers)?
I am reading The Book about homotopical type theory http://homotopytypetheory.org/book/ and I have idea - can homotopical type theory be use as the real model of logic something like usual set theory is used as the model for the standard logics. Are such models already construcuted. If multiple types (sorts) are allowed then combination of logics can come naturally. What else new results can be gained from such new kinds of models? Can they allow to prove completeness and soundness more easily, can they be used to faster arrive at the computable semantics that can be used for building reasoners (solvers)?