Library UniMath.MoreFoundations.NullHomotopies
Require Export UniMath.Foundations.PartD.
Require Import UniMath.Foundations.UnivalenceAxiom.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.MoreFoundations.Notations.
Local Open Scope transport.
Definition nullHomotopyTo {X Y} (f:X->Y) (y:Y) := ∏ x:X, f x = y.
Definition NullHomotopyTo {X Y} (f:X->Y) := total2 (nullHomotopyTo f).
Definition NullHomotopyTo_center {X Y} (f:X->Y) : NullHomotopyTo f -> Y := pr1.
Definition NullHomotopyTo_path {X Y} {f:X->Y} (r:NullHomotopyTo f) := pr2 r.
Definition nullHomotopyFrom {X Y} (f:X->Y) (y:Y) := ∏ x:X, y = f x.
Definition NullHomotopyFrom {X Y} (f:X->Y) := total2 (nullHomotopyFrom f).
Definition NullHomotopyFrom_center {X Y} (f:X->Y) : NullHomotopyFrom f -> Y := pr1.
Definition NullHomotopyFrom_path {X Y} {f:X->Y} (r:NullHomotopyFrom f) := pr2 r.
Definition nullHomotopyTo_transport {X Y} {f:X->Y} {y:Y} (h : nullHomotopyTo f y)
{y':Y} (p:y = y') (x:X) : (p # h) x = h x @ p.
Show proof.
Lemma isaset_NullHomotopyTo {X Y} (i:isaset Y) (f:X->Y) : isaset (NullHomotopyTo f).
Show proof.
intros. apply (isofhleveltotal2 2).
{ apply i. }
intros y. apply impred; intros x. apply isasetaprop. apply i.
{ apply i. }
intros y. apply impred; intros x. apply isasetaprop. apply i.
Lemma isaprop_nullHomotopyTo {X Y} (is:isaset Y) (f:X->Y) (y:Y) :
isaprop (nullHomotopyTo f y).
Show proof.
Lemma isaprop_NullHomotopyTo {X} {Y} (is:isaset Y) (f:X->Y) :
∥ X ∥ -> isaprop (NullHomotopyTo f).
Show proof.
apply factor_through_squash.
apply isapropisaprop.
intros x. apply invproofirrelevance. intros [r i] [s j].
apply subtypePairEquality.
- intros n. apply (isaprop_nullHomotopyTo is).
- exact (!i x @ j x).
apply isapropisaprop.
intros x. apply invproofirrelevance. intros [r i] [s j].
apply subtypePairEquality.
- intros n. apply (isaprop_nullHomotopyTo is).
- exact (!i x @ j x).
Definition cone_squash_map {X Y} (f:X->Y) (y:Y) :
nullHomotopyTo f y -> ∥ X ∥ -> Y.
Show proof.
Goal ∏ X Y (y:Y) (f:X->Y) (e:∏ m:X, f m = y),
f = cone_squash_map f y e ∘ squash_element.
Show proof.
reflexivity.