Handling heterogeneous paths in a set

Question

I have two heterogeneous paths in a Set, with the same endpoints but over different paths. How do I fill in between them?

In more concrete terms, here's my code with foo being my question:

{-# OPTIONS --cubical #-}

module _ where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything hiding (assoc)

variable
  ℓ : Level
  A : Type ℓ
  B : A → Type ℓ
  x y : A

module _
  (AIsSet : isSet A)
  (p q : Path A x y)
  (BIsProp : ∀ x → isProp (B x))
  {x′ : B x}
  {y′ : B y}
  where

  p′ : PathP (λ i → B (p i)) x′ y′
  p′ = isProp→PathP BIsProp p x′ y′

  q′ : PathP (λ i → B (q i)) x′ y′
  q′ = isProp→PathP BIsProp q x′ y′

  foo : PathP (λ i → PathP (λ j → B (AIsSet x y p q i j)) x′ y′) p′ q′
  foo = ?
    where
      doesThisHelp? : ∀ j → PathP (λ i → B (AIsSet x y p q i j)) (p′ j) (q′ j)
      doesThisHelp? j = isProp→PathP BIsProp (λ i → AIsSet x y p q i j) (p′ j) (q′ j)

Answer 1

This is when you want to use isOfHLevel→isOfHLevelDep:

  foo : PathP (λ i → PathP (λ j → B (AIsSet x y p q i j)) x′ y′) p′ q′
  foo = let r = isOfHLevel→isOfHLevelDep {n = 2} (\ a → hLevelSuc 1 (B a) (BIsProp a)) in
        r x′ y′ p′ q′ (AIsSet x y p q)

doesThisHelp? probably does not, as it is building a square where two of the sides are p' and q' but you don't know what the other two sides are. While foo specifies the other two sides to be (constantly) x' and y'.