Suppose I have

  • cong : {A B : Type} (f : A -> B) (p : a = b) : f a = f b
  • coe : (A : I -> Type) -> A 0 -> A 1

It is a common pattern in less crude type theory that we implement =-trans as =-trans : {a b c : A} (p : a = b) (q : b = c) : a = c := coe (cong (\x. a = x) q) p But in this case, \x => a = x is of type A -> Type, where the codomain and domain does not live in the same universe, as demanded by cong. Is there a clever way to add some lifts in =-trans to make the code type check or do I have to inline cong?

  • $\begingroup$ What about having A and B live at possibly different universes? Would this solve your issue? Otherwise, if you start playing around with lifting, I fear you will only be able to prove a degraded version of your goal, typically something like lift a = lift c (an equality that relates the liftings of a and c to the type A moved one universe up). $\endgroup$ Commented Nov 7, 2022 at 14:43


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.