namespace latin:/❚

fixmeta ur:?LF❚

theory TypeEquality =
  include ?TypedLogic❙
  structure tpeq : ?EqualityND =
    include ?Logic❙
    term = tp❙
    equal # 1 ≛ 2 prec 50❙   
  ❚
❚

theory Transport =
  include ?TypeEquality❙
  include ?TypedEqualityND❙
  
  congTp : {A, X,Y} ⊦ X≐Y ⟶ {B: tm A ⟶ tp} ⊦ B X ≛ B Y❘# 4 congTp 5❙  
  
  transport : {A, B} ⊦ A ≛ B ⟶ tm A ⟶ tm B❘# 4 ↑ 3 prec 70❙
  transport_refl: {A,X: tm A} ⊦ X↑tpeq/refl ≐ X❙

  // Doesn't typecheck:
  transport_trans: {A,B,C, X: tm A, p:⊦ A ≛ B, q: ⊦ B ≛ C} ⊦ X↑p↑q ≐ X↑(tpeq/eq/trans p q)❙
❚