[HoTT-reading-group] Chapter 7

[Jason Gross]

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).


Code:

Require Import HoTT.

Section circ_not_modality.
  Context `{Univalence}.
  Definition mod := fun A => A * S1.

  Definition modality_eta : forall A, A -> mod A
    := fun A a => (a, base).

  Definition modality_ind : forall A (B : mod A -> Type),
                              (forall a, mod (B (modality_eta _ a)))
                              -> forall z, mod (B z).
  Proof.
    unfold mod, modality_eta.
    intros A B f [a c].
    revert c.
    apply (@S1_rect (fun c => B (a, c) * S1) (f a)); simpl in *.
    generalize (f a).
    clear f.
    intro fa.
    rewrite transport_prod.
    destruct fa as [fa0 fa1]; simpl.
    rewrite transport_const.
    apply path_prod; simpl; try reflexivity.
    SearchAbout (transport (fun _ => _ * _)).

    pose Unit as A'.
    pose (fun ac : A' * S1 => S1_rectnd Type Bool (path_universe negb) (snd
ac)) as B'.
    pose (tt : A') as a'.
    assert (fa' : B' (a', base)) by admit.
    assert (transport (fun c : S1 => B' (a', c)) loop fa' = fa').
    clear.
    subst A' B' a'; simpl in *.
    SearchAbout transport ap.
    rewrite transport_idmap_ap.
    rewrite S1_rectnd_beta_loop.
    rewrite transport_path_universe.




On Tue, Apr 1, 2014 at 11:59 AM, Joe Hannon <hannon at math.bu.edu> wrote:

> So Chris gave a counterexample to the assertion that crossing with a
> circle satisfies 7.7.5 i-iii but not iv?
>
>
> On Tue, Apr 1, 2014 at 1:28 AM, Jason Gross <jasongross9 at gmail.com> wrote:
>
>> Hi,
>> 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 here<http://golem.ph.utexas.edu/category/2012/06/directed_homotopy_type_theory.html>,
>> here<https://golem.ph.utexas.edu/category/2013/03/category_theory_in_homotopy_ty.html>,
>> and here<http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/>.)
>>  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.
>>
>> 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.
>>
>> -Jason
>>
>> _______________________________________________
>> HoTT-reading-group mailing list
>> HoTT-reading-group at mit.edu
>> http://mailman.mit.edu/mailman/listinfo/hott-reading-group
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140401/32674d47/attachment.htm