[HoTT-reading-group] HoTT-reading-group Digest, Vol 2, Issue 4

[J. Ian Johnson]

In regard to the exercise 1.11:

Two different ways:

Theorem neg3neg1 : forall A : Type, (((A -> False) -> False) -> False) -> (A -> False).
Proof.
intros A H a; apply H; intro na; apply na; exact a.
Qed.

Or...

Definition neg3neg1 := (fun (A : Type) (H : (((A -> False) -> False) -> False) (a : A) => H (fun na : A -> False => na a)).

Exercise 1.13
Theorem no_undecidable : forall A: Prop, ~ ~ (A \/ ~ A).
Proof.
intros A Hneg.
assert (nnp : ~ ~ A) by (intro np; apply Hneg; right; assumption).
apply nnp; intro a; apply Hneg; left; assumption.
Qed.

Or...
Definition no_undecidable :=
fun (A : Prop) (Hneg : ~ (A \/ ~ A)) =>
(fun nnp : ~ ~ A => nnp (fun a : A => Hneg (or_introl a)))
  (fun np : ~ A => Hneg (or_intror np)).

Dave's question 
Definition Fib {A B} (f : A -> B) (y : B) := sigT (fun x => (f x) =T y).

Theorem Dave : forall A B C (f : A -> B + C), sum (sigT (fun b => Fib f (inl b))) (sigT (fun c => Fib f (inr c))) -> A.
Proof.
intros A B C f H.
inversion H as [l|r].
destruct l as [? [a ?]]; exact a.
destruct r as [? [a ?]]; exact a.
Qed. 

Jason on the collapsing of equalities to refl:
Definition Is_Contr (A : Type) := sigT (fun x : A => (forall y, x =T y)).

Theorem jgross : forall A (x : A), Is_Contr (sigT (fun y => y =T x)).
Proof.
  intros A x.
  assert (sigT (fun y => y =T x)).
  exists x; reflexivity.
  exists X.
  intros [y prf].
  induction prf.
  destruct X as [y_ prf_].
  induction prf_; reflexivity.
Qed.

----- Original Message -----
From: "Darij Grinberg" <darijgrinberg at gmail.com>
To: "Michael M" <tactics40 at gmail.com>
Cc: "hott-reading-group" <hott-reading-group at mit.edu>
Sent: Monday, January 13, 2014 3:02:36 PM GMT -05:00 US/Canada Eastern
Subject: Re: [HoTT-reading-group] HoTT-reading-group Digest, Vol 2, Issue 4

Same here!

On Mon, Jan 13, 2014 at 9:01 PM, Michael M <tactics40 at gmail.com> wrote:
> Can someone link me to the Google Hangout? I don't have voice, but I'd like
> to sit in and listen, if it's not too much trouble.
>
> _______________________________________________
> HoTT-reading-group mailing list
> HoTT-reading-group at mit.edu
> http://mailman.mit.edu/mailman/listinfo/hott-reading-group
>
_______________________________________________
HoTT-reading-group mailing list
HoTT-reading-group at mit.edu
http://mailman.mit.edu/mailman/listinfo/hott-reading-group