Coq 8.4 has module-local inductive types; the idea is that you can't see why the underlying type can't work, because you're not allowed to do destructuring on the local inductive. This has the nifty side-effect (not "computational effects") that you can define (obstructed) functions that "compute" the way we want, but that have meaningful obstru…

Cofiber.v

Require Import HoTT.

Local Open Scope path_scope.
Local Open Scope equiv_scope.

Module Export Cofiber.

  Local Inductive cofiber {A B : Type} (f : A -> B) : Type :=
    | apex : cofiber f
    | ground : B -> cofiber f.

  Axiom ascent : forall { A B } (f : A -> B) ( a : A ) , apex f = ground f (f a).

  Definition cofiber_rect { A B } (f : A -> B) (P : cofiber f -> Type)
    (Hapx : P (apex _)) (Hgrnd : forall b, P (ground f b)) (Hasc : forall a, ascent f a # Hapx = Hgrnd (f a))
  : forall x, P x :=
  fun x => ( match x return ( _ -> P x ) with
    | apex => (fun _ => Hapx) | ground b => (fun _ => Hgrnd b) end ) Hasc.

  Axiom cofiber_comp_ascent : forall { A B } (f : A -> B) (P : cofiber f -> Type) 
    (Hapx : P (apex _)) (Hgrnd : forall b, P (ground f b)) (Hasc : forall a, ascent f a # Hapx = Hgrnd (f a)),
    forall a, apD (cofiber_rect f P Hapx Hgrnd Hasc) (ascent f a) = Hasc a.

  Record cofiber_section_data { A B } { f : A -> B } (P : cofiber f -> Type) :=
  { H_apx : P (apex f) ;
    H_grn : forall b, P (ground f b);
    H_asc : forall a, ascent f a # H_apx = H_grn (f a)
  }.

  Definition cofiber_sectn_sd { A B } { f : A -> B } (P : cofiber f -> Type) :
    (forall x, P x) -> cofiber_section_data P.
  Proof.
    intro sn.
    exists (sn (apex _)) (fun b => sn (ground f b)).
    intro.
    apply apD.
  Defined.

End Cofiber.

Lemma cofiber_sectn_equiv `{Funext} { A B } { f : A -> B } (P : cofiber f -> Type) :
   (forall c, P c) <~> (cofiber_section_data P).
Proof.
  apply equiv_adjointify with
   (cofiber_section_sd P)
   (fun C : cofiber_section_data P => cofiber_rect f P (H_apx _ C) (H_grn _ C) (H_asc _ C)).
 
(* identity at cofiber_section_data; easy *)
  intro.
  destruct x as [ Hapx Hgrn Hasc ].
  simpl.
  unfold cofiber_rect. unfold cofiber_sectn_sd.
  refine ( ap (Build_cofiber_section_data _ _ _ P Hapx Hgrn) _ ).
  apply path_forall. intro.
  apply cofiber_comp_ascent.

(* identity at forall ; a little trickier *)
  intro.
  apply path_forall.
  unfold cofiber_sectn_sd. simpl.

  (* we can't do case matching; but we *can* use the protocol implemented! *)
  unfold "==". (* because otherwise coq can't see the "forall c : cofiber f" *)
  apply cofiber_rect with (Hapx := 1) (Hgrnd := (fun b => 1)).
  intro.
  refine (transport_paths_FlFr_D _ _ @ _). simpl.
  rewrite @concat_p1.
  apply moveR_Vp.
  rewrite @concat_p1.
  apply symmetry.
  refine (cofiber_comp_ascent f P _ (fun b => x (ground f b)) (fun a' => apD x (ascent f a')) a).

Defined.