<div dir="ltr"><div><div>The definition of PathP when it is a path between sets does not make sense to me.<br><br></div>Here is an example : <br><br>```<br>module test where<br><br>open import PathPrelude<br><br><br>-- fun : ∀{ℓ} → {A B : Set ℓ} → A ≡ B → A → B<br>-- fun eq a = transp eq a<br><br>fun2 : ∀{ℓ} → {A B : Set ℓ} → A ≡ B → A → B<br>fun2 eq a = transp (λ i → eq i) a<br><br>fun3 : ∀{ℓ} → {A B : Set ℓ} → A ≡ B → A → B<br>fun3 eq a = {!!} -- C-u C-u C-c C-,<br><br>```<br></div>eq ' s type is :<br><div>```<br>eq : PathP (λ _ → Set .ℓ) .A .B<br></div><div>```<br>but the defintion of PathP is :<br>```</div><div>PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ<br></div><div>```</div><div>which means A B must be elements of Sets, not Sets.<br></div><div><br></div><div>Of course A ≡ B is a path inside Set ℓ , thus the definition of PathP makes no sense with regards to Sets.<br></div><div><br></div><div>Another problem I am experiencing that might be related is that A=B requires to be eta-abstracted to work like in the fun/fun2 case.</div><div><br></div><div><br></div><div>I also wonder why I cannot fill the hole with ```r i``` here :</div><div><a href="https://github.com/xekoukou/cubical-demo/blob/agda-mailing-list/Univalence.agda#L115">https://github.com/xekoukou/cubical-demo/blob/agda-mailing-list/Univalence.agda#L115</a><br></div></div>