{A B : Type} (f : A -> B) `{IsConnMap O _ _ f} (P : B -> Type) `{forall b:B, In O (P b)} (d : forall a:A, P (f a)) : forall a:A, conn_map_elim f P d (f a) = d a. Proof. intros a. unfold conn_map_elim. set (fibermap := (fun a0p : hfiber f (f a) => let (a0, p) := a0p in transport P p (d a0))). destruct (isconnected_elim O (P (f a)) fibermap) as [x e]. change (d a) with (fibermap (a;1)). apply inverse, e. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.