Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeFeb 20th 2015
    • (edited Feb 20th 2015)

    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. (?)