Relating Justification Logic Modality and Type Theory in Curry–Howard Fashion