[Agda] [ cubical ] : Questions on PathP on Sets.

[Apostolis Xekoukoulotakis]

The definition of PathP when it is a path between sets does not make sense
to me.

Here is an example :

```
module test where

open import PathPrelude


-- fun : ∀{ℓ} → {A B : Set ℓ} → A ≡ B → A → B
-- fun eq a = transp eq a

fun2 : ∀{ℓ} → {A B : Set ℓ} → A ≡ B → A → B
fun2 eq a = transp (λ i → eq i) a

fun3 : ∀{ℓ} → {A B : Set ℓ} → A ≡ B → A → B
fun3 eq a = {!!} -- C-u C-u C-c C-,

```
eq ' s type is :
```
eq : PathP (λ _ → Set .ℓ) .A .B
```
but the defintion of PathP is :
```
PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ
```
which means A B must be elements of Sets, not Sets.

Of course A ≡ B is a path inside Set ℓ , thus the definition of PathP makes
no sense with regards to Sets.

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.


I also wonder why I cannot fill the hole with ```r i``` here :
https://github.com/xekoukou/cubical-demo/blob/agda-mailing-list/Univalence.agda#L115
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170915/9810f545/attachment-0001.html>