[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

[Andrea Vezzosi]

On Fri, Sep 15, 2017 at 5:16 AM, Apostolis Xekoukoulotakis

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

Maybe you are missing that "Set ℓ : Set (ℓ-suc ℓ )"? i.e. the type of
types "Set ℓ" is itself an element of the type of larger types "Set
(ℓ-suc ℓ )".

If you look at the implicit arguments you'll see that you have

eq : PathP {ℓ-suc .ℓ} (λ _ → Set .ℓ) .A .B

Also note that "Set" is just the traditional name Agda uses for
universes, it's not related to hSets

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.

Right, "A ≡ B" and "(I -> Set ℓ)" are different types, both
constructed by lambdas, so you are actually converting between them on
the fly by performing the expansion.

Maybe we will introduce some subtyping to make this transparent to the user.

https://github.com/xekoukou/cubical-demo/blob/agda-mailing-list/Univalence.agda#L115

I will try to look at that more closely soon.

Cheers,
Andrea

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Apostolis Xekoukoulotakis]

So, the type of ```(λ _ → Set .ℓ)``` is ```(I -> Set (ℓ-suc .ℓ))```.

Regarding, ```A ≡ B``` and ```(I -> Set ℓ)```, I think I got it.

So my problem with the proof would most certainly have to do because I was
conflating them. I will look into it and come with more questions if
necessary.

Post by Andrea Vezzosi
On Fri, Sep 15, 2017 at 5:16 AM, Apostolis Xekoukoulotakis

Post by Apostolis Xekoukoulotakis
```
eq : PathP (λ _ → Set .ℓ) .A .B
```
```
PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ
```
which means A B must be elements of Sets, not Sets.

Maybe you are missing that "Set ℓ : Set (ℓ-suc ℓ )"? i.e. the type of
types "Set ℓ" is itself an element of the type of larger types "Set
(ℓ-suc ℓ )".
If you look at the implicit arguments you'll see that you have
eq : PathP {ℓ-suc .ℓ} (λ _ → Set .ℓ) .A .B
Also note that "Set" is just the traditional name Agda uses for
universes, it's not related to hSets

Post by Apostolis Xekoukoulotakis
Another problem I am experiencing that might be related is that A=B

requires

Post by Apostolis Xekoukoulotakis
to be eta-abstracted to work like in the fun/fun2 case.

Right, "A ≡ B" and "(I -> Set ℓ)" are different types, both
constructed by lambdas, so you are actually converting between them on
the fly by performing the expansion.
Maybe we will introduce some subtyping to make this transparent to the user.

Post by Apostolis Xekoukoulotakis
https://github.com/xekoukou/cubical-demo/blob/agda-

mailing-list/Univalence.agda#L115
I will try to look at that more closely soon.
Cheers,
Andrea

Post by Apostolis Xekoukoulotakis
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda