Improve and add a few path operators (#746)

* Change type symP for better goal inference.

* Add implicit args to substRefl in order to be able to specify A.

* fromPathP⁻ and toPathP⁻

* Adapt to changed symP.

Co-authored-by: Andreas Nuyts <andreas.nuyts@vub.ac.be>

Cubical/Categories/Category/Properties.agda

@@ -92,7 +92,8 @@ module _ {C : Category ℓ ℓ'} where
                   → (f : C [ x , y ]) (g : C [ y , z ]) (g' : C [ y' , z ])
                   → (r : PathP (λ i → C [ p i , z ]) g g')
                   → f ⋆⟨ C ⟩ g ≡ seqP {p = p} f g'
-  lCatWhiskerP f g g' r = cong (λ v → f ⋆⟨ C ⟩ v) (sym (fromPathP (symP r)))
+  lCatWhiskerP {z = z} {p = p} f g g' r =
+    cong (λ v → f ⋆⟨ C ⟩ v) (sym (fromPathP (symP {A = λ i → C [ p (~ i) , z ]} r)))
 
   rCatWhiskerP : {x y' y z : C .ob} {p : y' ≡ y}
                   → (f' : C [ x , y' ]) (f : C [ x , y ]) (g : C [ y , z ])

Cubical/Foundations/Path.agda

@@ -22,6 +22,13 @@ cong′ : ∀ {B : Type ℓ'} (f : A → B) {x y : A} (p : x ≡ y)
 cong′ f = cong f
 {-# INLINE cong′ #-}
 
+module _ {A : I → Type ℓ} {x : A i0} {y : A i1} where
+  toPathP⁻ : x ≡ transport⁻ (λ i → A i) y → PathP A x y
+  toPathP⁻ p = symP (toPathP (sym p))
+
+  fromPathP⁻ : PathP A x y → x ≡ transport⁻ (λ i → A i) y
+  fromPathP⁻ p = sym (fromPathP {A = λ i → A (~ i)} (symP p))
+
 PathP≡Path : ∀ (P : I → Type ℓ) (p : P i0) (q : P i1) →
              PathP P p q ≡ Path (P i1) (transport (λ i → P i) p) q
 PathP≡Path P p q i = PathP (λ j → P (i ∨ j)) (transport-filler (λ j → P j) p i) q

Cubical/Foundations/Prelude.agda

@@ -50,8 +50,8 @@ sym : x ≡ y → y ≡ x
 sym p i = p (~ i)
 {-# INLINE sym #-}
 
-symP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} →
-       (p : PathP A x y) → PathP (λ i → A (~ i)) y x
+symP : {A : I → Type ℓ} → {x : A i1} → {y : A i0} →
+       (p : PathP (λ i → A (~ i)) x y) → PathP A y x
 symP p j = p (~ j)
 
 cong : (f : (a : A) → B a) (p : x ≡ y) →
@@ -261,7 +261,7 @@ subst2 : ∀ {ℓ' ℓ''} {B : Type ℓ'} {z w : B} (C : A → B → Type ℓ'')
         (p : x ≡ y) (q : z ≡ w) → C x z → C y w
 subst2 B p q b = transport (λ i → B (p i) (q i)) b
 
-substRefl : (px : B x) → subst B refl px ≡ px
+substRefl : ∀ {B : A → Type ℓ} {x} → (px : B x) → subst B refl px ≡ px
 substRefl px = transportRefl px
 
 subst-filler : (B : A → Type ℓ') (p : x ≡ y) (b : B x)