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

[Andrea Vezzosi]

On Fri, Sep 15, 2017 at 5:16 AM, Apostolis Xekoukoulotakis
<apostolis.xekoukoulotakis at gmail.com> wrote:
> 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.

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.

>
> 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

I will try to look at that more closely soon.

Cheers,
Andrea

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