Pi types can be homogenous

pi_homogenous.v

Require Import HoTT.HoTT.
Require Import HoTT.hit.minus1Trunc HoTT.hit.Truncations.

Generalizable All Variables.
Set Implicit Arguments.

Class IsHomogenous X (x : X) := is_homogenous : forall y, existT idmap X y = existT idmap X x.

Lemma path_forall_type `{Funext, Univalence} X (Y Y' : X -> Type)
: Y == Y' -> (forall x, Y x) = (forall x, Y' x).
Proof.
  intro H'.
  refine (@path_universe
            _ _ _
            (fun f x => transport idmap (H' x) (f x))
            (isequiv_adjointify
               (fun f x => transport idmap (H' x) (f x))
               (fun f x => transport idmap (inverse (H' x)) (f x))
               _
               _));
    intro; apply path_forall; intro;
    rewrite <- transport_pp, ?concat_pV, ?concat_Vp; reflexivity.
Defined.

Instance pi_homogenous `{Univalence, Funext} X (P : X -> Type) (f : forall x, P x)
         `{H' : forall x, @IsHomogenous (P x) (f x)}
: @IsHomogenous (forall x, P x) f.
Proof.
  intro y.
  unfold IsHomogenous in H'.
  apply path_sigma_uncurried; simpl.
  exists (path_forall_type (fun x => ap projT1 (H' x (y x)))).
  unfold path_forall_type.
  simpl.
  rewrite transport_path_universe.
  apply path_forall; intro.
  etransitivity;
    [ | apply (fun x => apD (@pr2 Type idmap) (H' x (y x))) ].
  simpl.
  etransitivity;
    [ symmetry;
      refine (@transport_compose _ _ _ _ idmap pr1 (H' x (y x)) (y x))
    | ].
  reflexivity.
Defined.