<div dir="ltr">Yes. The counter-example is where you send the base-point to Bool, but the loop to the non-trivial path Bool = Bool. There's some code at the bottom that brings the proof obligation to a state negb x = x, which is obviously false. I suspect you might be able to prove something useful by trying to factor eta into a "hiding information" part (e.g., truncation) and an "adding information" part (e.g., cross with circle), and if your adding information is non-trivial (i.e., the type has any provably non-trivial higher homotopy group), then you should be able to discriminate on that information to break the induction principle. And if your modality only hides information, you might be able to prove (iv) from the (i)-(iii).<div>
<br></div><div><br></div><div>Code:</div><div><br></div><div><div style="font-family:arial,sans-serif;font-size:13px">Require Import HoTT.</div><div style="font-family:arial,sans-serif;font-size:13px"><br></div><div style="font-family:arial,sans-serif;font-size:13px">
Section circ_not_modality.</div><div style="font-family:arial,sans-serif;font-size:13px"> Context `{Univalence}.</div><div style="font-family:arial,sans-serif;font-size:13px"> Definition mod := fun A => A * S1.</div>
<div style="font-family:arial,sans-serif;font-size:13px"> </div><div style="font-family:arial,sans-serif;font-size:13px"> Definition modality_eta : forall A, A -> mod A</div><div style="font-family:arial,sans-serif;font-size:13px">
:= fun A a => (a, base).</div><div style="font-family:arial,sans-serif;font-size:13px"> </div><div style="font-family:arial,sans-serif;font-size:13px"> Definition modality_ind : forall A (B : mod A -> Type),</div>
<div style="font-family:arial,sans-serif;font-size:13px"> (forall a, mod (B (modality_eta _ a)))</div><div style="font-family:arial,sans-serif;font-size:13px"> -> forall z, mod (B z).</div>
<div style="font-family:arial,sans-serif;font-size:13px"> Proof.</div><div style="font-family:arial,sans-serif;font-size:13px"> unfold mod, modality_eta.</div><div style="font-family:arial,sans-serif;font-size:13px">
intros A B f [a c].</div>
<div style="font-family:arial,sans-serif;font-size:13px"> revert c.</div><div style="font-family:arial,sans-serif;font-size:13px"> apply (@S1_rect (fun c => B (a, c) * S1) (f a)); simpl in *.</div><div style="font-family:arial,sans-serif;font-size:13px">
generalize (f a).</div><div style="font-family:arial,sans-serif;font-size:13px"> clear f.</div><div style="font-family:arial,sans-serif;font-size:13px"> intro fa.</div><div style="font-family:arial,sans-serif;font-size:13px">
rewrite transport_prod.</div><div style="font-family:arial,sans-serif;font-size:13px"> destruct fa as [fa0 fa1]; simpl.</div><div style="font-family:arial,sans-serif;font-size:13px"> rewrite transport_const.</div>
<div style="font-family:arial,sans-serif;font-size:13px"> apply path_prod; simpl; try reflexivity.</div><div style="font-family:arial,sans-serif;font-size:13px"> SearchAbout (transport (fun _ => _ * _)).</div><div style="font-family:arial,sans-serif;font-size:13px">
<br></div><div style="font-family:arial,sans-serif;font-size:13px"> pose Unit as A'.</div><div style="font-family:arial,sans-serif;font-size:13px"> pose (fun ac : A' * S1 => S1_rectnd Type Bool (path_universe negb) (snd ac)) as B'.</div>
<div style="font-family:arial,sans-serif;font-size:13px"> pose (tt : A') as a'.</div><div style="font-family:arial,sans-serif;font-size:13px"> assert (fa' : B' (a', base)) by admit.</div><div style="font-family:arial,sans-serif;font-size:13px">
assert (transport (fun c : S1 => B' (a', c)) loop fa' = fa').</div><div style="font-family:arial,sans-serif;font-size:13px"> clear.</div><div style="font-family:arial,sans-serif;font-size:13px">
subst A' B' a'; simpl in *.</div>
<div style="font-family:arial,sans-serif;font-size:13px"> SearchAbout transport ap.</div><div style="font-family:arial,sans-serif;font-size:13px"> rewrite transport_idmap_ap.</div><div style="font-family:arial,sans-serif;font-size:13px">
rewrite S1_rectnd_beta_loop.</div><div style="font-family:arial,sans-serif;font-size:13px"> rewrite transport_path_universe.</div><div><br></div><div><br></div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">
On Tue, Apr 1, 2014 at 11:59 AM, Joe Hannon <span dir="ltr"><<a href="mailto:hannon@math.bu.edu" target="_blank">hannon@math.bu.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr">So Chris gave a counterexample to the assertion that crossing with a circle satisfies 7.7.5 i-iii but not iv?<br></div><div class="gmail_extra"><br><br><div class="gmail_quote"><div><div class="h5">On Tue, Apr 1, 2014 at 1:28 AM, Jason Gross <span dir="ltr"><<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>></span> wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><div dir="ltr">Hi,<div>This week, we talked about a variety of things, including how to construct the circle as the homotopy colimit of a diagram containing only the unit type, the difference between homotopy colimits and (regular) colimits, the homotopy groups of spheres, the univalence axiom for categories, simplicial types, and various problems with defining infinity categories in HoTT. (I referenced some posts by Mike Shulman, which are available <a href="http://golem.ph.utexas.edu/category/2012/06/directed_homotopy_type_theory.html" target="_blank">here</a>, <a href="https://golem.ph.utexas.edu/category/2013/03/category_theory_in_homotopy_ty.html" target="_blank">here</a>, and <a href="http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/" target="_blank">here</a>.) We also talked about whether or not one of the axioms for the definition of a modality is redundant, and Chris came up with a counter-example to an idea I had about product-with-the-circle.</div>
<div><br></div><div>For next week, please, again, have read chapter 7 (homotopy n-types). The exercises I suggested last time were 7.1, 7.2, and 7.12. If you're looking for more exercises, feel free to also try 7.5 and 7.14. You can also think about whether or not 7.7.5(iv) is redundant.</div>
<span><font color="#888888">
<div><br></div><div>-Jason </div></font></span></div>
<br></div></div>_______________________________________________<br>
HoTT-reading-group mailing list<br>
<a href="mailto:HoTT-reading-group@mit.edu" target="_blank">HoTT-reading-group@mit.edu</a><br>
<a href="http://mailman.mit.edu/mailman/listinfo/hott-reading-group" target="_blank">http://mailman.mit.edu/mailman/listinfo/hott-reading-group</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>