<div dir="ltr"><div><div><div><div>I&#39;m trying to get a better understanding of the problem by manually translating the definition down to eliminators. First, here&#39;s a version of Conor&#39;s example without mutual induction:<br>

<br>noo : (X : Set) -&gt; (WOne &lt;-&gt; X) -&gt; X -&gt; Zero<br>noo .WOne Refl (wrap f) = noo (Zero → WOne) myIso f<br><br></div>And here are the standard eliminators for WOne and &lt;-&gt;:<br><br>WOne-elim : (P : WOne -&gt; Set) -&gt;<br>

            (m : (f : Zero -&gt; WOne) <br>                 (h : (z : Zero) -&gt; P (f z)) -&gt; <br>                 P (wrap f)) -&gt; <br>            (x : WOne) -&gt; P x<br>WOne-elim P m (wrap f) = m f (λ z → WOne-elim P m (f z)) <br>

<br>&lt;-&gt;-elim : (X : Set) (P : (Y : Set) -&gt; X &lt;-&gt; Y -&gt; Set) -&gt;<br>           (m : P X Refl) -&gt;<br>           (Y : Set) (E : X &lt;-&gt; Y) -&gt; P Y E<br>&lt;-&gt;-elim X P m .X Refl = m<br><br></div>

Now I try to write noo using only these eliminators, to see what goes wrong:<br><br>noo&#39; : (X : Set) -&gt; (WOne &lt;-&gt; X) -&gt; X -&gt; Zero<br>noo&#39; X E x = &lt;-&gt;-elim WOne (λ Y _ → Y → Zero) subgoal X E x<br>

  where<br>    subgoal : WOne -&gt; Zero<br>    subgoal = (WOne-elim (λ _ → Zero) (λ f h → h {!!}))<br><br></div>What I understand of it, is that the order in which we apply the eliminators is important here. We start with x : X, so we cannot apply WOne-elim directly. So we first apply &lt;-&gt;-elim instead, leaving the subgoal ? : WOne -&gt; Zero. Now we can apply WOne-elim, however we are only allowed to make recursive calls to the subgoal, not to noo&#39; itself. In particular, we cannot supply myIso as the argument for WOne &lt;-&gt; X, as it is already fixed to be Refl. I wonder if this problem was already present in &#39;Eliminating Dependent Pattern Matching&#39;, or was introduced later by the termination checker of Agda? This is certainly all very interesting...<br>

<br></div>Jesper<br><div><div><div><br><br></div></div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Jan 8, 2014 at 11:05 AM, Altenkirch Thorsten <span dir="ltr">&lt;<a href="mailto:psztxa@exmail.nottingham.ac.uk" target="_blank">psztxa@exmail.nottingham.ac.uk</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">P.S. An attempt at a summary:<br>
<br>
We already knew that pattern matching is incompatible with univalence<br>
because we can prove K.<br>
<br>
Now, due to the example by Maxime (and Conor) there is another<br>
incompatibilty which arises from pattern matching making things appear<br>
structurally recursive which shouldn&#39;t be.<br>
<br>
This one is not covered by K and it is another example where pattern<br>
matching is non-conservative over the standard eliminators (I guess we<br>
could invent a version of combinators which allow us to use propositional<br>
equality of types during recursion).<br>
<br>
As a consequence it also affects Coq, which always ruled out K but not<br>
this one.<br>
<br>
This is clearly a bug (has anybody filed a bug report) which should be<br>
fixed as a matter of urgency. Any proposals?<br>
<br>
Thorsten<br>
<br>
<br>
On 08/01/2014 09:52, &quot;Altenkirch Thorsten&quot;<br>
<div class="HOEnZb"><div class="h5">&lt;<a href="mailto:psztxa@exmail.nottingham.ac.uk">psztxa@exmail.nottingham.ac.uk</a>&gt; wrote:<br>
<br>
&gt;On 07/01/2014 23:03, &quot;Conor McBride&quot; &lt;<a href="mailto:conor@strictlypositive.org">conor@strictlypositive.org</a>&gt; wrote:<br>
&gt;<br>
&gt;&gt;<br>
&gt;&gt;On 7 Jan 2014, at 22:47, Altenkirch Thorsten<br>
&gt;&gt;&lt;<a href="mailto:psztxa@exmail.nottingham.ac.uk">psztxa@exmail.nottingham.ac.uk</a>&gt; wrote:<br>
&gt;&gt;<br>
&gt;&gt;&gt; Hi Conor,<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; I am sure this must be a stupid question but why is this not covered<br>
&gt;&gt;&gt; by your result that pattern matching can be reduced to eliminators + K?<br>
&gt;&gt;<br>
&gt;&gt;The recursive call isn&#39;t covered by the inductive hypothesis. The direct<br>
&gt;&gt;version<br>
&gt;&gt;gives no account of the inductive hypothesis *at all*, hence the whole<br>
&gt;&gt;mess.<br>
&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; moo (wrap f) = noo (Zero -&gt; WOne) myIso f<br>
&gt;&gt;&gt;&gt;&gt;&gt; noo .WOne Refl x = moo x<br>
&gt;&gt;<br>
&gt;&gt;The recursive call<br>
&gt;&gt;<br>
&gt;&gt;  moo x<br>
&gt;&gt;<br>
&gt;&gt;is really a recursive call<br>
&gt;&gt;<br>
&gt;&gt;  moo (subst myIso ... f)<br>
&gt;&gt;<br>
&gt;&gt;but the inductive hypothesis tells us just that we can call moo on<br>
&gt;&gt;outputs of f.<br>
&gt;&gt;<br>
&gt;&gt;Bottom line: it&#39;s not structurally recursive.<br>
&gt;<br>
&gt;I know this - this was precisely the comment I made in my reply to Maxime.<br>
&gt;<br>
&gt;However, it seems I am a victim of my own propaganda: I was always<br>
&gt;thinking that Conor&#39;s result tells us that we can replace pattern matching<br>
&gt;(with guarded recursion) by elimination constants.<br>
&gt;<br>
&gt;However, this example shows that this is not true. Once we perform the<br>
&gt;unification required by pattern matching we obtain a a term which &quot;looks&quot;<br>
&gt;as if it is structurally smaller even though it isn&#39;t.<br>
&gt;<br>
&gt;One obvious question is how we can recognize good instances of pattern<br>
&gt;matching from bad ones.<br>
&gt;<br>
&gt;This also increases the argument in favour of a safe version of pattern<br>
&gt;matching which is evidence producing. One of my new students, Gabe<br>
&gt;Dijkstra, is working on this - mainly triggered by the without-K issue.<br>
&gt;However, as we see now there are other issues which went unnoticed.<br>
&gt;<br>
&gt;Cheers,<br>
&gt;Thorsten<br>
&gt;<br>
&gt;&gt;<br>
&gt;&gt;Cheers<br>
&gt;&gt;<br>
&gt;&gt;Conor<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; moo&#39;s input is bigger than the third argument in its noo call<br>
&gt;&gt;&gt;&gt; noo&#39;s third input is the same as the argument in its moo call<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; Size-change termination, how are ye?<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; When you do the translation to eliminators, you&#39;re obliged to<br>
&gt;&gt;&gt;&gt; show how recursive calls correspond to invocations of the<br>
&gt;&gt;&gt;&gt; inductive hypothesis: here that&#39;s just not going to happen.<br>
&gt;&gt;&gt;&gt; Transporting f across myIso does indeed give an element of<br>
&gt;&gt;&gt;&gt; WOne (your Box), but that does not make a nullary inductive<br>
&gt;&gt;&gt;&gt; hypothesis any easier to invoke.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; I&#39;d quite like to see us defining a type theory in which the<br>
&gt;&gt;&gt;&gt; only checking is type checking, then using it as a target for<br>
&gt;&gt;&gt;&gt; elaboration. Eliminators are one candidate, but there are<br>
&gt;&gt;&gt;&gt; others. Sized types are certainly another strong candidate.<br>
&gt;&gt;&gt;&gt; I&#39;m also interested to see whether there are &quot;locally clocked&quot;<br>
&gt;&gt;&gt;&gt; explanations for termination, as there seem to be for<br>
&gt;&gt;&gt;&gt; productivity.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; Interesting times<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; Conor<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; bad : Zero<br>
&gt;&gt;&gt;&gt;&gt;&gt; bad = moo (wrap \ ())<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; T.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; I am also not sure how specific the problem is to univalence. As<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;Cody<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; said, I would expect to find some set-theoretical models where the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; equality holds. So being able to prove the negation is disturbing.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Maxime.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; On 01/06/2014 07:23 PM, Abhishek Anand wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; It is known that UIP is inconsistent with univalence.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Does this typecheck even after disabling UIP(==K axiom?) ?<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; I might be wrong, but I think that UIP is baked into the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;typechecker<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of Agda.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; But, UIP can be disabled somehow?<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; -- Abhishek<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; <a href="http://www.cs.cornell.edu/~aa755/" target="_blank">http://www.cs.cornell.edu/~aa755/</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; &lt;<a href="http://www.cs.cornell.edu/%7Eaa755/" target="_blank">http://www.cs.cornell.edu/%7Eaa755/</a>&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; On Mon, Jan 6, 2014 at 3:42 PM, Maxime Dénès &lt;<a href="mailto:mail@maximedenes.fr">mail@maximedenes.fr</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; &lt;mailto:<a href="mailto:mail@maximedenes.fr">mail@maximedenes.fr</a>&gt;&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  Bingo, Agda seems to have the same problem:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  module Termination where<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  open import Relation.Binary.Core<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  data Empty : Set where<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  data Box : Set where<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  wrap : (Empty → Box) → Box<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  postulate<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  iso : (Empty → Box) ≡ Box<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  loop : Box -&gt; Empty<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  loop (wrap x) rewrite iso = loop x<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  gift : Empty → Box<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  gift ()<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  bug : Empty<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  bug = loop (wrap gift)<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  However, I may be missing something due to my ignorance of Agda.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  It may be well known that the axiom I introduced is<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;inconsistent.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  Forgive me if it is the case.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  Maxime.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  On 01/06/2014 01:15 PM, Maxime Dénès wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;      The anti-extensionality bug is indeed related to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;termination.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;      More precisely, it is the subterm relation used by the guard<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;      checker which is not defined quite the right way on<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;dependent<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;      pattern matching.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;      It is not too hard to fix (we have a patch), but doing so<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;      without ruling out any interesting legitimate example<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;(dealing<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;      with recursion on dependently typed data structures) is more<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;      challenging.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;      I am also curious as to whether Agda is impacted. Let&#39;s try<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;it<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; :)<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;      Maxime.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;      On 01/06/2014 12:59 PM, Altenkirch Thorsten wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          Which bug was this?<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          I only saw the one which allowed you to prove<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          anti-extensionality? But<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          this wasn&#39;t related to termination, or?<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          Thorsten<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          On 06/01/2014 16:54, &quot;Cody Roux&quot;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&lt;<a href="mailto:cody.roux@andrew.cmu.edu">cody.roux@andrew.cmu.edu</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          &lt;mailto:<a href="mailto:cody.roux@andrew.cmu.edu">cody.roux@andrew.cmu.edu</a>&gt;&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;              Nice summary!<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;              On 01/06/2014 08:49 AM, Altenkirch Thorsten wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;                  Agda enforces termination via a termination<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;                  checker which is more<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;                  flexible but I think less principled than Coq&#39;s<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;                  approach.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;              That&#39;s a bit scary given that there was an<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;              inconsistency found in<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;              the Coq termination checker just a couple of weeks<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;ago<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; :)<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;              BTW, has anyone tried reproducing the bug in Agda?<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;              Cody<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          This message and any attachment are intended solely for<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          the addressee and may contain confidential information.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;If<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          you have received this message in error, please send it<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          back to me, and immediately delete it. Please do not<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;use,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          copy or disclose the information contained in this<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;message<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          or in any attachment. Any views or opinions expressed by<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          the author of this email do not necessarily reflect the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          views of the University of Nottingham.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          This message has been checked for viruses but the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;contents<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          of an attachment<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          may still contain software viruses which could damage<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;your<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          computer system, you are advised to perform your own<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          checks. Email communications with the University of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;          Nottingham may be monitored as permitted by UK<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; legislation.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;      _______________________________________________<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;      Agda mailing list<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;      <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;      <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  _______________________________________________<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  Agda mailing list<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;  <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; _______________________________________________<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Agda mailing list<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; _______________________________________________<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Agda mailing list<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;<br>
&gt;&gt;<br>
&gt;<br>
&gt;<br>
<br>
</div></div><br>_______________________________________________<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" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>