`{Univalence} n {A B : pType} (f : A ->* B) : loops ([image n.+1 f, factor1 (image n.+1 f) (point A)]) <~> image n (fmap loops f). Proof. set (C := [image n.+1 f, factor1 (image n.+1 f) (point A)]). pose (g := Build_pMap A C (factor1 (image n.+1 f)) 1). pose (h := Build_pMap C B (factor2 (image n.+1 f)) (point_eq f)). transparent assert (I : (Factorization (@IsConnMap n) (@MapIn n) (fmap loops f))). { refine (@Build_Factorization (@IsConnMap n) (@MapIn n) (loops A) (loops B) (fmap loops f) (loops C) (fmap loops g) (fmap loops h) _ _ _). intros x; symmetry. refine (_ @ fmap_comp loops g h x). simpl. abstract (rewrite !concat_1p; reflexivity). } exact (path_intermediate (path_factor (O_factsys n) (fmap loops f) I (image n (fmap loops f)))). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Factorization Truncations.Core Truncations.Connectedness HProp. Require Import Pointed.Core Pointed.pEquiv. Require Import WildCat. Require Import Spaces.Nat.Core.