Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.
Require Import TruncType.
Require Import ReflectiveSubuniverse.
Require Import Colimits.Pushout Truncations.Core HIT.SetCone.

Local Open Scope path_scope.

Section AssumingUA.
Context `{ua:Univalence}.

(** We will now prove that for sets, epis and surjections are equivalent.*)
Definition isepi {X Y} `(f:X->Y) := forall Z: HSet,
  forall g h: Y -> Z, g o f = h o f -> g = h.

Definition isepi_funext {X Y : Type} (f : X -> Y)
  := forall Z : HSet, forall g0 g1 : Y -> Z, g0 o f == g1 o f -> g0 == g1.

Definition isepi' {X Y} `(f : X -> Y) :=
  forall (Z : HSet) (g : Y -> Z), Contr { h : Y -> Z | g o f = h o f }.

Lemma equiv_isepi_isepi' {X Y} f : @isepi X Y f <~> @isepi' X Y f.
ua: Univalence
X, Y: Type
f: X -> Y
isepi f <~> isepi' f
Proof.
ua: Univalence
X, Y: Type
f: X -> Y
isepi f <~> isepi' f
  unfold isepi, isepi'.
ua: Univalence
X, Y: Type
f: X -> Y
(forall (Z : HSet) (g h : Y -> Z),
 (fun x : X => g (f x)) = (fun x : X => h (f x)) ->
 g = h) <~>
(forall (Z : HSet) (g : Y -> Z),
 Contr
   {h : Y -> Z &
   (fun x : X => g (f x)) = (fun x : X => h (f x))})
  apply (@equiv_functor_forall' _ _ _ _ _ (equiv_idmap _)); intro Z.
ua: Univalence
X, Y: Type
f: X -> Y
Z: HSet
(forall g h : Y -> 1%equiv Z,
 (fun x : X => g (f x)) = (fun x : X => h (f x)) ->
 g = h) <~>
(forall g : Y -> Z,
 Contr
   {h : Y -> Z &
   (fun x : X => g (f x)) = (fun x : X => h (f x))})
  apply (@equiv_functor_forall' _ _ _ _ _ (equiv_idmap _)); intro g.
ua: Univalence
X, Y: Type
f: X -> Y
Z: HSet
g: Y -> 1%equiv Z
(forall h : Y -> 1%equiv Z,
 (fun x : X => 1%equiv g (f x)) =
 (fun x : X => h (f x)) -> 1%equiv g = h) <~>
Contr
  {h : Y -> Z &
  (fun x : X => g (f x)) = (fun x : X => h (f x))}
  unfold equiv_idmap; simpl.
ua: Univalence
X, Y: Type
f: X -> Y
Z: HSet
g: Y -> 1%equiv Z
(forall h : Y -> Z,
 (fun x : X => g (f x)) = (fun x : X => h (f x)) ->
 g = h) <~>
Contr
  {h : Y -> Z &
  (fun x : X => g (f x)) = (fun x : X => h (f x))}
  refine (transitivity (@equiv_sig_ind _ (fun h : Y -> Z => g o f = h o f) (fun h => g = h.1)) _).
ua: Univalence
X, Y: Type
f: X -> Y
Z: HSet
g: Y -> 1%equiv Z
(forall
 xy : {h : Y -> Z &
      (fun x : X => g (f x)) = (fun x : X => h (f x))},
 g = xy.1) <~>
Contr
  {h : Y -> Z &
  (fun x : X => g (f x)) = (fun x : X => h (f x))}
  (** TODO(JasonGross): Can we do this entirely by chaining equivalences? *)
  apply equiv_iff_hprop.
ua: Univalence
X, Y: Type
f: X -> Y
Z: HSet
g: Y -> 1%equiv Z
(forall
 xy : {h : Y -> Z &
      (fun x : X => g (f x)) = (fun x : X => h (f x))},
 g = xy.1) ->
Contr
  {h : Y -> Z &
  (fun x : X => g (f x)) = (fun x : X => h (f x))}
ua: Univalence
X, Y: Type
f: X -> Y
Z: HSet
g: Y -> 1%equiv Z
Contr
  {h : Y -> Z &
  (fun x : X => g (f x)) = (fun x : X => h (f x))} ->
forall
xy : {h : Y -> Z &
     (fun x : X => g (f x)) = (fun x : X => h (f x))},
g = xy.1
  {
ua: Univalence
X, Y: Type
f: X -> Y
Z: HSet
g: Y -> 1%equiv Z
(forall
 xy : {h : Y -> Z &
      (fun x : X => g (f x)) = (fun x : X => h (f x))},
 g = xy.1) ->
Contr
  {h : Y -> Z &
  (fun x : X => g (f x)) = (fun x : X => h (f x))} intro hepi.
ua: Univalence
X, Y: Type
f: X -> Y
Z: HSet
g: Y -> 1%equiv Z
hepi: forall
xy : {h : Y -> Z &
     (fun x : X => g (f x)) =
     (fun x : X => h (f x))}, 
g = xy.1
Contr
  {h : Y -> Z &
  (fun x : X => g (f x)) = (fun x : X => h (f x))}
    nrapply (Build_Contr _ (g; idpath)).
ua: Univalence
X, Y: Type
f: X -> Y
Z: HSet
g: Y -> 1%equiv Z
hepi: forall
xy : {h : Y -> Z &
     (fun x : X => g (f x)) =
     (fun x : X => h (f x))}, 
g = xy.1
forall
y : {h : Y -> Z &
    (fun x : X => g (f x)) = (fun x : X => h (f x))},
(g; 1) = y
    intro xy; specialize (hepi xy).
ua: Univalence
X, Y: Type
f: X -> Y
Z: HSet
g: Y -> 1%equiv Z
xy: {h : Y -> Z &
(fun x : X => g (f x)) = (fun x : X => h (f x))}
hepi: g = xy.1
(g; 1) = xy
    apply path_sigma_uncurried.
ua: Univalence
X, Y: Type
f: X -> Y
Z: HSet
g: Y -> 1%equiv Z
xy: {h : Y -> Z &
(fun x : X => g (f x)) = (fun x : X => h (f x))}
hepi: g = xy.1
{p : (g; 1).1 = xy.1 &
transport
  (fun h : Y -> Z =>
   (fun x : X => g (f x)) = (fun x : X => h (f x))) p
  (g; 1).2 = xy.2}
    exists hepi.
ua: Univalence
X, Y: Type
f: X -> Y
Z: HSet
g: Y -> 1%equiv Z
xy: {h : Y -> Z &
(fun x : X => g (f x)) = (fun x : X => h (f x))}
hepi: g = xy.1
transport
  (fun h : Y -> Z =>
   (fun x : X => g (f x)) = (fun x : X => h (f x)))
  hepi (g; 1).2 = xy.2
    apply path_ishprop. }
ua: Univalence
X, Y: Type
f: X -> Y
Z: HSet
g: Y -> 1%equiv Z
Contr
  {h : Y -> Z &
  (fun x : X => g (f x)) = (fun x : X => h (f x))} ->
forall
xy : {h : Y -> Z &
     (fun x : X => g (f x)) = (fun x : X => h (f x))},
g = xy.1
  {
ua: Univalence
X, Y: Type
f: X -> Y
Z: HSet
g: Y -> 1%equiv Z
Contr
  {h : Y -> Z &
  (fun x : X => g (f x)) = (fun x : X => h (f x))} ->
forall
xy : {h : Y -> Z &
     (fun x : X => g (f x)) = (fun x : X => h (f x))},
g = xy.1 intros hepi xy.
ua: Univalence
X, Y: Type
f: X -> Y
Z: HSet
g: Y -> 1%equiv Z
hepi: Contr
  {h : Y -> Z &
  (fun x : X => g (f x)) =
  (fun x : X => h (f x))}
xy: {h : Y -> Z &
(fun x : X => g (f x)) = (fun x : X => h (f x))}
g = xy.1
    exact (ap pr1 ((contr (g; 1))^ @ contr xy)). }
Defined.

Definition equiv_isepi_isepi_funext {X Y : Type} (f : X -> Y)
  : isepi f <~> isepi_funext f.
ua: Univalence
X, Y: Type
f: X -> Y
isepi f <~> isepi_funext f
Proof.
ua: Univalence
X, Y: Type
f: X -> Y
isepi f <~> isepi_funext f
  apply equiv_iff_hprop.
ua: Univalence
X, Y: Type
f: X -> Y
isepi f -> isepi_funext f
ua: Univalence
X, Y: Type
f: X -> Y
isepi_funext f -> isepi f
  -
ua: Univalence
X, Y: Type
f: X -> Y
isepi f -> isepi_funext f intros e ? g0 g1 h.
ua: Univalence
X, Y: Type
f: X -> Y
e: isepi f
Z: HSet
g0, g1: Y -> Z
h: (fun x : X => g0 (f x)) == (fun x : X => g1 (f x))
g0 == g1
    apply equiv_path_arrow.
ua: Univalence
X, Y: Type
f: X -> Y
e: isepi f
Z: HSet
g0, g1: Y -> Z
h: (fun x : X => g0 (f x)) == (fun x : X => g1 (f x))
g0 = g1
    apply e.
ua: Univalence
X, Y: Type
f: X -> Y
e: isepi f
Z: HSet
g0, g1: Y -> Z
h: (fun x : X => g0 (f x)) == (fun x : X => g1 (f x))
(fun x : X => g0 (f x)) = (fun x : X => g1 (f x))
    by apply path_arrow.
  -
ua: Univalence
X, Y: Type
f: X -> Y
isepi_funext f -> isepi f intros e ? g0 g1 p.
ua: Univalence
X, Y: Type
f: X -> Y
e: isepi_funext f
Z: HSet
g0, g1: Y -> Z
p: (fun x : X => g0 (f x)) = (fun x : X => g1 (f x))
g0 = g1
    apply path_arrow.
ua: Univalence
X, Y: Type
f: X -> Y
e: isepi_funext f
Z: HSet
g0, g1: Y -> Z
p: (fun x : X => g0 (f x)) = (fun x : X => g1 (f x))
g0 == g1
    apply e.
ua: Univalence
X, Y: Type
f: X -> Y
e: isepi_funext f
Z: HSet
g0, g1: Y -> Z
p: (fun x : X => g0 (f x)) = (fun x : X => g1 (f x))
(fun x : X => g0 (f x)) == (fun x : X => g1 (f x))
    by apply equiv_path_arrow.
Defined.

Section cones.
  Lemma isepi'_contr_cone `{Funext} {A B : HSet} (f : A -> B) : isepi' f -> Contr (setcone f).
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
isepi' f -> Contr (setcone f)
  Proof.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
isepi' f -> Contr (setcone f)
    intros hepi.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
Contr (setcone f)
    apply (Build_Contr _ (setcone_point _)).
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
forall y : setcone f, setcone_point f = y
    pose (alpha1 := @pglue A B Unit f (const_tt _)).
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
forall y : setcone f, setcone_point f = y
    pose (tot:= { h : B -> setcone f & tr o push o inl o f = h o f }).
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
tot:= {h : B -> setcone f &
tr o push o inl o f = h o f}: Type
forall y : setcone f, setcone_point f = y
    transparent assert (l : tot).
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
tot:= {h : B -> setcone f &
tr o push o inl o f = h o f}: Type
tot
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
tot:= {h : B -> setcone f &
tr o push o inl o f = h o f}: Type
l:= ?Goal: tot
forall y : setcone f, setcone_point f = y
    {
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
tot:= {h : B -> setcone f &
tr o push o inl o f = h o f}: Type
tot simple refine (tr o _ o inl; _).
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
tot:= {h : B -> setcone f &
tr o push o inl o f = h o f}: Type
B + ?Goal0@{g0:=tr} -> Pushout f (const_tt A)
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
tot:= {h : B -> setcone f &
tr o push o inl o f = h o f}: Type
g0: Pushout f (const_tt A) ->
Trunc 0 (Pushout f (const_tt A))
Type
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
tot:= {h : B -> setcone f &
tr o push o inl o f = h o f}: Type
(fun h : B -> setcone f => tr o push o inl o f = h o f)
  (tr o ?f0 o inl)
      {
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
tot:= {h : B -> setcone f &
tr o push o inl o f = h o f}: Type
B + ?Goal0@{g0:=tr} -> Pushout f (const_tt A) refine push. }
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
tot:= {h : B -> setcone f &
tr o push o inl o f = h o f}: Type
(fun h : B -> setcone f => tr o push o inl o f = h o f)
  (tr o push o inl)
      {
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
tot:= {h : B -> setcone f &
tr o push o inl o f = h o f}: Type
(fun h : B -> setcone f => tr o push o inl o f = h o f)
  (tr o push o inl) refine idpath. } }
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
tot:= {h : B -> setcone f &
tr o push o inl o f = h o f}: Type
l:= (tr o push o inl; 1): tot
forall y : setcone f, setcone_point f = y
    pose (r := (@const B (setcone f) (setcone_point _); (ap (fun f => @tr 0 _ o f) (path_forall _ _ alpha1))) : tot).
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
tot:= {h : B -> setcone f &
tr o push o inl o f = h o f}: Type
l:= (tr o push o inl; 1): tot
r:= (const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) => tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) alpha1))
:
tot: tot
forall y : setcone f, setcone_point f = y
    subst tot.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
l:= (tr o push o inl; 1): {h : B -> setcone f & tr o push o inl o f = h o f}
r:= (const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) => tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) alpha1))
:
{h : B -> setcone f & tr o push o inl o f = h o f}: {h : B -> setcone f & tr o push o inl o f = h o f}
forall y : setcone f, setcone_point f = y
    assert (X : l = r).
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
l:= (tr o push o inl; 1): {h : B -> setcone f & tr o push o inl o f = h o f}
r:= (const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) => tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) alpha1))
:
{h : B -> setcone f & tr o push o inl o f = h o f}: {h : B -> setcone f & tr o push o inl o f = h o f}
l = r
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
l:= (tr o push o inl; 1): {h : B -> setcone f & tr o push o inl o f = h o f}
r:= (const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) => tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) alpha1))
:
{h : B -> setcone f & tr o push o inl o f = h o f}: {h : B -> setcone f & tr o push o inl o f = h o f}
X: l = r
forall y : setcone f, setcone_point f = y
      {
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
l:= (tr o push o inl; 1): {h : B -> setcone f & tr o push o inl o f = h o f}
r:= (const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) => tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) alpha1))
:
{h : B -> setcone f & tr o push o inl o f = h o f}: {h : B -> setcone f & tr o push o inl o f = h o f}
l = r let lem := constr:(fun X push' => hepi (Build_HSet (setcone f)) (tr o push' o @inl _ X)) in
        pose (lem _ push).
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
l:= (tr o push o inl; 1): {h : B -> setcone f & tr o push o inl o f = h o f}
r:= (const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) => tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) alpha1))
:
{h : B -> setcone f & tr o push o inl o f = h o f}: {h : B -> setcone f & tr o push o inl o f = h o f}
i:= (fun (X : Type)
   (push' : B + X -> Pushout f (const_tt A)) =>
 hepi (Build_HSet (setcone f)) (tr o push' o inl))
  Unit push: Contr
  {h : B -> Build_HSet (setcone f) &
  tr o push o inl o f = h o f}
l = r
        refine (path_contr l r). }
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
l:= (tr o push o inl; 1): {h : B -> setcone f & tr o push o inl o f = h o f}
r:= (const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) => tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) alpha1))
:
{h : B -> setcone f & tr o push o inl o f = h o f}: {h : B -> setcone f & tr o push o inl o f = h o f}
X: l = r
forall y : setcone f, setcone_point f = y
    subst l r.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) alpha1))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
forall y : setcone f, setcone_point f = y

    pose (I0 b := ap10 (X ..1) b).
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) alpha1))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0:= fun b : B => ap10 X ..1 b: forall b : B,
(tr o push o inl; 1).1 b =
(const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) =>
   tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) alpha1)).1
  b
forall y : setcone f, setcone_point f = y
    refine (Trunc_ind _ _).
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) alpha1))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0:= fun b : B => ap10 X ..1 b: forall b : B,
(tr o push o inl; 1).1 b =
(const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) =>
   tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) alpha1)).1
  b
forall a : Pushout f (const_tt A),
setcone_point f = tr a
    pose (fun a : B + Unit => (match a as a return setcone_point _ = tr (push a) with
                                 | inl a' => (I0 a')^
                                 | inr tt => idpath
                               end)) as I0f.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) alpha1))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0:= fun b : B => ap10 X ..1 b: forall b : B,
(tr o push o inl; 1).1 b =
(const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) =>
   tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) alpha1)).1
  b
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => (I0 a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
forall a : Pushout f (const_tt A),
setcone_point f = tr a
    refine (Pushout_ind _ (fun a' => I0f (inl a')) (fun u => (I0f (inr u))) _).
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) alpha1))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0:= fun b : B => ap10 X ..1 b: forall b : B,
(tr o push o inl; 1).1 b =
(const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) =>
   tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) alpha1)).1
  b
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => (I0 a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
forall a : A,
transport
  (fun w : Pushout f (const_tt A) =>
   setcone_point f = tr w) (pglue a) (I0f (inl (f a))) =
I0f (inr (const_tt A a))

    simpl.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
alpha1:= pglue: forall a : A,
pushl (f a) = pushr (const_tt A a)
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) alpha1))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0:= fun b : B => ap10 X ..1 b: forall b : B,
(tr o push o inl; 1).1 b =
(const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) =>
   tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) alpha1)).1
  b
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => (I0 a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
forall a : A,
transport
  (fun w : Pushout f (const_tt A) =>
   setcone_point f = tr w) (pglue a) (I0 (f a))^ = 1 subst alpha1.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0:= fun b : B => ap10 X ..1 b: forall b : B,
(tr o push o inl; 1).1 b =
(const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) =>
   tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) pglue)).1
  b
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => (I0 a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
forall a : A,
transport
  (fun w : Pushout f (const_tt A) =>
   setcone_point f = tr w) (pglue a) (I0 (f a))^ = 1 intros.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0:= fun b : B => ap10 X ..1 b: forall b : B,
(tr o push o inl; 1).1 b =
(const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) =>
   tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) pglue)).1
  b
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => (I0 a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
a: A
transport
  (fun w : Pushout f (const_tt A) =>
   setcone_point f = tr w) (pglue a) (I0 (f a))^ = 1
    unfold setcone_point.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0:= fun b : B => ap10 X ..1 b: forall b : B,
(tr o push o inl; 1).1 b =
(const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) =>
   tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) pglue)).1
  b
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => (I0 a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
a: A
transport
  (fun w : Pushout f (const_tt A) =>
   tr (push (inr tt)) = tr w) (pglue a) (I0 (f a))^ =
1
    subst I0.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => ((fun b : B => ap10 X ..1 b) a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
a: A
transport
  (fun w : Pushout f (const_tt A) =>
   tr (push (inr tt)) = tr w) (pglue a)
  ((fun b : B => ap10 X ..1 b) (f a))^ = 1 simpl.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => ((fun b : B => ap10 X ..1 b) a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
a: A
transport
  (fun w : Pushout f (const_tt A) =>
   tr (push (inr tt)) = tr w) (pglue a)
  (ap10 X ..1 (f a))^ = 1
    pose (X..2) as p.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => ((fun b : B => ap10 X ..1 b) a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
a: A
p:= X ..2: transport
  (fun h : B -> setcone f =>
   tr o push o inl o f = h o f) 
  X ..1 (tr o push o inl; 1).2 =
(const (setcone_point f);
ap
  (fun f0 : A -> Pushout f (const_tt A) => tr o f0)
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) pglue)).2
transport
  (fun w : Pushout f (const_tt A) =>
   tr (push (inr tt)) = tr w) (pglue a)
  (ap10 X ..1 (f a))^ = 1 simpl in p.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => ((fun b : B => ap10 X ..1 b) a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
a: A
p:= X ..2: transport
  (fun h : B -> setcone f =>
   (fun x : A => tr (push (inl (f x)))) =
   (fun x : A => h (f x))) 
  X ..1 1 =
ap
  (fun (f0 : A -> Pushout f (const_tt A)) (x : A)
   => tr (f0 x))
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) pglue)
transport
  (fun w : Pushout f (const_tt A) =>
   tr (push (inr tt)) = tr w) (pglue a)
  (ap10 X ..1 (f a))^ = 1
    rewrite (transport_precompose f _ _ X..1) in p.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => ((fun b : B => ap10 X ..1 b) a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
a: A
p: ap (fun (h : B -> setcone f) (x : A) => h (f x))
  X ..1 =
ap
  (fun (f0 : A -> Pushout f (const_tt A)) (x : A)
   => tr (f0 x))
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) pglue)
transport
  (fun w : Pushout f (const_tt A) =>
   tr (push (inr tt)) = tr w) (pglue a)
  (ap10 X ..1 (f a))^ = 1
    assert (H':=concat (ap (fun x => ap10 x a) p) (ap10_ap_postcompose tr (path_arrow (pushl o f) (pushr o const_tt _) pglue) _)).
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => ((fun b : B => ap10 X ..1 b) a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
a: A
p: ap (fun (h : B -> setcone f) (x : A) => h (f x))
  X ..1 =
ap
  (fun (f0 : A -> Pushout f (const_tt A)) (x : A)
   => tr (f0 x))
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) pglue)
H': ap10
  (ap
     (fun (h : B -> setcone f) (x : A) => h (f x))
     X ..1) a =
ap tr
  (ap10
     (path_arrow (pushl o f) 
        (pushr o const_tt A) pglue) a)
transport
  (fun w : Pushout f (const_tt A) =>
   tr (push (inr tt)) = tr w) (pglue a)
  (ap10 X ..1 (f a))^ = 1
    rewrite ap10_path_arrow in H'.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => ((fun b : B => ap10 X ..1 b) a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
a: A
p: ap (fun (h : B -> setcone f) (x : A) => h (f x))
  X ..1 =
ap
  (fun (f0 : A -> Pushout f (const_tt A)) (x : A)
   => tr (f0 x))
  (path_forall (fun a : A => pushl (f a))
     (fun a : A => pushr (const_tt A a)) pglue)
H': ap10
  (ap
     (fun (h : B -> setcone f) (x : A) => h (f x))
     X ..1) a = ap tr (pglue a)
transport
  (fun w : Pushout f (const_tt A) =>
   tr (push (inr tt)) = tr w) (pglue a)
  (ap10 X ..1 (f a))^ = 1
    clear p.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => ((fun b : B => ap10 X ..1 b) a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
a: A
H': ap10
  (ap
     (fun (h : B -> setcone f) (x : A) => h (f x))
     X ..1) a = ap tr (pglue a)
transport
  (fun w : Pushout f (const_tt A) =>
   tr (push (inr tt)) = tr w) (pglue a)
  (ap10 X ..1 (f a))^ = 1
    (** Apparently [pose; clearbody] is only ~.8 seconds, while [pose proof] is ~4 seconds? *)
    pose (concat (ap10_ap_precompose f (X ..1) a)^ H') as p.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => ((fun b : B => ap10 X ..1 b) a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
a: A
H': ap10
  (ap
     (fun (h : B -> setcone f) (x : A) => h (f x))
     X ..1) a = ap tr (pglue a)
p:= (ap10_ap_precompose f X ..1 a)^ @ H': ap10 X ..1 (f a) = ap tr (pglue a)
transport
  (fun w : Pushout f (const_tt A) =>
   tr (push (inr tt)) = tr w) (pglue a)
  (ap10 X ..1 (f a))^ = 1
    clearbody p.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => ((fun b : B => ap10 X ..1 b) a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
a: A
H': ap10
  (ap
     (fun (h : B -> setcone f) (x : A) => h (f x))
     X ..1) a = ap tr (pglue a)
p: ap10 X ..1 (f a) = ap tr (pglue a)
transport
  (fun w : Pushout f (const_tt A) =>
   tr (push (inr tt)) = tr w) (pglue a)
  (ap10 X ..1 (f a))^ = 1
    simpl in p.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => ((fun b : B => ap10 X ..1 b) a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
a: A
H': ap10
  (ap
     (fun (h : B -> setcone f) (x : A) => h (f x))
     X ..1) a = ap tr (pglue a)
p: ap10 X ..1 (f a) = ap tr (pglue a)
transport
  (fun w : Pushout f (const_tt A) =>
   tr (push (inr tt)) = tr w) (pglue a)
  (ap10 X ..1 (f a))^ = 1
    rewrite p.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => ((fun b : B => ap10 X ..1 b) a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
a: A
H': ap10
  (ap
     (fun (h : B -> setcone f) (x : A) => h (f x))
     X ..1) a = ap tr (pglue a)
p: ap10 X ..1 (f a) = ap tr (pglue a)
transport
  (fun w : Pushout f (const_tt A) =>
   tr (push (inr tt)) = tr w) (pglue a)
  (ap tr (pglue a))^ = 1
    rewrite transport_paths_Fr.
ua: Univalence
H: Funext
A, B: HSet
f: A -> B
hepi: isepi' f
X: (tr o push o inl; 1) =
((const (setcone_point f);
 ap
   (fun f0 : A -> Pushout f (const_tt A) =>
    tr o f0)
   (path_forall (fun a : A => pushl (f a))
      (fun a : A => pushr (const_tt A a)) pglue))
 :
 {h : B -> setcone f &
 tr o push o inl o f = h o f})
I0f:= fun a : B + Unit =>
match
  a as a0 return (setcone_point f = tr (push a0))
with
| inl a' => ((fun b : B => ap10 X ..1 b) a')^
| inr u =>
    match
      u as u0
      return
        (setcone_point f = tr (push (inr u0)))
    with
    | tt => 1
    end
end: forall a : B + Unit,
setcone_point f = tr (push a)
a: A
H': ap10
  (ap
     (fun (h : B -> setcone f) (x : A) => h (f x))
     X ..1) a = ap tr (pglue a)
p: ap10 X ..1 (f a) = ap tr (pglue a)
(ap tr (pglue a))^ @ ap tr (pglue a) = 1
    apply concat_Vp.
  Qed.
End cones.

Lemma issurj_isepi {X Y} (f:X->Y): IsSurjection f -> isepi f.
ua: Univalence
X, Y: Type
f: X -> Y
IsConnMap (Tr (-1)) f -> isepi f
Proof.
ua: Univalence
X, Y: Type
f: X -> Y
IsConnMap (Tr (-1)) f -> isepi f
intros sur ? ? ? ep.
ua: Univalence
X, Y: Type
f: X -> Y
sur: IsConnMap (Tr (-1)) f
Z: HSet
g, h: Y -> Z
ep: (fun x : X => g (f x)) = (fun x : X => h (f x))
g = h apply path_forall.
ua: Univalence
X, Y: Type
f: X -> Y
sur: IsConnMap (Tr (-1)) f
Z: HSet
g, h: Y -> Z
ep: (fun x : X => g (f x)) = (fun x : X => h (f x))
g == h intro y.
ua: Univalence
X, Y: Type
f: X -> Y
sur: IsConnMap (Tr (-1)) f
Z: HSet
g, h: Y -> Z
ep: (fun x : X => g (f x)) = (fun x : X => h (f x))
y: Y
g y = h y
specialize (sur y).
ua: Univalence
X, Y: Type
f: X -> Y
y: Y
sur: IsConnected (Tr (-1)) (hfiber f y)
Z: HSet
g, h: Y -> Z
ep: (fun x : X => g (f x)) = (fun x : X => h (f x))
g y = h y pose (center (merely (hfiber f y))).
ua: Univalence
X, Y: Type
f: X -> Y
y: Y
sur: IsConnected (Tr (-1)) (hfiber f y)
Z: HSet
g, h: Y -> Z
ep: (fun x : X => g (f x)) = (fun x : X => h (f x))
t:= center (merely (hfiber f y)): merely (hfiber f y)
g y = h y
apply (Trunc_rec (n:=-1) (A:=(sig (fun x : X => f x = y))));
  try assumption.
ua: Univalence
X, Y: Type
f: X -> Y
y: Y
sur: IsConnected (Tr (-1)) (hfiber f y)
Z: HSet
g, h: Y -> Z
ep: (fun x : X => g (f x)) = (fun x : X => h (f x))
t:= center (merely (hfiber f y)): merely (hfiber f y)
{x : X & f x = y} -> g y = h y
intros [x p].
ua: Univalence
X, Y: Type
f: X -> Y
y: Y
sur: IsConnected (Tr (-1)) (hfiber f y)
Z: HSet
g, h: Y -> Z
ep: (fun x : X => g (f x)) = (fun x : X => h (f x))
t:= center (merely (hfiber f y)): merely (hfiber f y)
x: X
p: f x = y
g y = h y set (p0:=apD10 ep x).
ua: Univalence
X, Y: Type
f: X -> Y
y: Y
sur: IsConnected (Tr (-1)) (hfiber f y)
Z: HSet
g, h: Y -> Z
ep: (fun x : X => g (f x)) = (fun x : X => h (f x))
t:= center (merely (hfiber f y)): merely (hfiber f y)
x: X
p: f x = y
p0:= apD10 ep x: (fun x : X => g (f x)) x =
(fun x : X => h (f x)) x
g y = h y
transitivity (g (f x)).
ua: Univalence
X, Y: Type
f: X -> Y
y: Y
sur: IsConnected (Tr (-1)) (hfiber f y)
Z: HSet
g, h: Y -> Z
ep: (fun x : X => g (f x)) = (fun x : X => h (f x))
t:= center (merely (hfiber f y)): merely (hfiber f y)
x: X
p: f x = y
p0:= apD10 ep x: (fun x : X => g (f x)) x =
(fun x : X => h (f x)) x
g y = g (f x)
ua: Univalence
X, Y: Type
f: X -> Y
y: Y
sur: IsConnected (Tr (-1)) (hfiber f y)
Z: HSet
g, h: Y -> Z
ep: (fun x : X => g (f x)) = (fun x : X => h (f x))
t:= center (merely (hfiber f y)): merely (hfiber f y)
x: X
p: f x = y
p0:= apD10 ep x: (fun x : X => g (f x)) x =
(fun x : X => h (f x)) x
g (f x) = h y
-
ua: Univalence
X, Y: Type
f: X -> Y
y: Y
sur: IsConnected (Tr (-1)) (hfiber f y)
Z: HSet
g, h: Y -> Z
ep: (fun x : X => g (f x)) = (fun x : X => h (f x))
t:= center (merely (hfiber f y)): merely (hfiber f y)
x: X
p: f x = y
p0:= apD10 ep x: (fun x : X => g (f x)) x =
(fun x : X => h (f x)) x
g y = g (f x) by apply ap.
-
ua: Univalence
X, Y: Type
f: X -> Y
y: Y
sur: IsConnected (Tr (-1)) (hfiber f y)
Z: HSet
g, h: Y -> Z
ep: (fun x : X => g (f x)) = (fun x : X => h (f x))
t:= center (merely (hfiber f y)): merely (hfiber f y)
x: X
p: f x = y
p0:= apD10 ep x: (fun x : X => g (f x)) x =
(fun x : X => h (f x)) x
g (f x) = h y transitivity (h (f x));auto with path_hints.
ua: Univalence
X, Y: Type
f: X -> Y
y: Y
sur: IsConnected (Tr (-1)) (hfiber f y)
Z: HSet
g, h: Y -> Z
ep: (fun x : X => g (f x)) = (fun x : X => h (f x))
t:= center (merely (hfiber f y)): merely (hfiber f y)
x: X
p: f x = y
p0:= apD10 ep x: (fun x : X => g (f x)) x =
(fun x : X => h (f x)) x
h (f x) = h y by apply ap.
Qed.

Corollary issurj_isepi_funext {X Y} (f:X->Y) : IsSurjection f -> isepi_funext f.
ua: Univalence
X, Y: Type
f: X -> Y
IsConnMap (Tr (-1)) f -> isepi_funext f
Proof.
ua: Univalence
X, Y: Type
f: X -> Y
IsConnMap (Tr (-1)) f -> isepi_funext f
  intro s.
ua: Univalence
X, Y: Type
f: X -> Y
s: IsConnMap (Tr (-1)) f
isepi_funext f
  apply equiv_isepi_isepi_funext.
ua: Univalence
X, Y: Type
f: X -> Y
s: IsConnMap (Tr (-1)) f
isepi f
  by apply issurj_isepi.
Defined.

(** Old-style proof using polymorphic Omega. Needs resizing for the isepi proof to live in the
 same universe as X and Y (the Z quantifier is instantiated with an HSet at a level higher)
<<
Lemma isepi_issurj {X Y} (f:X->Y): isepi f -> issurj f.
Proof.
  intros epif y.
  set (g :=fun _:Y => Unit_hp).
  set (h:=(fun y:Y => (hp (hexists (fun _ : Unit => {x:X & y = (f x)})) _ ))).
  assert (X1: g o f = h o f ).
  - apply path_forall. intro x. apply path_equiv_biimp_rec;[|done].
    intros _ . apply min1. exists tt. by (exists x).
  - specialize (epif _ g h).
    specialize (epif X1). clear X1.
    set (p:=apD10 epif y).
    apply (@minus1Trunc_map (sig (fun _ : Unit => sig (fun x : X => y = f x)))).
    + intros [ _ [x eq]].
      exists x.
        by symmetry.
    + apply (transport hproptype p tt).
Defined.
>>
*)

Section isepi_issurj.
  Context {X Y : HSet} (f : X -> Y) (Hisepi : isepi f).
  Definition epif := equiv_isepi_isepi' _ Hisepi.
  Definition fam (c : setcone f) : HProp.
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
c: setcone f
HProp
  Proof.
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
c: setcone f
HProp
    pose (fib y := hexists (fun x : X => f x = y)).
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
c: setcone f
fib:= fun y : Y => hexists (fun x : X => f x = y): Y -> HProp
HProp
    apply (fun f => @Trunc_rec _ _ HProp _ f c).
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
c: setcone f
fib:= fun y : Y => hexists (fun x : X => f x = y): Y -> HProp
Pushout f (const_tt X) -> HProp
    refine (Pushout_rec HProp fib (fun _ => Unit_hp) (fun x => _)).
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
c: setcone f
fib:= fun y : Y => hexists (fun x : X => f x = y): Y -> HProp
x: X
fib (f x) = Unit_hp
    (** Prove that the truncated sigma is equivalent to Unit *)
    pose (contr_inhabited_hprop (fib (f x)) (tr (x; idpath))) as i.
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
c: setcone f
fib:= fun y : Y => hexists (fun x : X => f x = y): Y -> HProp
x: X
i:= contr_inhabited_hprop (fib (f x)) (tr (x; 1)): Contr (fib (f x))
fib (f x) = Unit_hp
    apply path_hprop.
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
c: setcone f
fib:= fun y : Y => hexists (fun x : X => f x = y): Y -> HProp
x: X
i:= contr_inhabited_hprop (fib (f x)) (tr (x; 1)): Contr (fib (f x))
fib (f x) <~> Unit_hp simpl.
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
c: setcone f
fib:= fun y : Y => hexists (fun x : X => f x = y): Y -> HProp
x: X
i:= contr_inhabited_hprop (fib (f x)) (tr (x; 1)): Contr (fib (f x))
Tr (-1) {x0 : X & f x0 = f x} <~> Unit simpl in i.
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
c: setcone f
fib:= fun y : Y => hexists (fun x : X => f x = y): Y -> HProp
x: X
i:= contr_inhabited_hprop
  (Tr (-1) {x0 : X & f x0 = f x}) 
  (tr (x; 1)): Contr (Tr (-1) {x0 : X & f x0 = f x})
Tr (-1) {x0 : X & f x0 = f x} <~> Unit
    apply (equiv_contr_unit).
  Defined.

  Lemma isepi_issurj : IsSurjection f.
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
IsConnMap (Tr (-1)) f
  Proof.
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
IsConnMap (Tr (-1)) f
    intros y.
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
y: Y
IsConnected (Tr (-1)) (hfiber f y)
    pose (i := isepi'_contr_cone _ epif).
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
y: Y
i:= isepi'_contr_cone f epif: Contr (setcone f)
IsConnected (Tr (-1)) (hfiber f y)

    assert (X0 : forall x : setcone f, fam x = fam (setcone_point f)).
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
y: Y
i:= isepi'_contr_cone f epif: Contr (setcone f)
forall x : setcone f, fam x = fam (setcone_point f)
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
y: Y
i:= isepi'_contr_cone f epif: Contr (setcone f)
X0: forall x : setcone f,
fam x = fam (setcone_point f)
IsConnected (Tr (-1)) (hfiber f y)
    {
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
y: Y
i:= isepi'_contr_cone f epif: Contr (setcone f)
forall x : setcone f, fam x = fam (setcone_point f) intros.
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
y: Y
i:= isepi'_contr_cone f epif: Contr (setcone f)
x: setcone f
fam x = fam (setcone_point f) apply contr_dom_equiv.
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
y: Y
i:= isepi'_contr_cone f epif: Contr (setcone f)
x: setcone f
Contr (setcone f) apply i. }
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
y: Y
i:= isepi'_contr_cone f epif: Contr (setcone f)
X0: forall x : setcone f,
fam x = fam (setcone_point f)
IsConnected (Tr (-1)) (hfiber f y)
    specialize (X0 (tr (push (inl y)))).
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
y: Y
i:= isepi'_contr_cone f epif: Contr (setcone f)
X0: fam (tr (push (inl y))) = fam (setcone_point f)
IsConnected (Tr (-1)) (hfiber f y) simpl in X0.
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
y: Y
i:= isepi'_contr_cone f epif: Contr (setcone f)
X0: hexists (fun x : X => f x = y) = Unit_hp
IsConnected (Tr (-1)) (hfiber f y)
    unfold IsConnected.
ua: Univalence
X, Y: HSet
f: X -> Y
Hisepi: isepi f
y: Y
i:= isepi'_contr_cone f epif: Contr (setcone f)
X0: hexists (fun x : X => f x = y) = Unit_hp
Contr (Tr (-1) (hfiber f y))
    refine (transport (fun A => Contr A) (ap trunctype_type X0)^ _); exact _.
  Defined.
End isepi_issurj.

Lemma isepi_isequiv X Y (f : X -> Y) `{IsEquiv _ _ f}
: isepi f.
ua: Univalence
X, Y: Type
f: X -> Y
H: IsEquiv f
isepi f
Proof.
ua: Univalence
X, Y: Type
f: X -> Y
H: IsEquiv f
isepi f
  intros ? g h H'.
ua: Univalence
X, Y: Type
f: X -> Y
H: IsEquiv f
Z: HSet
g, h: Y -> Z
H': (fun x : X => g (f x)) = (fun x : X => h (f x))
g = h
  apply ap10 in H'.
ua: Univalence
X, Y: Type
f: X -> Y
H: IsEquiv f
Z: HSet
g, h: Y -> Z
H': (fun x : X => g (f x)) == (fun x : X => h (f x))
g = h
  apply path_forall.
ua: Univalence
X, Y: Type
f: X -> Y
H: IsEquiv f
Z: HSet
g, h: Y -> Z
H': (fun x : X => g (f x)) == (fun x : X => h (f x))
g == h
  intro x.
ua: Univalence
X, Y: Type
f: X -> Y
H: IsEquiv f
Z: HSet
g, h: Y -> Z
H': (fun x : X => g (f x)) == (fun x : X => h (f x))
x: Y
g x = h x
  transitivity (g (f (f^-1 x))).
ua: Univalence
X, Y: Type
f: X -> Y
H: IsEquiv f
Z: HSet
g, h: Y -> Z
H': (fun x : X => g (f x)) == (fun x : X => h (f x))
x: Y
g x = g (f (f^-1 x))
ua: Univalence
X, Y: Type
f: X -> Y
H: IsEquiv f
Z: HSet
g, h: Y -> Z
H': (fun x : X => g (f x)) == (fun x : X => h (f x))
x: Y
g (f (f^-1 x)) = h x
  -
ua: Univalence
X, Y: Type
f: X -> Y
H: IsEquiv f
Z: HSet
g, h: Y -> Z
H': (fun x : X => g (f x)) == (fun x : X => h (f x))
x: Y
g x = g (f (f^-1 x)) by rewrite eisretr.
  -
ua: Univalence
X, Y: Type
f: X -> Y
H: IsEquiv f
Z: HSet
g, h: Y -> Z
H': (fun x : X => g (f x)) == (fun x : X => h (f x))
x: Y
g (f (f^-1 x)) = h x transitivity (h (f (f^-1 x))).
ua: Univalence
X, Y: Type
f: X -> Y
H: IsEquiv f
Z: HSet
g, h: Y -> Z
H': (fun x : X => g (f x)) == (fun x : X => h (f x))
x: Y
g (f (f^-1 x)) = h (f (f^-1 x))
ua: Univalence
X, Y: Type
f: X -> Y
H: IsEquiv f
Z: HSet
g, h: Y -> Z
H': (fun x : X => g (f x)) == (fun x : X => h (f x))
x: Y
h (f (f^-1 x)) = h x
    *
ua: Univalence
X, Y: Type
f: X -> Y
H: IsEquiv f
Z: HSet
g, h: Y -> Z
H': (fun x : X => g (f x)) == (fun x : X => h (f x))
x: Y
g (f (f^-1 x)) = h (f (f^-1 x)) apply H'.
    *
ua: Univalence
X, Y: Type
f: X -> Y
H: IsEquiv f
Z: HSet
g, h: Y -> Z
H': (fun x : X => g (f x)) == (fun x : X => h (f x))
x: Y
h (f (f^-1 x)) = h x by rewrite eisretr.
Qed.
End AssumingUA.