[Agda] Understanding Glue

[Andreas Nuyts]

Hi Thorsten,

Your implementation is also what Orton and Pitts do in their internal 
model of cubical type theory:
https://doi.org/10.23638/LMCS-14(4:23)2018

They rely on an additional axiom, the strictness axiom, to strictify 
MyGlue so that it actually extends T.

Note that this implementation only relies on one direction of the 
equivalence. This is the only direction needed to form Glue (up to iso 
or relying on the strictness axiom) as a pre-type. The other direction 
is needed to make it Kan fibrant.
I am now puzzled by the fact that this means that you can define a 
non-Kan type in cubical Agda. I guess "Partial" is a non-fibrant type 
former? Does Agda somehow prevent the user to exploit Kan-fibrancy of 
types constructed using "Partial"?

Best regards,
Andreas

On 20/05/2020 11:34, Thorsten Altenkirch wrote:
>
> Hi,
>
> I am trying to understand the Glue construction better. I was 
> wondering whether Glue just means that a certain pre-type is fibrant 
> (i.e. admits composition, i.e. transp and hcomp). I was trying in agda
>
> MyGlue : (A : Set) {φ : I}
>
>      → Partial φ (Σ[ T ∈Set ] T ≃' A) → Set
>
> MyGlue A {φ} Te = Σ (PartialP φ λ o → fst (Te o)) (λ t → A [ φ ↦(λ p → 
> fst (snd (Te p)) (t p)) ])
>
> I have switched off universe checking, hence Setw = Set. Basically I 
> have used the domain of glue as the definition of Glue. However, this 
> doesn’t seem enough to derive
>
> ua : {A B : Set} → (p : A ≃' B) → A ≡ B
>
> because we need the extra definitional equality
>
> MyGlue A i1 (T , e) = T
>
> Is there a way to avoid this? This is not a provable equality either, 
> I think.
>
> Cheers,
>
> Thorsten
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> _______________________________________________
> 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/20200520/09fd5665/attachment.html>