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

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

On Fri, Sep 15, 2017 at 2:51 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> 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
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170915/bba0509f/attachment.html>