<div dir="ltr"><div><div>So, the type of ```(λ _ → Set .ℓ)``` is ```(I -> Set (ℓ-suc .ℓ))```.<br><br></div>Regarding, ```A ≡ B``` and ```(I -> Set ℓ)```, I think I got it. <br><br></div>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.<br> </div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Sep 15, 2017 at 2:51 PM, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Fri, Sep 15, 2017 at 5:16 AM, Apostolis Xekoukoulotakis<br>
<<a href="mailto:apostolis.xekoukoulotakis@gmail.com">apostolis.xekoukoulotakis@<wbr>gmail.com</a>> wrote:<br>
> eq ' s type is :<br>
> ```<br>
> eq : PathP (λ _ → Set .ℓ) .A .B<br>
> ```<br>
> but the defintion of PathP is :<br>
> ```<br>
> PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ<br>
> ```<br>
> which means A B must be elements of Sets, not Sets.<br>
<br>
</span>Maybe you are missing that "Set ℓ : Set (ℓ-suc ℓ )"? i.e. the type of<br>
types "Set ℓ" is itself an element of the type of larger types "Set<br>
(ℓ-suc ℓ )".<br>
<br>
If you look at the implicit arguments you'll see that you have<br>
<br>
eq : PathP {ℓ-suc .ℓ} (λ _ → Set .ℓ) .A .B<br>
<br>
Also note that "Set" is just the traditional name Agda uses for<br>
universes, it's not related to hSets<br>
<span class=""><br>
><br>
> Another problem I am experiencing that might be related is that A=B requires<br>
> to be eta-abstracted to work like in the fun/fun2 case.<br>
<br>
</span>Right, "A ≡ B" and "(I -> Set ℓ)" are different types, both<br>
constructed by lambdas, so you are actually converting between them on<br>
the fly by performing the expansion.<br>
<br>
Maybe we will introduce some subtyping to make this transparent to the user.<br>
<span class=""><br>
><br>
> I also wonder why I cannot fill the hole with ```r i``` here :<br>
> <a href="https://github.com/xekoukou/cubical-demo/blob/agda-mailing-list/Univalence.agda#L115" rel="noreferrer" target="_blank">https://github.com/xekoukou/<wbr>cubical-demo/blob/agda-<wbr>mailing-list/Univalence.agda#<wbr>L115</a><br>
<br>
</span>I will try to look at that more closely soon.<br>
<br>
Cheers,<br>
Andrea<br>
<br>
> ______________________________<wbr>_________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
><br>
</blockquote></div><br></div>