Whitehead's Lemma (#1067)

* Whiteheads Lemma

* comments in Whiteheads lemma file

* delete-trailing-whitespace

* moved lemmas, removed duplicates

Cubical/Foundations/Equiv/Properties.agda

@@ -253,3 +253,8 @@ isEquiv[equivFunA≃B∘f]→isEquiv[f] f (g , gIsEquiv) g∘fIsEquiv  =
 
       w' : isEquiv (equivFun (invEquiv (_ , g∘fIsEquiv)) ∘ g)
       w' = snd (compEquiv (_ , gIsEquiv) (invEquiv (_ , g∘fIsEquiv)))
+
+isPointedTarget→isEquiv→isEquiv : {A B : Type ℓ} (f : A → B)
+    → (B → isEquiv f) → isEquiv f
+equiv-proof (isPointedTarget→isEquiv→isEquiv f hf) =
+  λ y → equiv-proof (hf y) y

Cubical/Foundations/Pointed/Properties.agda

@@ -234,3 +234,13 @@ Iso.fun (pointedSecIso Q) F = (λ x → F (fst x) .fst (snd x)) , (λ x → F x
 Iso.inv (pointedSecIso Q) F a = (fst F ∘ (a ,_)) , snd F a
 Iso.rightInv (pointedSecIso Q) F = refl
 Iso.leftInv (pointedSecIso Q) F = refl
+
+compPathrEquiv∙ : {A : Type ℓ} {a b c : A} {q : a ≡ b} (p : b ≡ c)
+    → ((a ≡ b) , q) ≃∙ ((a ≡ c) , q ∙ p)
+fst (compPathrEquiv∙ p) = compPathrEquiv p
+snd (compPathrEquiv∙ p) = refl
+
+compPathlEquiv∙ : {A : Type ℓ} {a b c : A} {q : b ≡ c} (p : a ≡ b)
+    → ((b ≡ c) , q) ≃∙ ((a ≡ c) , p ∙ q)
+fst (compPathlEquiv∙ p) = compPathlEquiv p
+snd (compPathlEquiv∙ p) = refl

Cubical/HITs/SetTruncation/Properties.agda

@@ -333,3 +333,8 @@ Iso.fun (PathIdTrunc₀Iso {b = b}) p =
 Iso.inv PathIdTrunc₀Iso = pRec (squash₂ _ _) (cong ∣_∣₂)
 Iso.rightInv PathIdTrunc₀Iso _ = squash₁ _ _
 Iso.leftInv PathIdTrunc₀Iso _ = squash₂ _ _ _ _
+
+mapFunctorial : {A B C : Type ℓ} (f : A → B) (g : B → C)
+  → map g ∘ map f ≡ map (g ∘ f)
+mapFunctorial f g =
+  funExt (elim (λ x → isSetPathImplicit) λ a → refl)