# Univalent Foundations. Vladimir Voevodsky. Feb. 2010 - Sep. 2011. Port to coq

trunk (8.4-8.5) in March 2014. The third part of the original uu0 file, created on Dec. 3, 2014.
Only one universe is used, and it is never used as a type.
The only axiom we use is funextemptyAxiom , which is the functional extensionality axiom for functions with values in the empty type. Any results that don't depend on axioms should be in an earlier file.

## Contents

• More results on propositions
• Isolated points and types with decidable equality
• Basic results on complements to a point
• Basic results on types with an isolated point
• Weak equivalences and isolated points
• Recomplement on functions
• Standard weak equivalences between compl T t1 and compl T t2 for isolated t1 and t2
• Transposition of two isolated points
• Types with decidable equality
• unit
• bool
• coprod
• Splitting of X into a coproduct by X -> bool
• Semi-boolean hfiber of functions over isolated points
• hfibers of ii1 and ii2
• ii1 and ii2 map isolated points to isolated points
• hfibers of coprodf of two functions
• Coproduct of two functions of h-level n is of h-level n
• h-levels of coproducts and their component types
• h-fibers of the sum of two functions sumofmaps f g
• The sum of two functions of h-level (S (S n)) is of h-level (S (S n))
• The sum of two functions of h-level n with non-intersecting images is of h-level n
• Coproducts and complements
• Decidable propositions and decidable inclusions
• Decidable propositions
• Paths to and from an isolated point form a decidable proposition
• Decidable inclusions
• Decidable inclusions and isolated points
• Decidable inclusions and coprojections

## Preamble

Imports

### More results on propositions

Theorem isapropneg (X : UU) : isaprop (neg X).
Proof.
apply invproofirrelevance.
intros x x'. apply (funextempty X x x').
Defined.

Lemma isaprop_isProofIrrelevant X : isaprop (isProofIrrelevant X).
Proof.
intros. apply invproofirrelevance. intros i j.
apply funextsec; intro x; apply funextsec; intro y.
generalize (i x y) as p; generalize (j x y) as q; intros.
apply isProofIrrelevant_paths. assumption.
Defined.

Corollary isapropdneg (X : UU) : isaprop (dneg X).
Proof.
intro. apply (isapropneg (neg X)).
Defined.

Definition isaninvprop (X : UU) := isweq (todneg X).

Definition invimpl (X : UU) (is : isaninvprop X) : (dneg X) X
:= invmap (make_weq (todneg X) is).

Lemma isapropaninvprop (X : UU) : isaninvprop X isaprop X.
Proof.
intros X0.
apply (isofhlevelweqb (S O) (make_weq (todneg X) X0) (isapropdneg X)).
Defined.

Theorem isaninvpropneg (X : UU) : isaninvprop (neg X).
Proof.
intros.
set (f := todneg (neg X)).
set (g := negf (todneg X)).
set (is1 := isapropneg X).
set (is2 := isapropneg (dneg X)).
apply (isweqimplimpl f g is1 is2).
Defined.

Theorem isapropdec (X : UU) : isaprop X isaprop (decidable X).
Proof.
intros i. apply isapropcoprod.
- exact i.
- apply isapropneg.
- exact (λ x n, n x).
Defined.

## Isolated points and types with decidable equality.

### Basic results on complements to a point

Definition compl (X : UU) (x : X) := x', x != x'.
Definition make_compl (X : UU) (x : X) := tpair (λ x' : X, x != x').
Definition pr1compl (X : UU) (x : X) := @pr1 _ (λ x' : X, x != x').

Lemma isinclpr1compl (X : UU) (x : X) : isincl (pr1compl X x).
Proof.
intros. apply (isinclpr1 _ (λ x' : X, isapropneg _)).
Defined.

Definition recompl (X : UU) (x : X) : compl X x ⨿ unit X
:= λ u : _,
match u with
| ii1 x0pr1compl _ _ x0
| ii2 tx
end.

Definition maponcomplincl {X Y : UU} (f : X Y) (is : isincl f) (x : X) :
compl X x compl Y (f x)
:= λ x0' : _,
match x0' with
tpair _ x' neqxtpair _ (f x')
(negf (invmaponpathsincl _ is x x') neqx)
end.

Definition weqoncompl {X Y : UU} (w : X Y) x : compl X x compl Y (w x).
Proof.
intros. intermediate_weq ( x', w x != w x').
- apply weqfibtototal; intro x'. apply weqiff.
{apply logeqnegs. apply weq_to_iff. apply weqonpaths. }
{apply isapropneg. }
{apply isapropneg. }
- refine (weqfp _ _).
Defined.

Definition weqoncompl_compute {X Y : UU} (w : X Y) (x : X) :
x', pr1 (weqoncompl w x x') = w (pr1 x').
Proof.
intros. induction x' as [x' b]. apply idpath.
Defined.

Definition homotweqoncomplcomp {X Y Z : UU} (f : X Y) (g : Y Z)
(x : X) : homot (weqcomp (weqoncompl f x) (weqoncompl g (f x)))
(weqoncompl (weqcomp f g) x).
Proof.
intros. intro x'. induction x' as [ x' nexx' ].
apply (invmaponpathsincl _ (isinclpr1compl Z _) _ _).
simpl. apply idpath.
Defined.

### Decomposition of a type with an isolated point into two parts weqrecompl

Definition invrecompl (X : UU) (x : X) (is : isisolated X x) :
X coprod (compl X x) unit
:= λ x' : X, match (is x') with
| ii1 eii2 tt
| ii2 phiii1 (make_compl _ _ x' phi)
end.

Theorem isweqrecompl (X : UU) (x : X) (is : isisolated X x) :
isweq (recompl _ x).
Proof.
set (f := recompl _ x). set (g := invrecompl X x is).
unfold invrecompl in g. simpl in g.
assert (efg: x' : X, paths (f (g x')) x').
{
intro. induction (is x') as [ x0 | e ].
- induction x0. unfold f. unfold g. simpl. unfold recompl. simpl.
induction (is x) as [ x0 | e ].
+ simpl. apply idpath.
+ induction (e (idpath x)).
- unfold f. unfold g. simpl. unfold recompl. simpl.
induction (is x') as [ x0 | e0 ].
+ induction (e x0).
+ simpl. apply idpath.
}
assert (egf : u : coprod (compl X x) unit, paths (g (f u)) u).
{
unfold isisolated in is. intro. induction (is (f u)) as [ p | e ].
- induction u as [ c | u].
+ simpl. induction c as [ t x0 ]. simpl in p. induction (x0 p).
+ induction u. assert (e1 : paths (g (f (ii2 tt))) (g x)).
apply (maponpaths g p).
assert (e2 : paths (g x) (ii2 tt)).
{
unfold g. induction (is x) as [ i | e ].
apply idpath.
induction (e (idpath x)).
}
apply (pathscomp0 e1 e2).
- induction u as [ c | u ]. simpl. induction c as [ t x0 ].
simpl. unfold isisolated in is. unfold g. induction (is t) as [ p | e0 ].
induction (x0 p). simpl in g. unfold f. unfold recompl. simpl in e.
assert (ee : e0 = x0)
by apply (proofirrelevance _ (isapropneg (x = t))).
induction ee. apply idpath.
unfold f. unfold g. simpl. induction u. induction (is x).
+ apply idpath.
+ induction (e (idpath x)).
}
apply (isweq_iso f g egf efg).
Defined.

Definition weqrecompl (X : UU) (x : X) (is : isisolated _ x) :
compl X x ⨿ unit X := make_weq _ (isweqrecompl X x is).

### Theorem saying that recompl commutes up to homotopy with maponcomplweq

Theorem homotrecomplnat {X Y : UU} (w : X Y) (x : X) (a : compl X x ⨿ unit) :
recompl Y (w x) (coprodf (weqoncompl w x) (idfun unit) a)
= w (recompl X x a).
Proof.
intros. induction a as [ ane | t ]. induction ane as [ a ne ]. simpl.
apply idpath. induction t. simpl. apply idpath.
Defined.

### Recomplement on functions

Definition recomplf {X Y : UU} (x : X) (y : Y) (isx : isisolated X x)
(f : compl X x compl Y y) : X Y
:= funcomp (funcomp (invmap (weqrecompl X x isx)) (coprodf f (idfun unit)))
(recompl Y y).

Definition weqrecomplf {X Y : UU} (x : X) (y : Y) (isx : isisolated X x)
(isy : isisolated Y y) (w : (compl X x) (compl Y y)) : X Y
:= weqcomp (weqcomp (invweq (weqrecompl X x isx)) (weqcoprodf w (idweq unit)))
(weqrecompl Y y isy).

Definition homotrecomplfhomot {X Y : UU} (x : X) (y : Y) (isx : isisolated X x)
(f f' : compl X x compl Y y) (h : homot f f') :
homot (recomplf x y isx f) (recomplf x y isx f').
Proof.
intros. intro a. unfold recomplf.
apply (maponpaths (recompl Y y)
(homotcoprodfhomot _ _ _ _ h (λ t : unit, idpath t)
(invmap (weqrecompl X x isx) a))).
Defined.

Lemma pathsrecomplfxtoy {X Y : UU} (x : X) (y : Y) (isx : isisolated X x)
(f : compl X x compl Y y) : (recomplf x y isx f x) = y.
Proof.
intros. unfold recomplf. unfold weqrecompl. unfold invmap. simpl.
unfold invrecompl. unfold funcomp. induction (isx x) as [ i1 | i2 ].
- simpl. apply idpath.
- induction (i2 (idpath _)).
Defined.

Definition homotrecomplfcomp {X Y Z : UU} (x : X) (y : Y) (z : Z)
(isx : isisolated X x) (isy : isisolated Y y)
(f : compl X x compl Y y) (g : compl Y y compl Z z) :
homot (funcomp (recomplf x y isx f) (recomplf y z isy g))
(recomplf x z isx (funcomp f g)).
Proof.
intros. intro x'. unfold recomplf.
set (e := homotinvweqweq (weqrecompl Y y isy)
(coprodf f (idfun unit)
(invmap (weqrecompl X x isx) x'))).
unfold funcomp. simpl in e. simpl. rewrite e.
set (e' := homotcoprodfcomp f (idfun unit) g (idfun unit)
(invmap (weqrecompl X x isx) x')).
unfold funcomp in e'. rewrite e'. apply idpath.
Defined.

Definition homotrecomplfidfun {X : UU} (x : X) (isx : isisolated X x) :
homot (recomplf x x isx (idfun (compl X x))) (idfun _).
Proof.
intros. intro x'. unfold recomplf. unfold weqrecompl. unfold invmap. simpl.
unfold invrecompl. unfold funcomp. induction (isx x') as [ e | ne ].
- simpl. apply e.
- simpl. apply idpath.
Defined.

Lemma ishomotinclrecomplf {X Y : UU} (x : X) (y : Y) (isx : isisolated X x)
(f : compl X x compl Y y) (x'n : compl X x) (y'n : compl Y y)
(e : paths (recomplf x y isx f (pr1 x'n)) (pr1 y'n)) : (f x'n) = y'n.
Proof.
intros. induction x'n as [ x' nexx' ]. induction y'n as [ y' neyy' ].
simpl in e . apply (invmaponpathsincl _ (isinclpr1compl _ _)). simpl.
rewrite (pathsinv0 e). unfold recomplf. unfold invmap. unfold coprodf.
simpl. unfold funcomp. unfold invrecompl.
induction (isx x') as [ exx' | nexx'' ].
- induction (nexx' exx').
- simpl. assert (ee : nexx' = nexx'').
apply (proofirrelevance _ (isapropneg _)).
rewrite ee. apply idpath.
Defined.

### Equivalence between complTt1 and complTt2 for isolated t1t2

Definition funtranspos0 {T: UU} (t1 t2 : T) (is2 : isisolated T t2)
(x : compl T t1) : compl T t2
:= match (is2 (pr1 x)) with
| ii1 e
match (is2 t1) with
| ii1 e'fromempty (pr2 x (pathscomp0 (pathsinv0 e') e))
| ii2 ne'make_compl T t2 t1 ne' end
| ii2 nemake_compl T t2 (pr1 x) ne end.

Definition homottranspos0t2t1t1t2 {T : UU} (t1 t2 : T)
(is1 : isisolated T t1) (is2 : isisolated T t2) :
funtranspos0 t2 t1 is1 funtranspos0 t1 t2 is2 ¬ idfun _.
Proof.
intros. intro x. unfold funtranspos0. unfold funcomp.
induction x as [ t net1 ]; simpl.
induction (is2 t) as [ et2 | net2 ].
- induction (is2 t1) as [ et2t1 | net2t1 ].
+ induction (net1 (pathscomp0 (pathsinv0 et2t1) et2)).
+ simpl. induction (is1 t1) as [ e | ne ].
× induction (is1 t2) as [ et1t2 | net1t2 ].
{induction (net2t1 (pathscomp0 (pathsinv0 et1t2) e)). }
{apply (invmaponpathsincl _ (isinclpr1compl _ _)).
simpl. exact et2. }
× induction (ne (idpath _)).
- simpl. induction (is1 t) as [ et1t | net1t ].
+ induction (net1 et1t).
+ apply (invmaponpathsincl _ (isinclpr1compl _ _)). simpl.
apply idpath.
Defined.

Definition weqtranspos0 {T : UU} (t1 t2 : T) :
isisolated T t1 isisolated T t2 compl T t1 compl T t2.
Proof.
intros is1 is2.
simple refine (weq_iso (funtranspos0 t1 t2 is2)
(funtranspos0 t2 t1 is1) _ _).
- intro x. apply (homottranspos0t2t1t1t2 t1 t2 is1 is2).
- intro x. apply (homottranspos0t2t1t1t2 t2 t1 is2 is1).
Defined.

### Transposition of two isolated points

Definition funtranspos {T : UU} (t1 t2 : isolated T) : T T
:= recomplf (pr1 t1) (pr1 t2) (pr2 t1)
(funtranspos0 (pr1 t1) (pr1 t2) (pr2 t2)).

Definition homottranspost2t1t1t2 {T : UU} (t1 t2 : T) (is1 : isisolated T t1)
(is2 : isisolated T t2) :
homot (funcomp (funtranspos (tpair _ t1 is1) (tpair _ t2 is2))
(funtranspos (tpair _ t2 is2) (tpair _ t1 is1))) (idfun _).
Proof.
intros. intro t. unfold funtranspos.
rewrite (homotrecomplfcomp t1 t2 t1 is1 is2 _ _ t).
set (e := homotrecomplfhomot t1 t1 is1 _ (idfun _)
(homottranspos0t2t1t1t2 t1 t2 is1 is2) t).
set (e' := homotrecomplfidfun t1 is1 t).
apply (pathscomp0 e e').
Defined.

Theorem weqtranspos {T : UU} (t1 t2 : T) (is1 : isisolated T t1)
(is2 : isisolated T t2) : T T.
Proof.
intros.
set (f := funtranspos (tpair _ t1 is1) (tpair _ t2 is2)).
set (g := funtranspos (tpair _ t2 is2) (tpair _ t1 is1)).
split with f.
assert (egf : t : T, paths (g (f t)) t)
by (intro; refine (homottranspost2t1t1t2 _ _ _ _ _)).
assert (efg : t : T, paths (f (g t)) t)
by (intro; refine (homottranspost2t1t1t2 _ _ _ _ _)).
apply (isweq_iso _ _ egf efg).
Defined.

Lemma pathsfuntransposoft1 {T : UU} (t1 t2 : T) (is1 : isisolated T t1)
(is2 : isisolated T t2) :
paths (funtranspos (tpair _ t1 is1) (tpair _ t2 is2) t1) t2.
Proof.
intros. unfold funtranspos. rewrite (pathsrecomplfxtoy t1 t2 is1 _).
apply idpath.
Defined.

Lemma pathsfuntransposoft2 {T : UU} (t1 t2 : T) (is1 : isisolated T t1)
(is2 : isisolated T t2) :
paths (funtranspos (tpair _ t1 is1) (tpair _ t2 is2) t2) t1.
Proof.
intros. unfold funtranspos. simpl. unfold funtranspos0.
unfold recomplf. unfold funcomp. unfold coprodf. unfold invmap.
unfold weqrecompl. unfold recompl. simpl. unfold invrecompl.
induction (is1 t2) as [ et1t2 | net1t2 ].
- apply (pathsinv0 et1t2).
- simpl. induction (is2 t2) as [ et2t2 | net2t2 ].
+ induction (is2 t1) as [ et2t1 | net2t1 ].
× induction (net1t2 (pathscomp0 (pathsinv0 et2t1) et2t2)).
× simpl. apply idpath.
+ induction (net2t2 (idpath _)).
Defined.

Lemma pathsfuntransposofnet1t2 {T : UU} (t1 t2 : T) (is1 : isisolated T t1)
(is2 : isisolated T t2) (t : T) (net1t : t1 != t)
(net2t : t2 != t) :
paths (funtranspos (tpair _ t1 is1) (tpair _ t2 is2) t) t.
Proof.
intros. unfold funtranspos. simpl. unfold funtranspos0. unfold recomplf.
unfold funcomp. unfold coprodf. unfold invmap. unfold weqrecompl.
unfold recompl. simpl. unfold invrecompl.
induction (is1 t) as [ et1t | net1t' ].
- induction (net1t et1t).
- simpl. induction (is2 t) as [ et2t | net2t' ]. induction (net2t et2t).
simpl. apply idpath.
Defined.

Lemma homotfuntranspos2 {T : UU} (t1 t2 : T) (is1 : isisolated T t1)
(is2 : isisolated T t2) :
homot (funcomp (funtranspos (tpair _ t1 is1) (tpair _ t2 is2))
(funtranspos (tpair _ t1 is1) (tpair _ t2 is2))) (idfun _).
Proof.
intros. intro t. unfold funcomp. unfold idfun.
induction (is1 t) as [ et1t | net1t ].
- rewrite (pathsinv0 et1t). rewrite (pathsfuntransposoft1 _ _).
rewrite (pathsfuntransposoft2 _ _). apply idpath.
- induction (is2 t) as [ et2t | net2t ].
+ rewrite (pathsinv0 et2t).
rewrite (pathsfuntransposoft2 _ _). rewrite (pathsfuntransposoft1 _ _).
apply idpath.
+ rewrite (pathsfuntransposofnet1t2 _ _ _ _ _ net1t net2t).
rewrite (pathsfuntransposofnet1t2 _ _ _ _ _ net1t net2t).
apply idpath.
Defined.

## Semi-boolean hfiber of functions over isolated points

Definition eqbx (X : UU) (x : X) (is : isisolated X x) : X bool.
Proof.
intros x'. induction (is x'). apply true. apply false.
Defined.

Lemma iscontrhfibereqbx (X : UU) (x : X) (is : isisolated X x) :
iscontr (hfiber (eqbx X x is) true).
Proof.
intros.
assert (b : (eqbx X x is x) = true).
{
unfold eqbx. induction (is x) as [ e | ne ].
- apply idpath.
- induction (ne (idpath _)).
}
set (i := make_hfiber (eqbx X x is) x b). split with i.
unfold eqbx. induction (boolchoice (eqbx X x is x)) as [ b' | nb' ].
- intro t. induction t as [ x' e ].
assert (e' : x' = x).
{
induction (is x') as [ ee | nee ]. apply (pathsinv0 ee).
induction (nopathsfalsetotrue e) .
}
apply (invmaponpathsincl _ (isinclfromhfiber (eqbx X x is) isasetbool true)
(make_hfiber _ x' e) i e').
- induction (nopathstruetofalse (pathscomp0 (pathsinv0 b) nb')).
Defined.

Definition bhfiber {X Y : UU} (f : X Y) (y : Y) (is : isisolated Y y)
:= hfiber (λ x : X, eqbx Y y is (f x)) true.

Lemma weqhfibertobhfiber {X Y : UU} (f : X Y) (y : Y) (is : isisolated Y y) :
(hfiber f y) (bhfiber f y is).
Proof.
intros. set (g := eqbx Y y is). set (ye := pr1 (iscontrhfibereqbx Y y is)).
split with (hfibersftogf f g true ye).
apply (isofhlevelfffromZ 0 _ _ ye (fibseqhf f g true ye)).
apply (isapropifcontr).
apply (iscontrhfibereqbx _ y is).
Defined.

### h-fibers of ii1 and ii2

Theorem isinclii1 (X Y : UU) : isincl (@ii1 X Y).
Proof.
intros.
set (f := @ii1 X Y). set (g := coprodtoboolsum X Y).
set (gf := λ x : X, (g (f x))).
set (gf' := λ x : X, tpair (boolsumfun X Y) true x).
assert (h : x : X, paths (gf' x) (gf x))
by (intro; apply idpath).
assert (is1 : isofhlevelf (S O) gf')
by apply (isofhlevelfsnfib O (boolsumfun X Y) true (isasetbool true true)).
assert (is2 : isofhlevelf (S O) gf)
by apply (isofhlevelfhomot (S O) gf' gf h is1).
apply (isofhlevelff (S O) _ _ is2 (isofhlevelfweq (S (S O))
(weqcoprodtoboolsum X Y))).
Defined.

Corollary iscontrhfiberii1x (X Y : UU) (x : X) :
iscontr (hfiber (@ii1 X Y) (ii1 x)).
Proof.
intros.
set (xe1 := make_hfiber (@ii1 _ _) x (idpath (@ii1 X Y x))).
apply (iscontraprop1 (isinclii1 X Y (ii1 x)) xe1).
Defined.

Corollary neghfiberii1y (X Y : UU) (y : Y) : neg (hfiber (@ii1 X Y) (ii2 y)).
Proof.
intros. intro xe. induction xe as [ x e ]. apply (negpathsii1ii2 _ _ e).
Defined.

Theorem isinclii2 (X Y : UU) : isincl (@ii2 X Y).
Proof.
intros.
set (f := @ii2 X Y). set (g := coprodtoboolsum X Y).
set (gf := λ y : Y, (g (f y))).
set (gf' := λ y : Y, tpair (boolsumfun X Y) false y).
assert (h : y : Y, paths (gf' y) (gf y))
by (intro; apply idpath).
assert (is1 : isofhlevelf (S O) gf')
by apply (isofhlevelfsnfib O (boolsumfun X Y) false
(isasetbool false false)).
assert (is2 : isofhlevelf (S O) gf)
by apply (isofhlevelfhomot (S O) gf' gf h is1).
apply (isofhlevelff (S O) _ _ is2
(isofhlevelfweq (S (S O)) (weqcoprodtoboolsum X Y))).
Defined.

Corollary iscontrhfiberii2y (X Y : UU) (y : Y) :
iscontr (hfiber (@ii2 X Y) (ii2 y)).
Proof.
intros. set (xe1 := make_hfiber (@ii2 _ _) y (idpath (@ii2 X Y y))).
apply (iscontraprop1 (isinclii2 X Y (ii2 y)) xe1).
Defined.

Corollary neghfiberii2x (X Y : UU) (x : X) : neg (hfiber (@ii2 X Y) (ii1 x)).
Proof.
intros. intro ye. induction ye as [ y e ]. apply (negpathsii2ii1 _ _ e).
Defined.

Lemma negintersectii1ii2 {X Y : UU} (z : coprod X Y) :
hfiber (@ii1 X Y) z hfiber (@ii2 _ _) z empty.
Proof.
intros X0 X1. induction X0 as [ t x ]. induction X1 as [ t0 x0 ].
set (e := pathscomp0 x (pathsinv0 x0)).
apply (negpathsii1ii2 _ _ e).
Defined.

### ii1 and ii2 map isolated points to isolated points

Lemma isolatedtoisolatedii1 (X Y : UU) (x : X) (is : isisolated _ x) :
isisolated (coprod X Y) (ii1 x).
Proof.
intros. unfold isisolated. intro x'. induction x' as [ x0 | y ].
- induction (is x0) as [ p | e ].
+ apply (ii1 (maponpaths (@ii1 X Y) p)).
+ apply (ii2 (negf (invmaponpathsincl (@ii1 X Y) (isinclii1 X Y) _ _) e)).
- apply (ii2 (negpathsii1ii2 x y)).
Defined.

Lemma isolatedtoisolatedii2 (X Y : UU) (y : Y) (is : isisolated _ y) :
isisolated (coprod X Y) (ii2 y).
Proof.
intros. intro x'. induction x' as [ x | y0 ].
- apply (ii2 (negpathsii2ii1 x y)).
- induction (is y0) as [ p | e ].
+ apply (ii1 (maponpaths (@ii2 X Y) p)).
+ apply (ii2 (negf (invmaponpathsincl (@ii2 X Y) (isinclii2 X Y) _ _) e)).
Defined.

### h-fibers of coprodf of two functions

Theorem weqhfibercoprodf1 {X Y X' Y' : UU} (f : X X') (g : Y Y')
(x' : X') : weq (hfiber f x') (hfiber (coprodf f g) (ii1 x')).
Proof.
intros.
set (ix := @ii1 X Y). set (ix' := @ii1 X' Y').
set (fpg := coprodf f g). set (fpgix := λ x : X, (fpg (ix x))).
assert (w1 : weq (hfiber f x') (hfiber fpgix (ix' x')))
by apply (samehfibers f ix' (isinclii1 _ _) x').
assert (w2 : weq (hfiber fpgix (ix' x')) (hfiber fpg (ix' x'))).
{
split with (hfibersgftog ix fpg (ix' x')). unfold isweq. intro y.

set (u := invezmaphf ix fpg (ix' x') y).
assert (is : isweq u) by apply isweqinvezmaphf.

apply (iscontrweqb (make_weq u is)).
induction y as [ xy e ]. induction xy as [ x0 | y0 ].
- simpl. apply iscontrhfiberofincl. apply (isinclii1 X Y).
- apply (fromempty ((negpathsii2ii1 x' (g y0)) e)).
}
apply (weqcomp w1 w2).
Defined.

Theorem weqhfibercoprodf2 {X Y X' Y' : UU} (f : X X') (g : Y Y') (y' : Y') :
weq (hfiber g y') (hfiber (coprodf f g) (ii2 y')).
Proof.
intros.
set (iy := @ii2 X Y). set (iy' := @ii2 X' Y').
set (fpg := coprodf f g). set (fpgiy := λ y : Y, (fpg (iy y))).
assert (w1 : weq (hfiber g y') (hfiber fpgiy (iy' y')))
by apply (samehfibers g iy' (isinclii2 _ _) y').
assert (w2 : weq (hfiber fpgiy (iy' y')) (hfiber fpg (iy' y'))).
{
split with (hfibersgftog iy fpg (iy' y')). unfold isweq. intro y.

set (u:= invezmaphf iy fpg (iy' y') y).
assert (is : isweq u) by apply isweqinvezmaphf.

apply (iscontrweqb (make_weq u is)).
induction y as [ xy e ]. induction xy as [ x0 | y0 ].
simpl. apply (fromempty ((negpathsii1ii2 (f x0) y') e)). simpl.
apply iscontrhfiberofincl. apply (isinclii2 X Y).
}
apply (weqcomp w1 w2).
Defined.

### Theorem saying that coproduct of two functions of h-level n is of h-level n

Theorem isofhlevelfcoprodf (n : nat) {X Y Z T : UU} (f : X Z) (g : Y T)
(is1 : isofhlevelf n f) (is2 : isofhlevelf n g) :
isofhlevelf n (coprodf f g).
Proof.
intros. unfold isofhlevelf. intro y. induction y as [ z | t ].
apply (isofhlevelweqf n (weqhfibercoprodf1 f g z)). apply (is1 z).
apply (isofhlevelweqf n (weqhfibercoprodf2 f g t)). apply (is2 t).
Defined.

### Theorems about h-levels of coproducts and their component types

Theorem isofhlevelsnsummand1 (n : nat) (X Y : UU) :
isofhlevel (S n) (coprod X Y) isofhlevel (S n) X.
Proof.
intros is.
apply (isofhlevelXfromfY (S n) (@ii1 X Y)
(isofhlevelfsnincl n _ (isinclii1 _ _)) is).
Defined.

Theorem isofhlevelsnsummand2 (n : nat) (X Y : UU) :
isofhlevel (S n) (coprod X Y) isofhlevel (S n) Y.
Proof.
intros is.
apply (isofhlevelXfromfY (S n) (@ii2 X Y)
(isofhlevelfsnincl n _ (isinclii2 _ _)) is).
Defined.

Theorem isofhlevelssncoprod (n : nat) (X Y : UU) (isx : isofhlevel (S (S n)) X)
(isy : isofhlevel (S (S n)) Y) : isofhlevel (S (S n)) (coprod X Y).
Proof.
intros. apply isofhlevelfromfun.
set (f := coprodf (λ x : X, tt) (λ y : Y, tt)).
assert (is1 : isofhlevelf (S (S n)) f)
by apply (isofhlevelfcoprodf (S (S n)) _ _ (isofhleveltofun _ X isx)
(isofhleveltofun _ Y isy)).
assert (is2 : isofhlevel (S (S n)) (coprod unit unit))
by apply (isofhlevelweqb (S (S n)) boolascoprod
(isofhlevelssnset n _ (isasetbool))).
apply (isofhlevelfgf (S (S n)) _ _ is1 (isofhleveltofun _ _ is2)).
Defined.

Lemma isasetcoprod (X Y : UU) (isx : isaset X) (isy : isaset Y) :
isaset (coprod X Y).
Proof.
intros. apply (isofhlevelssncoprod 0 _ _ isx isy).
Defined.

### h-fibers of the sum of two functions sumofmapsfg

Lemma coprodofhfiberstohfiber {X Y Z : UU} (f : X Z) (g : Y Z) (z : Z) :
(hfiber f z) ⨿ (hfiber g z) hfiber (sumofmaps f g) z.
Proof.
intros hfg.
induction hfg as [ hf | hg ].
- induction hf as [ x fe ]. split with (ii1 x). simpl. assumption.
- induction hg as [ y ge ]. split with (ii2 y). simpl. assumption.
Defined.

Lemma hfibertocoprodofhfibers {X Y Z : UU} (f : X Z) (g : Y Z) (z : Z) :
hfiber (sumofmaps f g) z (hfiber f z) ⨿ (hfiber g z).
Proof.
intros hsfg.
induction hsfg as [ xy e ]. induction xy as [ x | y ].
- simpl in e. apply (ii1 (make_hfiber _ x e)).
- simpl in e. apply (ii2 (make_hfiber _ y e)).
Defined.

Theorem weqhfibersofsumofmaps {X Y Z : UU} (f : X Z) (g : Y Z) (z : Z) :
weq ((hfiber f z) ⨿ (hfiber g z)) (hfiber (sumofmaps f g) z).
Proof.
intros.
set (ff := coprodofhfiberstohfiber f g z).
set (gg := hfibertocoprodofhfibers f g z).
split with ff.
assert (effgg : hsfg : _, paths (ff (gg hsfg)) hsfg).
{
intro. induction hsfg as [ xy e ]. induction xy as [ x | y ].
- simpl. apply idpath.
- simpl. apply idpath.
}
assert (eggff : hfg : _, paths (gg (ff hfg)) hfg).
{
intro. induction hfg as [ hf | hg ]. induction hf as [ x fe ].
- simpl. apply idpath.
- induction hg as [ y ge ]. simpl. apply idpath.
}
apply (isweq_iso _ _ eggff effgg).
Defined.

### Theorem saying that the sum of two functions of h-level (S (S n)) is of hlevel (S (S n))

Theorem isofhlevelfssnsumofmaps (n : nat) {X Y Z : UU} (f : X Z) (g : Y Z)
(isf : isofhlevelf (S (S n)) f) (isg : isofhlevelf (S (S n)) g) :
isofhlevelf (S (S n)) (sumofmaps f g).
Proof.
intros. intro z.
set (w := weqhfibersofsumofmaps f g z).
set (is := isofhlevelssncoprod n _ _ (isf z) (isg z)).
apply (isofhlevelweqf _ w is).
Defined.

### The sum of two functions of h-level n with non-intersecting images is of h-level n

Lemma noil1 {X Y Z : UU} (f : X Z) (g : Y Z)
(noi : (x : X) (y : Y), neg (paths (f x) (g y))) (z : Z) :
hfiber f z hfiber g z empty.
Proof.
intros hfz hgz.
induction hfz as [ x fe ]. induction hgz as [ y ge ].
apply (noi x y (pathscomp0 fe (pathsinv0 ge))).
Defined.

Lemma weqhfibernoi1 {X Y Z : UU} (f : X Z) (g : Y Z)
(noi : (x : X) (y : Y), neg (paths (f x) (g y))) (z : Z)
(xe : hfiber f z) : (hfiber (sumofmaps f g) z) (hfiber f z).
Proof.
intros.
set (w1 := invweq (weqhfibersofsumofmaps f g z)).
assert (a : neg (hfiber g z)) by (intro ye; apply (noil1 f g noi z xe ye)).
set (w2 := invweq (weqii1withneg (hfiber f z) a)). apply (weqcomp w1 w2).
Defined.

Lemma weqhfibernoi2 {X Y Z : UU} (f : X Z) (g : Y Z)
(noi : (x : X) (y : Y), neg (paths (f x) (g y))) (z : Z)
(ye : hfiber g z) : (hfiber (sumofmaps f g) z) (hfiber g z).
Proof.
intros. set (w1 := invweq (weqhfibersofsumofmaps f g z)).
assert (a : neg (hfiber f z)). intro xe. apply (noil1 f g noi z xe ye).
set (w2 := invweq (weqii2withneg (hfiber g z) a)).
apply (weqcomp w1 w2).
Defined.

Theorem isofhlevelfsumofmapsnoi (n : nat) {X Y Z : UU} (f : X Z) (g : Y Z)
(isf : isofhlevelf n f) (isg : isofhlevelf n g)
(noi : (x : X) (y : Y), neg (paths (f x) (g y))) :
isofhlevelf n (sumofmaps f g).
Proof.
intros. intro z. induction n as [ | n ].
- set (zinx := invweq (make_weq _ isf) z).
set (ziny := invweq (make_weq _ isg) z).
assert (ex : (f zinx) = z) by apply (homotweqinvweq (make_weq _ isf) z).
assert (ey : (g ziny) = z) by apply (homotweqinvweq (make_weq _ isg) z).
induction ((noi zinx ziny) (pathscomp0 ex (pathsinv0 ey))).
- apply isofhlevelsn. intro hfgz.
induction ((invweq (weqhfibersofsumofmaps f g z) hfgz)) as [ xe | ye ].
+ apply (isofhlevelweqb _ (weqhfibernoi1 f g noi z xe) (isf z)).
+ apply (isofhlevelweqb _ (weqhfibernoi2 f g noi z ye) (isg z)).
Defined.

### Coproducts and complements

Definition tocompltoii1x (X Y : UU) (x : X) :
coprod (compl X x) Y compl (coprod X Y) (ii1 x).
Proof.
intros X0. induction X0 as [ c | y ].
- split with (ii1 (pr1 c)).
assert (e : neg (x = (pr1 c))) by apply (pr2 c).
apply (negf (invmaponpathsincl (@ii1 _ _) (isinclii1 X Y) _ _) e).
- split with (ii2 y). apply (negf (pathsinv0) (negpathsii2ii1 x y)).
Defined.

Definition fromcompltoii1x (X Y : UU) (x : X) :
compl (coprod X Y) (ii1 x) coprod (compl X x) Y.
Proof.
intros X0. induction X0 as [ t x0 ]. induction t as [ x1 | y ].
- assert (ne : x != x1) by apply (negf (maponpaths (@ii1 _ _)) x0).
apply (ii1 (make_compl _ _ x1 ne)).
- apply (ii2 y).
Defined.

Theorem isweqtocompltoii1x (X Y : UU) (x : X) : isweq (tocompltoii1x X Y x).
Proof.
intros.
set (f := tocompltoii1x X Y x). set (g := fromcompltoii1x X Y x).
assert (egf : nexy : _, paths (g (f nexy)) nexy).
{
intro. induction nexy as [ c | y ].
- induction c as [ t x0 ]. simpl.
assert (e : paths (negf (maponpaths (@ii1 X Y))
(negf (invmaponpathsincl (@ii1 X Y)
(isinclii1 X Y) x t) x0))
x0) by apply (isapropneg (x = t)).
apply (maponpaths (fun ee : x != tii1 (make_compl X x t ee)) e).
- apply idpath.
}
assert (efg: neii1x : _, paths (f (g neii1x)) neii1x).
{
intro. induction neii1x as [ t x0 ]. induction t as [ x1 | y ].
- simpl.
assert (e : paths (negf (invmaponpathsincl (@ii1 X Y)
(isinclii1 X Y) x x1)
(negf (maponpaths (@ii1 X Y)) x0)) x0)
by apply (isapropneg (paths _ _)).
apply (maponpaths (fun ee : (neg (paths (ii1 x) (ii1 x1)))
⇒ (make_compl _ _ (ii1 x1) ee)) e).
- simpl.
assert (e : paths (negf pathsinv0 (negpathsii2ii1 x y)) x0)
by apply (isapropneg (paths _ _)).
apply (maponpaths (fun ee : (neg (paths (ii1 x) (ii2 y)))
⇒ (make_compl _ _ (ii2 y) ee)) e).
}
apply (isweq_iso f g egf efg).
Defined.

Definition tocompltoii2y (X Y : UU) (y : Y) :
coprod X (compl Y y) compl (coprod X Y) (ii2 y).
Proof.
intros X0. induction X0 as [ x | c ].
- split with (ii1 x). apply (negpathsii2ii1 x y).
- split with (ii2 (pr1 c)).
assert (e : neg(y = (pr1 c))) by apply (pr2 c).
apply (negf (invmaponpathsincl (@ii2 _ _) (isinclii2 X Y) _ _) e).
Defined.

Definition fromcompltoii2y (X Y : UU) (y : Y) :
compl (coprod X Y) (ii2 y) coprod X (compl Y y).
Proof.
intros X0. induction X0 as [ t x ]. induction t as [ x0 | y0 ].
- apply (ii1 x0).
- assert (ne : y != y0) by apply (negf (maponpaths (@ii2 _ _)) x).
apply (ii2 (make_compl _ _ y0 ne)).
Defined.

Theorem isweqtocompltoii2y (X Y : UU) (y : Y) : isweq (tocompltoii2y X Y y).
Proof.
intros.
set (f := tocompltoii2y X Y y). set (g := fromcompltoii2y X Y y).
assert (egf : nexy : _, paths (g (f nexy)) nexy).
{
intro. induction nexy as [ x | c ].
- apply idpath.
- induction c as [ t x ]. simpl.

assert (e : paths (negf (maponpaths (@ii2 X Y))
(negf (invmaponpathsincl (@ii2 X Y)
(isinclii2 X Y) y t) x))
x) by apply (isapropneg (y = t)).

apply (maponpaths (fun ee : y != tii2 (make_compl _ y t ee)) e).
}
assert (efg : neii2x : _, paths (f (g neii2x)) neii2x).
{
intro. induction neii2x as [ t x ]. induction t as [ x0 | y0 ].
- simpl.
assert (e : (negpathsii2ii1 x0 y) = x)
by apply (isapropneg (paths _ _)).
apply (maponpaths (fun ee : (neg (paths (ii2 y) (ii1 x0)))
⇒ (make_compl _ _ (ii1 x0) ee)) e).
- simpl.
assert (e : paths (negf (invmaponpathsincl _ (isinclii2 X Y) y y0)
(negf (maponpaths (@ii2 X Y)) x)) x)
by apply (isapropneg (paths _ _)).
apply (maponpaths (fun ee : (neg (paths (ii2 y) (ii2 y0)))
⇒ (make_compl _ _ (ii2 y0) ee)) e).
}
apply (isweq_iso f g egf efg).
Defined.

Definition tocompltodisjoint (X : UU) : X compl (coprod X unit) (ii2 tt)
:= λ x : _, make_compl _ _ (ii1 x) (negpathsii2ii1 x tt).

Definition fromcompltodisjoint (X : UU) : compl (coprod X unit) (ii2 tt) X.
Proof.
intros X0. induction X0 as [ t x ]. induction t as [ x0 | u ].
- assumption.
- induction u. apply (fromempty (x (idpath (ii2 tt)))).
Defined.

Lemma isweqtocompltodisjoint (X : UU) : isweq (tocompltodisjoint X).
Proof.
intros.
set (ff := tocompltodisjoint X). set (gg := fromcompltodisjoint X).
assert (egf : x : X, paths (gg (ff x)) x) by (intro; apply idpath).
assert (efg : xx : _, paths (ff (gg xx)) xx).
{
intro. induction xx as [ t x ]. induction t as [ x0 | u ].
- simpl. unfold ff. unfold tocompltodisjoint. simpl.
assert (ee : (negpathsii2ii1 x0 tt) = x)
by apply (proofirrelevance _ (isapropneg _)).
induction ee. apply idpath.
- induction u. simpl. apply (fromempty (x (idpath _))).
}
apply (isweq_iso ff gg egf efg).
Defined.

Definition weqtocompltodisjoint (X : UU) : X compl (X ⨿ unit) (ii2 tt)
:= make_weq _ (isweqtocompltodisjoint X).

Corollary isweqfromcompltodisjoint (X : UU) : isweq (fromcompltodisjoint X).
Proof.
intros. apply (isweqinvmap (weqtocompltodisjoint X)).
Defined.

## Decidable propositions and decidable inclusions

### Decidable propositions isdecprop

Lemma isdecpropif' (X : UU) : isaprop X X ⨿ ¬ X iscontr (X ⨿ ¬ X).
Proof.
intros is a.
assert (is1 : isaprop (coprod X (neg X))) by (apply isapropdec; assumption).
apply (iscontraprop1 is1 a).
Defined.

Lemma isdecproppaths {X : UU} (is : isdeceq X) (x x' : X) :
isdecprop (x = x').
Proof.
intros. apply (isdecpropif _ (isasetifdeceq _ is x x') (is x x')).
Defined.

Lemma isdeceqif {X : UU} (is : x x' : X, isdecprop (x = x')) : isdeceq X.
Proof.
intros. intros x x'. apply (pr1 (is x x')).
Defined.

Lemma isaninv1 (X : UU) : isdecprop X isaninvprop X.
Proof.
intros is1. unfold isaninvprop.
assert (is2 := pr1 is1); simpl in is2.
{intro X0. induction is2 as [ a | b ].
- assumption.
assert (is3: isaprop (dneg X)).
{apply (isapropneg (X empty)). }
apply (isweqimplimpl (todneg X) adjevinv is1 is3).
Defined.

Theorem isdecpropfibseq1 {X Y Z : UU} (f : X Y) (g : Y Z) (z : Z)
(fs : fibseqstr f g z) : isdecprop X isaprop Z isdecprop Y.
Proof.
intros isx isz.
assert (isc : iscontr Z) by apply (iscontraprop1 isz z).
assert (X0 : isweq f) by apply (isweqfinfibseq f g z fs isc).
apply (isdecpropweqf (make_weq _ X0) isx).
Defined.

Theorem isdecpropfibseq0 {X Y Z : UU} (f : X Y) (g : Y Z) (z : Z)
(fs : fibseqstr f g z) : isdecprop Y isdeceq Z isdecprop X.
Proof.
intros isy isz.
assert (isg : isofhlevelf 1 g)
by apply (isofhlevelffromXY 1 g (isdecproptoisaprop _ isy)
(isasetifdeceq _ isz)).
assert (isp : isaprop X) by apply (isofhlevelXfromg 1 f g z fs isg).
induction (pr1 isy) as [ y | ny ].
- apply (isdecpropfibseq1 _ _ y (fibseq1 f g z fs y)
(isdecproppaths isz (g y) z)
(isdecproptoisaprop _ isy)).
- apply (isdecpropif _ isp (ii2 (negf f ny))).
Defined.

Theorem isdecpropdirprod {X Y : UU} (isx : isdecprop X) (isy : isdecprop Y) :
isdecprop (X × Y).
Proof.
intros.
assert (isp : isaprop (X × Y))
by apply (isofhleveldirprod 1 _ _ (isdecproptoisaprop _ isx)
(isdecproptoisaprop _ isy)).
induction (pr1 isx) as [ x | nx ].
- induction (pr1 isy) as [ y | ny ].
+ apply (isdecpropif _ isp (ii1 (make_dirprod x y))).
+ assert (nxy : neg (X × Y)).
{
intro xy. induction xy as [ x0 y0 ]. apply (ny y0).
}
apply (isdecpropif _ isp (ii2 nxy)).
- assert (nxy : neg (X × Y)).
{
intro xy. induction xy as [ x0 y0 ]. apply (nx x0).
}
apply (isdecpropif _ isp (ii2 nxy)).
Defined.

Lemma fromneganddecx {X Y : UU} : isdecprop X ¬ (X × Y) ¬X ⨿ ¬Y.
Proof.
intros isx nf.
induction (pr1 isx) as [ x | nx ].
- assert (ny := negf (λ y : Y, make_dirprod x y) nf).
exact (ii2 ny).
- exact (ii1 nx).
Defined.

Lemma fromneganddecy {X Y : UU} : isdecprop Y ¬ (X × Y) ¬X ⨿ ¬Y.
Proof.
intros isy nf. induction (pr1 isy) as [ y | ny ].
- assert (nx := negf (λ x : X, make_dirprod x y) nf).
exact (ii1 nx).
- exact (ii2 ny).
Defined.

### Paths to and from an isolated point form a decidable proposition

Lemma isdecproppathsfromisolated (X : UU) (x : X) (is : isisolated X x)
(x' : X) : isdecprop (x = x').
Proof.
intros. apply isdecpropif.
- apply isaproppathsfromisolated. assumption.
- apply (is x').
Defined.

Lemma isdecproppathstoisolated (X : UU) (x : X) (is : isisolated X x)
(x' : X) : isdecprop (x' = x).
Proof.
intros.
apply (isdecpropweqf (weqpathsinv0 x x')
(isdecproppathsfromisolated X x is x')).
Defined.

### Decidable inclusions

Definition isdecincl {X Y : UU} (f : X Y) := y : Y, isdecprop (hfiber f y).
Lemma isdecincltoisincl {X Y : UU} (f : X Y) : isdecincl f isincl f.
Proof.
intros is y. apply (isdecproptoisaprop _ (is y)).
Defined.
Coercion isdecincltoisincl : isdecincl >-> isincl.

Lemma isdecinclfromisweq {X Y : UU} (f : X Y) : isweq f isdecincl f.
Proof.
intros iswf. intro y. apply (isdecpropfromiscontr (iswf y)).
Defined.

Lemma isdecpropfromdecincl {X Y : UU} (f : X Y) :
isdecincl f isdecprop Y isdecprop X.
Proof.
intros isf isy.
induction (pr1 isy) as [ y | n ].
- assert (w : weq (hfiber f y) X)
by apply (weqhfibertocontr
f y (iscontraprop1 (isdecproptoisaprop _ isy) y)).
apply (isdecpropweqf w (isf y)).
- apply isdecpropif. apply (isapropinclb _ isf isy). apply (ii2 (negf f n)).
Defined.

Lemma isdecinclii1 (X Y : UU) : isdecincl (@ii1 X Y).
Proof.
intros. intro y. induction y as [ x | y ].
- apply (isdecpropif _ (isinclii1 X Y (ii1 x))
(ii1 (make_hfiber (@ii1 _ _) x (idpath _)))).
- apply (isdecpropif _ (isinclii1 X Y (ii2 y))
(ii2 (neghfiberii1y X Y y))).
Defined.

Lemma isdecinclii2 (X Y : UU) : isdecincl (@ii2 X Y).
Proof.
intros. intro y. induction y as [ x | y ].
- apply (isdecpropif _ (isinclii2 X Y (ii1 x)) (ii2 (neghfiberii2x X Y x))).
- apply (isdecpropif _ (isinclii2 X Y (ii2 y))
(ii1 (make_hfiber (@ii2 _ _) y (idpath _)))).
Defined.

Lemma isdecinclpr1 {X : UU} (P : X UU) (is : x : X, isdecprop (P x)) :
isdecincl (@pr1 _ P).
Proof.
intros. intro x.
assert (w : weq (P x) (hfiber (@pr1 _ P) x)) by apply ezweqpr1.
apply (isdecpropweqf w (is x)).
Defined.

Theorem isdecinclhomot {X Y : UU} (f g : X Y)
(h : x : X, paths (f x) (g x)) (is : isdecincl f) : isdecincl g.
Proof.
intros. intro y.
apply (isdecpropweqf (weqhfibershomot f g h y) (is y)).
Defined.

Theorem isdecinclcomp {X Y Z : UU} (f : X Y) (g : Y Z)
(isf : isdecincl f) (isg : isdecincl g) : isdecincl (λ x : X, g (f x)).
Proof.
intros. intro z.
set (gf := λ x : X, g (f x)).
assert (wy : ye : hfiber g z, weq (hfiber f (pr1 ye))
(hfiber (hfibersgftog f g z) ye))
by apply ezweqhf.
assert (ww : y : Y, weq (hfiber f y) (hfiber gf (g y))).
{
intro. apply (samehfibers f g). apply (isdecincltoisincl _ isg).
}
induction (pr1 (isg z)) as [ ye | nye ].
- induction ye as [ y e ]. induction e. apply (isdecpropweqf (ww y) (isf y)).
- assert (wz : (hfiber gf z) (hfiber g z)).
{
split with (hfibersgftog f g z). intro ye. induction (nye ye).
}
apply (isdecpropweqb wz (isg z)).
Defined.

The conditions of the following theorem can be weakened by assuming only that the h-fibers of g satisfy isdeceq i.e. are "sets with decidable equality".

Theorem isdecinclf {X Y Z : UU} (f : X Y) (g : Y Z) (isg : isincl g)
(isgf : isdecincl (λ x : X, g (f x))) : isdecincl f.
Proof.
intros. intro y. set (gf := λ x : _, g (f x)).
assert (ww : weq (hfiber f y) (hfiber gf (g y)))
by (apply (samehfibers f g); assumption).
apply (isdecpropweqb ww (isgf (g y))).
Defined.

Theorem isdecinclg {X Y Z : UU} (f : X Y) (g : Y Z) (isf : isweq f)
(isgf : isdecincl (λ x : X, g (f x))) : isdecincl g.
Proof.
intros. intro z.
set (gf := λ x : X, g (f x)).
assert (w : (hfiber gf z) (hfiber g z)).
{
split with (hfibersgftog f g z). intro ye.
assert (ww : weq (hfiber f (pr1 ye)) (hfiber (hfibersgftog f g z) ye))
by apply ezweqhf.
apply (iscontrweqf ww (isf (pr1 ye))).
}
apply (isdecpropweqf w (isgf z)).
Defined.

### Decidable inclusions and isolated points

Theorem isisolateddecinclf {X Y : UU} (f : X Y) (x : X) :
isdecincl f isisolated X x isisolated Y (f x).
Proof.
intros isf isx.
assert (is' : y : Y, isdecincl (d1g f y x)).
{
intro y. intro xe. set (w := ezweq2g f x xe).
apply (isdecpropweqf w (isdecproppathstoisolated X x isx _)).
}
assert (is'' : y : Y, isdecprop ((f x) = y))
by (intro; apply (isdecpropfromdecincl _ (is' y) (isf y))).
intro y'.
apply (pr1 (is'' y')).
Defined.

### Decidable inclusions and coprojections

Definition negimage {X Y : UU} (f : X Y) : UU
:= total2 (λ y : Y, neg (hfiber f y)).
Definition make_negimage {X Y : UU} (f : X Y) :
t : Y, ¬ hfiber f t y : Y, ¬ hfiber f y
:= tpair (λ y : Y, neg (hfiber f y)).

Lemma isinclfromcoprodwithnegimage {X Y : UU} (f : X Y) (is : isincl f) :
isincl (sumofmaps f (@pr1 _ (λ y : Y, neg (hfiber f y)))).
Proof.
intros.
assert (noi : (x : X) (nx : negimage f), neg (paths (f x) (pr1 nx))).
{
intros x nx e. induction nx as [ y nhf ]. simpl in e.
apply (nhf (make_hfiber _ x e)).
}
assert (is' : isincl (@pr1 _ (λ y : Y, neg (hfiber f y)))).
{
apply isinclpr1. intro y. apply isapropneg.
}
apply (isofhlevelfsumofmapsnoi 1 f _ is is' noi).
Defined.

Definition iscoproj {X Y : UU} (f : X Y) : UU
:= isweq (sumofmaps f (@pr1 _ (λ y : Y, neg (hfiber f y)))).

Definition weqcoproj {X Y : UU} (f : X Y) (is : iscoproj f) :
weq (coprod X (negimage f)) Y := make_weq _ is.

Theorem iscoprojfromisdecincl {X Y : UU} (f : X Y) (is : isdecincl f) :
iscoproj f.
Proof.
intros.
set (p := sumofmaps f (@pr1 _ (λ y : Y, neg (hfiber f y)))).
assert (is' : isincl p).
{
apply isinclfromcoprodwithnegimage. apply (isdecincltoisincl _ is).
}
unfold iscoproj. intro y. induction (pr1 (is y)) as [ h | nh ].
- induction h as [ x e ]. induction e. change (f x) with (p (ii1 x)).
apply iscontrhfiberofincl. assumption.
- change y with (p (ii2 (make_negimage _ y nh))). apply iscontrhfiberofincl.
assumption.
Defined.

Theorem isdecinclfromiscoproj {X Y : UU} (f : X Y) (is : iscoproj f) :
isdecincl f.
Proof.
intros.
set (g := (sumofmaps f (@pr1 _ (λ y : Y, neg (hfiber f y))))).
set (f' := λ x : X, g (ii1 x)).
assert (is' : isdecincl f')
by apply (isdecinclcomp _ _ (isdecinclii1 _ _) (isdecinclfromisweq _ is)).
assumption.
Defined.