<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
Indeed, it would be clearer to present the Glue, unglue construction at the pre-type
<div class="">level. If we have A and a partial map w: T -> A defined on phi then we can find an extension</div>
<div class=""><br class="">
</div>
<div class=""> G = Glue (A, phi, w) and unglue : G -> A</div>
<div class=""><br class="">
</div>
<div class="">such that (G,unglue) = (T,w) on the extent phi.</div>
<div class=""> This can be done for any function w.</div>
<div class=""><br class="">
</div>
<div class=""><br class="">
</div>
<div class=""> The main Lemma is then that if A, T are fibrant and w is an equivalence, then G is fibrant</div>
<div class="">and unglue is an equivalence. </div>
<div class="">(This expresses that the type Sigma (X:U) Equiv X A is contractible, which is one way</div>
<div class="">to state univalence.)</div>
<div class=""><br class="">
</div>
<div class="">Best, Thierry<br class="">
<div class=""><br class="">
<div class=""><br class="">
<div><br class="">
<blockquote type="cite" class="">
<div class="">On 20 May 2020, at 11:34, Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" class="">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<div class="WordSection1" style="page: WordSection1; caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;">
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class="">Hi,<o:p class=""></o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class=""><o:p class=""> </o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class="">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<o:p class=""></o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class=""><o:p class=""> </o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class="">MyGlue : (A : Set) {φ : I}<o:p class=""></o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class=""> → Partial φ (Σ[ T<span class="Apple-converted-space"> </span></span><span style="font-size: 11pt; font-family: "Cambria Math", serif;" class="">∈</span><span style="font-size: 11pt;" class=""><span class="Apple-converted-space"> </span>Set
] T<span class="Apple-converted-space"> </span></span><span style="font-size: 11pt; font-family: "Cambria Math", serif;" class="">≃</span><span style="font-size: 11pt;" class="">' A) → Set<o:p class=""></o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class="">MyGlue A {φ} Te = Σ (PartialP φ λ o → fst (Te o)) (λ t → A [ φ<span class="Apple-converted-space"> </span></span><span style="font-size: 11pt; font-family: "Cambria Math", serif;" class="">↦</span><span style="font-size: 11pt;" class=""><span class="Apple-converted-space"> </span>(λ
p → fst (snd (Te p)) (t p)) ])<o:p class=""></o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class=""><o:p class=""> </o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class="">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<o:p class=""></o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class=""><o:p class=""> </o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class="">ua : {A B : Set} → (p : A<span class="Apple-converted-space"> </span></span><span style="font-size: 11pt; font-family: "Cambria Math", serif;" class="">≃</span><span style="font-size: 11pt;" class="">' B) → A ≡ B<o:p class=""></o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class=""><o:p class=""> </o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class="">because we need the extra definitional equality<o:p class=""></o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class=""><o:p class=""> </o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class="">
<span lang="DE" style="font-size: 11pt;" class="">MyGlue A i1 (T , e) = T<o:p class=""></o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span lang="DE" style="font-size: 11pt;" class=""><o:p class=""> </o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class="">Is there a way to avoid this? This is not a provable equality either, I think.<o:p class=""></o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class=""><o:p class=""> </o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class="">Cheers,<o:p class=""></o:p></span></div>
<div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: Calibri, sans-serif;" class="">
<span style="font-size: 11pt;" class="">Thorsten<o:p class=""></o:p></span></div>
</div>
<pre style="caret-color: rgb(0, 0, 0); font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class="">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.
</pre>
<br class="Apple-interchange-newline">
</div>
</blockquote>
</div>
<br class="">
</div>
</div>
</div>
</body>
</html>