Made substInPaths slightly more general by allowing A and B to be dif…

…ferent levels (#1076)
agda · Oct 31, 2023 · b3738bf · b3738bf
1 parent b822ba9
commit b3738bf
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Cubical/Foundations/Transport.agda b/Cubical/Foundations/Transport.agda
@@ -174,7 +174,7 @@ overPathFunct p q =
 
 -- substition over families of paths
 -- theorem 2.11.3 in The Book
-substInPaths : ∀ {ℓ} {A B : Type ℓ} {a a' : A}
+substInPaths : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}  {a a' : A}
                  → (f g : A → B) → (p : a ≡ a') (q : f a ≡ g a)
                  → subst (λ x → f x ≡ g x) p q ≡ sym (cong f p) ∙ q ∙ cong g p
 substInPaths {a = a} f g p q =