Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeFeb 20th 2015
   • (edited Feb 20th 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexthe MO discussion [here](http://mathoverflow.net/a/196458/381) mentions "justification logic" as a possible means to consider groupoids whose morphisms are proofs of equivalences. That certainly smells a lot like the basic idea of (homotopy) type theory. Is such a relation between justification logic and (homotopy) type theory discussed anywhere? Googling for these terms mainly shows one person asking the same question [here on Philosophy.SE](http://philosophy.stackexchange.com/questions/15609/is-there-any-relation-beetwen-justification-logic-and-type-theory), but not having received any reply -- and shows pointers to a language "[J-Calc](http://www.sciencedirect.com/science/article/pii/S1571066113000923)" which might just be the type-theoretic formulation of justification logic. (?)

   the MO discussion here mentions “justification logic” as a possible means to consider groupoids whose morphisms are proofs of equivalences. That certainly smells a lot like the basic idea of (homotopy) type theory. Is such a relation between justification logic and (homotopy) type theory discussed anywhere?

   Googling for these terms mainly shows one person asking the same question here on Philosophy.SE, but not having received any reply – and shows pointers to a language “J-Calc” which might just be the type-theoretic formulation of justification logic. (?)