Equivalences

Table of Contents

1 Equivalence Properties

module Lib.Prop.Equiv where

This file states multiple properties of equivalences. First, it shows that equivalences are an equivalence relation. Then, it shows closure and 3-for-2 properties. It defines an utility to chain equivalences. Finally, it shows equivalences between multiple types.

1.1 Packages imports

The imported packages can be accessed via the following links: 

import Lib.ContrMap
import Lib.QInv
import Lib.Data.Decidability  
import Lib.Data.Empty
import Lib.Data.Map
import Lib.Prop.Contr
import Lib.Prop.Paths
import Lib.Prop.Sg
import Lib.Prop.Unit

1.2 Accessors

Equiv/map (A B : U) (e : Equiv A B) : A → B = e.1
Equiv/is-equiv (A B : U) (e : Equiv A B) : is-equiv A B (Equiv/map A B e) = e.2

1.3 Inverse of an equivalence

We can define the inverse map of an equivalence. 

is-equiv/inv-map (A B : U) (f : A → B) (e : is-equiv A B f) : B → A =
  λy. (e y).1.1

Equiv/inv-map (A B : U) (e : Equiv A B) : B → A =
  is-equiv/inv-map A B (Equiv/map A B e) (Equiv/is-equiv A B e)

Futhermore, this inverse map is also an equivalence. 

is-equiv/inv-left-htpy (A B : U) (f : A → B) (e : is-equiv A B f) (x : A)
                            : Path A (is-equiv/inv-map A B f e (f x)) x =
  λi. ((e (f x)).2 (x, refl B (f x)) i).1

is-equiv/inv-right-htpy (A B : U) (f : A → B) (e : is-equiv A B f) (y : B)
                             : Path B (f (is-equiv/inv-map A B f e y)) y =
  inv B y
    ( f (is-equiv/inv-map A B f e y))
    ( e y).1.2

is-equiv/inv-is-equiv (A B : U) (f : A → B) (e : is-equiv A B f) : is-equiv B A (is-equiv/inv-map A B f e) =
  has-inverse/is-equiv B A
    ( is-equiv/inv-map A B f e)
    ( f,
      ( is-equiv/inv-left-htpy A B f e,
        is-equiv/inv-right-htpy A B f e))

Equiv/inv-equiv (A B : U) (e : Equiv A B) : Equiv B A =
  ( Equiv/inv-map A B e,
    is-equiv/inv-is-equiv A B
      ( Equiv/map A B e)
      ( Equiv/is-equiv A B e))

Moreover, we get the nice properties of inverse maps. 

Equiv/inv-right-htpy (A B : U) (e : Equiv A B) : Htpy' B B (λz. (Equiv/map A B e) (Equiv/inv-map A B e z)) (id B) =
  is-equiv/inv-right-htpy A B (Equiv/map A B e) (Equiv/is-equiv A B e)

Equiv/inv-left-htpy (A B : U) (e : Equiv A B) : Htpy' A A (λz. (Equiv/inv-map A B e) (Equiv/map A B e z)) (id A) =
  is-equiv/inv-left-htpy A B (Equiv/map A B e) (Equiv/is-equiv A B e)

1.4 Equivalence relation properties

is-equiv and Equiv are equivalence relations, that is, they are:

  • reflexive ;
  • symmetric ;
  • transitive.

The first property is handled in Prelude.ctt, but we redefine them here with a name consistent with the others properties: is-equiv/prop (resp. Equiv/prop). Then, we focus on showing the symmetry and the transitivity of this relation.

1.4.1 Reflexivity

is-equiv/refl (A : U) : is-equiv A A (id A)
  = id/is-equiv A

Equiv/refl (A : U) : Equiv A A
  = IdEquiv A

1.4.2 Symmetry

is-equiv/sym : (A B : U) → (f : A → B) → (e : is-equiv A B f) → is-equiv B A (is-equiv/inv-map A B f e) = is-equiv/inv-is-equiv 

Equiv/sym : (A B : U) → (e : Equiv A B) → Equiv B A = Equiv/inv-equiv

1.4.3 Transitivity

is-equiv/trans (A B C : U) (f : A → B) (g : B → C) (eF : is-equiv A B f) (eG : is-equiv B C g) : is-equiv A C (map/comp A B C g f) =
  is-bi-inv/is-equiv A C (map/comp A B C g f)
                         (is-bi-inv/comp-is-bi-inv A B C f g (is-equiv/is-bi-inv A B f eF) (is-equiv/is-bi-inv B C g eG))

Equiv/trans (A B C : U) (e-AB : Equiv A B) (e-BC : Equiv B C) : Equiv A C =
  (map/comp A B C (Equiv/map B C e-BC) (Equiv/map A B e-AB), is-equiv/trans A B C (Equiv/map A B e-AB) (Equiv/map B C e-BC) (Equiv/is-equiv A B e-AB) (Equiv/is-equiv B C e-BC))

1.5 Some facts on equivalences

1.5.1 A map to Empty is always an equivalence

First, we show that if f : is-empty A, then is-equiv f. Hence, we are given an element of Empty and thus ex-falso suffices to show that the fibers of f are contractible. 

is-empty/is-equiv (A : U) (f : is-empty A) : is-equiv A Empty f =
  λx. ind-Empty (λy. is-contr (Fib A Empty f y)) x

Thus, if is-empty A, we have an equivalence between A and Empty. 

Empty/equiv (A : U) (f : is-empty A) : Equiv A Empty =
  (f, is-empty/is-equiv A f)

1.5.2 Decidability is closed under equivalences

We show that if A and B are equivalent, then A is decidable iff B is decidable. 

is-decidable/is-equiv (A B : U) (f : A → B) (e : is-equiv A B f) (dB : is-decidable B) : is-decidable A =
  Coprod/map B (neg B) A (neg A)
             (is-equiv/inv-map A B f e)
             (λg a. g (f a)) dB

is-decidable-is-equiv' (A B : U) (f : A → B) (e : is-equiv A B f) (dA : is-decidable A) : is-decidable B =
  is-decidable/is-equiv B A (is-equiv/inv-map A B f e) (is-equiv/sym A B f e) dA

is-decidable/Equiv (A B : U) (e : Equiv A B) (dB : is-decidable B) : is-decidable A =
  Coprod/map B (neg B) A (neg A)
             (Equiv/inv-map A B e)
             (λf a. f ((Equiv/map A B e) a)) dB

is-decidable/Equiv' (A B : U) (e : Equiv A B) (dA : is-decidable A) : is-decidable B =
  is-decidable/Equiv B A (Equiv/sym A B e) dA

1.5.3 Equality decidability is closed under equivalences

We show that if A and B are equivalent, then A has decidable equality iff B has decidable equality. 

has-decidable-equality/is-equiv (A B : U) (f : A → B) (e : is-equiv A B f) (dB : has-decidable-equality B) : has-decidable-equality A =
  λx y.
    let eq-A : U = (Path A x y)
        eq-B : U = (Path B (f x) (f y)) 
        g : B → A = is-equiv/inv-map A B f e
        p : Path (A → A) (λz. g (f z)) (id A) = eq-htpy A (λ_. A) (λz. g (f z)) (id A) (is-equiv/inv-left-htpy A B f e)
        h : Path B (f x) (f y) → Path A x y = λq. (tr (A → A) (λz. g (f z)) (id A) p (λi. Path A (i x) (i y)) (ap B A g (f x) (f y) q))
    in
    Coprod/map eq-B (neg eq-B) eq-A (neg eq-A) h
                    (λi q. i (ap A B f x y q)) (dB (f x) (f y))

has-decidable-equality/is-equiv' (A B : U) (f : A → B) (e : is-equiv A B f) (dA : has-decidable-equality A) : has-decidable-equality B =
  has-decidable-equality/is-equiv B A (is-equiv/inv-map A B f e) (is-equiv/inv-is-equiv A B f e) dA

has-decidable-equality/Equiv (A B : U) (e : Equiv A B) (dB : has-decidable-equality B) : has-decidable-equality A =
  has-decidable-equality/is-equiv A B (Equiv/map A B e) (Equiv/is-equiv A B e) dB

has-decidable-equality/Equiv' (A B : U) (e : Equiv A B) (dA : has-decidable-equality A) : has-decidable-equality B =
  has-decidable-equality/is-equiv' A B (Equiv/map A B e) (Equiv/is-equiv A B e) dA

1.5.4 Equivalent types have equivalent identity types

If A and B are two equivalent types, then there is also an equivalence between their identity types. 

Equiv/Equiv-id (A B : U) (e : Equiv A B) (x y : A) : Equiv (Path A x y) (Path B (Equiv/map A B e x) (Equiv/map A B e y)) =
  (ap A B (Equiv/map A B e) x y, Equiv/is-inj A B (Equiv/map A B e) (Equiv/is-equiv A B e) x y)

1.5.5 Equivalences are injective

Obviously, if e(x) = e(y) for some equivalence e, then x = y. 

map-Equiv/is-injective (A B : U) (e : Equiv A B) (x y : A) (p : Path B (Equiv/map A B e x) (Equiv/map A B e y))
                            : Path A x y =
  comp-n A three-Nat x
    ( Equiv/inv-map A B e (Equiv/map A B e x))
    ( inv A
      ( Equiv/inv-map A B e (Equiv/map A B e x)) x
      ( Equiv/inv-left-htpy A B e x))
    ( Equiv/inv-map A B e (Equiv/map A B e y))
    ( ap B A (Equiv/inv-map A B e) (Equiv/map A B e x) (Equiv/map A B e y) p) y
    ( Equiv/inv-left-htpy A B e y)

1.6 Chain of equivalences

A comp-like chaining of equivalences. 

Equiv/comp/type (A : U) : Nat → U → U = split
  zero → λB. Equiv A B
  suc n → λB. (C : U) (e : Equiv B C) → Equiv/comp/type A n C  

Equiv/comp : (n : Nat) (A : U) (B : U) (e : Equiv A B) → Equiv/comp/type A n B = split
  zero → λ_ _ e. e
  suc n → λA B e C e'. Equiv/comp n A C (Equiv/trans A B C e e')

1.7 3-for-2 properties

1.7.1 3-for-2 property of equiv closure under composition

Given f : A → B and g : B → C the 3-for-2 property of equivalence closure under composition states that if any two of the three assertions

  • f is an equivalence
  • g is an equivalence
  • g ˆ f is an equivalence

hold, then so does the third. 

is-equiv/comp-is-equiv (A B C : U) (f : A → B) (g : B → C) (e : is-equiv A B f) (e' : is-equiv B C g)
                              : is-equiv A C (λz. g (f z)) =
  is-bi-inv/is-equiv A C
    ( λz. g (f z))
    ( is-bi-inv/comp-is-bi-inv A B C f g
        ( is-equiv/is-bi-inv A B f e)
        ( is-equiv/is-bi-inv B C g e'))

is-equiv/comp-left-is-equiv (A B C : U) (f : A → B) (g : B → C) (e : is-equiv B C g) (e' : is-equiv A C (λz. g (f z)))
                                   : is-equiv A B f =
  is-bi-inv/is-equiv A B f
    ( is-bi-inv/is-bi-inv-comp-left A B C f g
      ( is-equiv/is-bi-inv B C g e)
      ( is-equiv/is-bi-inv A C (λz. g (f z)) e'))

is-equiv/comp-right-is-equiv (A B C : U) (f : A → B) (g : B → C) (e : is-equiv A B f) (e' : is-equiv A C (λz. g (f z)))
                                    : is-equiv B C g =
  is-bi-inv/is-equiv B C g
    ( is-bi-inv/is-bi-inv-comp-right A B C f g
      ( is-equiv/is-bi-inv A B f e)
      ( is-equiv/is-bi-inv A C (λz. g (f z)) e'))

1.7.2 3-for-2 property of contractibility

Given f : A \to B, the 3-for-2 property of contractibility states that if any two of the three assertions

  • A is contractible
  • B is contractible
  • f is an equivalence

hold, then so does the third. We start by showing that if one of A or B is contractible and f is an equivalence, then the other is also contractible. It is easy: take the center of the contraction to be the x such that f x = b (given by the center of the equivalence), and the path is obtained using the contractibility of the fibrations of f. 

is-contr/is-contr-equiv (A B : U) (e : Equiv A B) (c : is-contr B) : is-contr A =
  let b : B = center B c
      f : A → B = Equiv/map A B e
      fc : Fib A B f b = (center (Fib A B f b) (Equiv/is-equiv A B e b))
      x : A = fc.1
      p : (y : A) → Path A x y = λy. Sg-path/left A (λz. Path B b (f z)) fc (y, contraction B c (f y)) ((Equiv/is-equiv A B e b).2 (y, contraction B c (f y)))
  in (x, p)

The other side is trivial. 

is-contr/is-contr-equiv' (A B : U) (e : Equiv A B) (c : is-contr A) : is-contr B =
  is-contr/is-contr-equiv B A (Equiv/sym A B e) c

Now, if two types are contractible, they are obviously equivalent: they both hold only one object, thus there is a trivial bijection between them. 

is-contr/is-equiv (A B : U) (f : A → B) (cA : is-contr A) (cB : is-contr B) : is-equiv A B f =
  λy.
    let t : Fib A B f y = (center A cA, is-contr/all-elements-equal B cB y (f (center A cA))) in
    ( t,
      λu.
        let p : Path A t.1 u.1 = is-contr/all-elements-equal A cA t.1 u.1 in
        SgPathO→PathΣ A
          ( λx. Path B y (f x)) t u
          ( p,
            is-contr→is-set B cB y (f u.1) (tr A t.1 u.1 p (λx. Path B y (f x)) t.2) u.2))

is-contr/Equiv (A B : U) (cA : is-contr A) (cB : is-contr B) : Equiv A B =
  let f : A → B = λ_. center B cB in
  ( f,
    is-contr/is-equiv A B f cA cB)

1.8 Equivalences between types

1.8.1 Coprod Empty A

There is a bi-invertible map between Coprod Empty A and A. 

is-equiv/is-bi-inv-copr-empty-type-map (A : U) : Coprod Empty A → A = split
  inl x → ex-falso A x
  inr y → y

is-equiv/is-bi-inv-copr-empty-type-inv-map (A : U) : A → Coprod Empty A = λx. inr x

is-equiv/is-bi-inv-copr-empty-type-left-htpy (A : U) : Htpy' (Coprod Empty A) (Coprod Empty A)
                                                             (λz. (is-equiv/is-bi-inv-copr-empty-type-inv-map A) (is-equiv/is-bi-inv-copr-empty-type-map A z)) (id (Coprod Empty A)) = split
  inl x → ex-falso (Path (Coprod Empty A) ((is-equiv/is-bi-inv-copr-empty-type-inv-map A) (is-equiv/is-bi-inv-copr-empty-type-map A (inl x))) (inl x)) x
  inr y → refl (Coprod Empty A) (inr y)

is-equiv/is-bi-inv-copr-empty-type (A : U) : is-bi-inv (Coprod Empty A) A (is-equiv/is-bi-inv-copr-empty-type-map A) =
  has-inverse-is-bi-inv (Coprod Empty A) A (is-equiv/is-bi-inv-copr-empty-type-map A)
    (is-equiv/is-bi-inv-copr-empty-type-inv-map A, (λx. refl A x, is-equiv/is-bi-inv-copr-empty-type-left-htpy A))

That is, these types are equivalent. 

is-equiv/is-equiv-copr-empty-type (A : U) : is-equiv (Coprod Empty A) A (is-equiv/is-bi-inv-copr-empty-type-map A) =
  is-bi-inv/is-equiv (Coprod Empty A) A (is-equiv/is-bi-inv-copr-empty-type-map A) (is-equiv/is-bi-inv-copr-empty-type A)

Equiv/Equiv-copr-empty-type (A : U) : Equiv (Coprod Empty A) A =
  (is-equiv/is-bi-inv-copr-empty-type-map A, is-equiv/is-equiv-copr-empty-type A)

1.8.2 Coprod is commutative

As expected, there is a bi-invertible map between Coprod A B and Coprod B A. 

is-equiv/is-bi-inv-comm-copr-map (A B : U) : Coprod A B → Coprod B A = split
  inl x → inr x
  inr y → inl y

is-equiv/is-bi-inv-comm-copr-map-htpy (A B : U) : Htpy' (Coprod B A) (Coprod B A) 
                                                        (λz. (is-equiv/is-bi-inv-comm-copr-map A B) (is-equiv/is-bi-inv-comm-copr-map B A z)) (id (Coprod B A)) = split
  inl x → refl (Coprod B A) (inl x)
  inr y → refl (Coprod B A) (inr y)

is-equiv/is-bi-inv-comm-copr (A B : U) : is-bi-inv (Coprod A B) (Coprod B A) (is-equiv/is-bi-inv-comm-copr-map A B) =
  has-inverse-is-bi-inv (Coprod A B) (Coprod B A) (is-equiv/is-bi-inv-comm-copr-map A B)
    (is-equiv/is-bi-inv-comm-copr-map B A, (is-equiv/is-bi-inv-comm-copr-map-htpy A B, is-equiv/is-bi-inv-comm-copr-map-htpy B A))

That is, Coprod is commutative. 

is-equiv/commutative-coprod (A B : U) : is-equiv (Coprod A B) (Coprod B A) (is-equiv/is-bi-inv-comm-copr-map A B) =
  is-bi-inv/is-equiv (Coprod A B) (Coprod B A) (is-equiv/is-bi-inv-comm-copr-map A B) (is-equiv/is-bi-inv-comm-copr A B)

Equiv/commutative-coprod (A B : U) : Equiv (Coprod A B) (Coprod B A) =
  (is-equiv/is-bi-inv-comm-copr-map A B, is-equiv/commutative-coprod A B)

1.8.3 Coprod A Empty

As such, Coprod A Empty is also equivalent to A. 

Equiv/Equiv-copr-type-empty (A : U) : Equiv (Coprod A Empty) A =
  Equiv/trans (Coprod A Empty) (Coprod Empty A) A (Equiv/commutative-coprod A Empty) (Equiv/Equiv-copr-empty-type A)

1.8.4 Σ Empty A is Empty

For any type family A over Empty, Σ Empty A is empty. 

Equiv/is-equiv-Sg-empty-map (A : Empty → U) : (Σ Empty A) → Empty =
  λu. u.1

Equiv/is-equiv-Sg-empty-inv-map (A : Empty → U) : Empty → (Σ Empty A) =
  λx. (x, ex-falso (A x) x)

Equiv/is-equiv-Sg-empty-right-htpy (A : Empty → U) : Htpy' Empty Empty
                                                           (λz. (Equiv/is-equiv-Sg-empty-map A) (Equiv/is-equiv-Sg-empty-inv-map A z))
                                                           (id Empty) = λx. refl Empty x

Equiv/is-equiv-Sg-empty-left-htpy (A : Empty → U) : Htpy' (Σ Empty A) (Σ Empty A)
                                                          (λz. (Equiv/is-equiv-Sg-empty-inv-map A) (Equiv/is-equiv-Sg-empty-map A z))
                                                          (id (Σ Empty A)) =
  λu. ex-falso (Path (Σ Empty A) ((Equiv/is-equiv-Sg-empty-inv-map A) (Equiv/is-equiv-Sg-empty-map A u)) u) u.1

Equiv/is-equiv-Sg-empty (A : Empty → U) : is-equiv (Σ Empty A) Empty (Equiv/is-equiv-Sg-empty-map A) =
  has-inverse/is-equiv (Σ Empty A) Empty (Equiv/is-equiv-Sg-empty-map A)
    (Equiv/is-equiv-Sg-empty-inv-map A, (Equiv/is-equiv-Sg-empty-right-htpy A, Equiv/is-equiv-Sg-empty-left-htpy A))

Equiv/Equiv-Sg-empty (A : Empty → U) : Equiv (Σ Empty A) Empty =
  (Equiv/is-equiv-Sg-empty-map A, Equiv/is-equiv-Sg-empty A)

1.8.5 Σ distributes over coproduct

Equiv/Sg-distr-over-coprod-map/sg (A B : U) (C : (Coprod A B) → U) : (z : Coprod A B) → (C z) → (Coprod (Σ A (λx. C (inl x))) (Σ B (λy. C (inr y)))) = split
  inl x → λc. inl (x, c)
  inr y → λc. inr (y, c)

Equiv/Sg-distr-over-coprod-map (A B : U) (C : (Coprod A B) → U) : (Σ (Coprod A B) C) → (Coprod (Σ A (λx. C (inl x))) (Σ B (λy. C (inr y)))) =
  λu. Equiv/Sg-distr-over-coprod-map/sg A B C u.1 u.2

Equiv/Sg-distr-over-coprod-inv-map (A B : U) (C : (Coprod A B) → U) : (Coprod (Σ A (λx. C (inl x))) (Σ B (λy. C (inr y)))) → (Σ (Coprod A B) C) = split
  inl u → (inl u.1, u.2)
  inr v → (inr v.1, v.2)

Equiv/Sg-distr-over-coprod-right-htpy (A B : U) (C : (Coprod A B) → U) : Htpy' (Coprod (Σ A (λx. C (inl x))) (Σ B (λy. C (inr y))))
                                                                               (Coprod (Σ A (λx. C (inl x))) (Σ B (λy. C (inr y))))
                                                                               (λz. (Equiv/Sg-distr-over-coprod-map A B C) (Equiv/Sg-distr-over-coprod-inv-map A B C z))
                                                                               (id (Coprod (Σ A (λx. C (inl x))) (Σ B (λy. C (inr y))))) = split
  inl u → refl (Coprod (Σ A (λx. C (inl x))) (Σ B (λy. C (inr y)))) (inl u)
  inr v → refl (Coprod (Σ A (λx. C (inl x))) (Σ B (λy. C (inr y)))) (inr v)

Equiv/Sg-distr-over-coprod-left-htpy/sg (A B : U) (C : (Coprod A B) → U)
                                             : (z : (Coprod A B)) → (c : C z) → Path (Σ (Coprod A B) C)
                                                                                     ((Equiv/Sg-distr-over-coprod-inv-map A B C) (Equiv/Sg-distr-over-coprod-map A B C (z, c)))
                                                                                     (z, c) = split
  inl x → λc. refl (Σ (Coprod A B) C) (inl x, c)
  inr y → λc. refl (Σ (Coprod A B) C) (inr y, c)

Equiv/Sg-distr-over-coprod-left-htpy (A B : U) (C : (Coprod A B) → U) : Htpy' (Σ (Coprod A B) C) (Σ (Coprod A B) C)
                                                                              (λz. (Equiv/Sg-distr-over-coprod-inv-map A B C) (Equiv/Sg-distr-over-coprod-map A B C z))
                                                                              (id (Σ (Coprod A B) C)) =
  λu. Equiv/Sg-distr-over-coprod-left-htpy/sg A B C u.1 u.2

Equiv/Sg-distr-over-coprod-is-equiv (A B : U) (C : (Coprod A B) → U) : is-equiv (Σ (Coprod A B) C) (Coprod (Σ A (λx. C (inl x))) (Σ B (λy. C (inr y))))
                                                                                (Equiv/Sg-distr-over-coprod-map A B C) =
  has-inverse/is-equiv (Σ (Coprod A B) C) (Coprod (Σ A (λx. C (inl x))) (Σ B (λy. C (inr y)))) (Equiv/Sg-distr-over-coprod-map A B C)
    (Equiv/Sg-distr-over-coprod-inv-map A B C, (Equiv/Sg-distr-over-coprod-right-htpy A B C, Equiv/Sg-distr-over-coprod-left-htpy A B C))


Equiv/Sg-distr-over-coprod (A B : U) (C : (Coprod A B) → U) : Equiv (Σ (Coprod A B) C) (Coprod (Σ A (λx. C (inl x))) (Σ B (λy. C (inr y)))) =
  (Equiv/Sg-distr-over-coprod-map A B C, Equiv/Sg-distr-over-coprod-is-equiv A B C)

1.8.6 Σ Unit A is (A star)

Equiv/Sg-unit-map/sg (A : Unit → U) : (x : Unit) → (A x) → A star = split
  star → (id (A star))

Equiv/Sg-unit-map (A : Unit → U) : (Σ Unit A) → (A star) = λu. Equiv/Sg-unit-map/sg A u.1 u.2

Equiv/Sg-unit-inv-map (A : Unit → U) : (A star) → (Σ Unit A) = λa. (star, a)

Equiv/Sg-unit-right-htpy (A : Unit → U) : Htpy' (A star) (A star) (λz. (Equiv/Sg-unit-map A) (Equiv/Sg-unit-inv-map A z)) (id (A star)) =
  λa. refl (A star) a

Equiv/Sg-unit-left-htpy/sg (A : Unit → U) : (x : Unit) → (a : A x) → Path (Σ Unit A) ((Equiv/Sg-unit-inv-map A) (Equiv/Sg-unit-map A (x, a))) (x, a) = split
  star → λa. refl (Σ Unit A) (star, a)

Equiv/Sg-unit-left-htpy (A : Unit → U) : Htpy' (Σ Unit A) (Σ Unit A) (λz. (Equiv/Sg-unit-inv-map A) (Equiv/Sg-unit-map A z)) (id (Σ Unit A)) =
  λu. Equiv/Sg-unit-left-htpy/sg A u.1 u.2

Equiv/Sg-unit-is-equiv (A : Unit → U) : is-equiv (Σ Unit A) (A star) (Equiv/Sg-unit-map A) =
  has-inverse/is-equiv (Σ Unit A) (A star) (Equiv/Sg-unit-map A)
    (Equiv/Sg-unit-inv-map A, (Equiv/Sg-unit-right-htpy A, Equiv/Sg-unit-left-htpy A))

Equiv/Sg-unit (A : Unit → U) : Equiv (Σ Unit A) (A star) =
  (Equiv/Sg-unit-map A, Equiv/Sg-unit-is-equiv A)

1.8.7 Fib pr1 is B x

Equiv/fib-pr1-space-map (A : U) (B : A → U) (x : A) (u : Fib (Σ A B) A (λu. u.1) x) : B x =
  let x' : A = u.1.1
      y  : B x' = u.1.2
      p  : Path A x x' = u.2
  in tr A x' x (inv A x x' p) B y

Equiv/fib-pr1-space-inv-map (A : U) (B : A → U) (x : A) (y : B x) : Fib (Σ A B) A (λu. u.1) x =
  ((x, y), refl A x)

Equiv/fib-pr1-space-right-htpy (A : U) (B : A → U) (x : A) : Htpy' (B x) (B x)
                                                                   (λz. (Equiv/fib-pr1-space-map A B x) (Equiv/fib-pr1-space-inv-map A B x z))
                                                                   (id (B x)) =
  λy. comp (B x) (tr A x x (inv A x x (refl A x)) B y)
           (tr A x x (refl A x) B y) (ap (Path A x x) (B x) (λp. tr A x x p B y) (inv A x x (refl A x)) (refl A x) (inv/refl A x))
           y (tr/refl-path A x B y)

Equiv/fib-pr1-space-left-htpy/refl (A : U) (B : A → U) (x : A) (y : B x)
                                      : Path (Fib (Σ A B) A (λu. u.1) x)
                                             ((Equiv/fib-pr1-space-inv-map A B x) (Equiv/fib-pr1-space-map A B x ((x, y), refl A x)))
                                             ((x, y), refl A x) =
  comp (Fib (Σ A B) A (λu. u.1) x) ((x, tr A x x (inv A x x (refl A x)) B y), refl A x)
                                   ((x, tr A x x (refl A x) B y), refl A x)
                                   (ap (Path A x x) (Fib (Σ A B) A (λu. u.1) x) (λp. ((x, tr A x x p B y), refl A x))
                                       (inv A x x (refl A x)) (refl A x) (inv/refl A x))
                                   ((x, y), refl A x)
                                   (ap (B x) (Fib (Σ A B) A (λu. u.1) x) (λy'. ((x, y'), refl A x)) (tr A x x (refl A x) B y) y
                                       (tr/refl-path A x B y))

Equiv/fib-pr1-space-left-htpy/sg (A : U) (B : A → U) (x : A) (x' : A) (y : B x') (p : Path A x x')
                                    : Path (Fib (Σ A B) A (λu. u.1) x)
                                           ((Equiv/fib-pr1-space-inv-map A B x) (Equiv/fib-pr1-space-map A B x ((x', y), p)))
                                           ((x', y), p) =
  J A x (λx'' q. (y' : B x'') → Path (Fib (Σ A B) A (λu. u.1) x) ((Equiv/fib-pr1-space-inv-map A B x) (Equiv/fib-pr1-space-map A B x ((x'', y'), q))) ((x'', y'), q))
        (λy'. Equiv/fib-pr1-space-left-htpy/refl A B x y') x' p y

Equiv/fib-pr1-space-left-htpy (A : U) (B : A → U) (x : A) : Htpy' (Fib (Σ A B) A (λu. u.1) x) (Fib (Σ A B) A (λu. u.1) x)
                                                                  (λz. (Equiv/fib-pr1-space-inv-map A B x) (Equiv/fib-pr1-space-map A B x z))
                                                                  (id (Fib (Σ A B) A (λu. u.1) x)) =
  λu. Equiv/fib-pr1-space-left-htpy/sg A B x u.1.1 u.1.2 u.2

We have shown that there is a bijection between (Fib pr1 x) and (B x), that is, these two spaces are equivalent. 

Equiv/fib-space-is-equiv (A : U) (B : A → U) (x : A) : is-equiv (Fib (Σ A B) A (λu. u.1) x) (B x) (Equiv/fib-pr1-space-map A B x) =
  has-inverse/is-equiv (Fib (Σ A B) A (λu. u.1) x) (B x) (Equiv/fib-pr1-space-map A B x)
    (Equiv/fib-pr1-space-inv-map A B x, (Equiv/fib-pr1-space-right-htpy A B x, Equiv/fib-pr1-space-left-htpy A B x))

Equiv/fib-space-Equiv (A : U) (B : A → U) (x : A) : Equiv (Fib (Σ A B) A (λu. u.1) x) (B x) =
  (Equiv/fib-pr1-space-map A B x, Equiv/fib-space-is-equiv A B x)

1.8.8 Σ fib is A

equiv-total-fib/map (A B : U) (f : A → B) (t : Σ B (Fib A B f)) : A = t.2.1

equiv-total-fib/inv-map (A B : U) (f : A → B) (x : A) : Σ B (Fib A B f) = (f x, (x, refl B (f x)))

equiv-total-fib/right-htpy (A B : U) (f : A → B) : Htpy' A A (λz. (equiv-total-fib/map A B f) (equiv-total-fib/inv-map A B f z)) (id A) =
  λx. refl A x

equiv-total-fib/left-htpy/refl (A B : U) (f : A → B) (x : A) 
                                     : Path (Σ B (Fib A B f)) ((equiv-total-fib/inv-map A B f) (equiv-total-fib/map A B f (f x, (x, inv B (f x) (f x) (refl B (f x))))))
                                            (f x, (x, inv B (f x) (f x) (refl B (f x)))) =
  ap (Path B (f x) (f x)) (Σ B (Fib A B f)) (λp. (f x, (x, p))) (refl B (f x)) (inv B (f x) (f x) (refl B (f x))) (refl/sym B (f x))

equiv-total-fib/left-htpy' (A B : U) (f : A → B) (y : B) (x : A) (p : Path B (f x) y)
                                : Path (Σ B (Fib A B f)) ((equiv-total-fib/inv-map A B f) (equiv-total-fib/map A B f (y, (x, inv B (f x) y p)))) (y, (x, inv B (f x) y p)) =
  J B (f x) (λz q. Path (Σ B (Fib A B f)) ((equiv-total-fib/inv-map A B f) (equiv-total-fib/map A B f (z, (x, inv B (f x) z q)))) (z, (x, inv B (f x) z q)))
            (equiv-total-fib/left-htpy/refl A B f x) y p

equiv-total-fib/left-htpy (A B : U) (f : A → B)
                               : Htpy' (Σ B (Fib A B f)) (Σ B (Fib A B f))
                                       (λz. (equiv-total-fib/inv-map A B f) (equiv-total-fib/map A B f z)) (id (Σ B (Fib A B f))) =
  λu.
    let x : A = u.2.1
        y : B = u.1
        p : Path B y (f x) = u.2.2
    in comp-n (Σ B (Fib A B f)) three-Nat ((equiv-total-fib/inv-map A B f) (equiv-total-fib/map A B f (y, (x, p))))
        ((equiv-total-fib/inv-map A B f) (equiv-total-fib/map A B f (y, (x, inv B (f x) y (inv B y (f x) p)))))
        (ap (Path B y (f x)) (Σ B (Fib A B f)) (λq. (equiv-total-fib/inv-map A B f) (equiv-total-fib/map A B f (y, (x, q)))) p (inv B (f x) y (inv B y (f x) p))
            (inv/involutive' B y (f x) p))
        (y, (x, inv B (f x) y (inv B y (f x) p))) (equiv-total-fib/left-htpy' A B f y x (inv B y (f x) p))
        (y, (x, p)) (ap (Path B y (f x)) (Σ B (Fib A B f)) (λq. (y, (x, q))) (inv B (f x) y (inv B y (f x) p)) p (inv/involutive B y (f x) p))

equiv-total-fib/Equiv (A B : U) (f : A → B) : Equiv (Σ B (Fib A B f)) A =
  has-inverse/Equiv (Σ B (Fib A B f)) A (equiv-total-fib/map A B f)
    (equiv-total-fib/inv-map A B f, (equiv-total-fib/right-htpy A B f, equiv-total-fib/left-htpy A B f))

Equiv/total-fib (A B : U) (f : A → B) : Equiv A (Σ B (Fib A B f)) =
  has-inverse/Equiv A
    ( Σ B (Fib A B f))
    ( equiv-total-fib/inv-map A B f)
    ( equiv-total-fib/map A B f,
      ( equiv-total-fib/left-htpy A B f, equiv-total-fib/right-htpy A B f))

1.8.9 Σ A Empty is empty

Equiv/Sg-empty-map (A : U) (u : Σ A (λ_. Empty)) : Empty = u.2

Equiv/Sg-empty-inv-map (A : U) (n : Empty) : Σ A (λ_. Empty) = (ex-falso A n, n)

Equiv/Sg-empty-right-htpy (A : U) : Htpy' Empty Empty (λz. (Equiv/Sg-empty-map A) (Equiv/Sg-empty-inv-map A z)) (id Empty) =
  λn. ex-falso (Path Empty ((Equiv/Sg-empty-map A) (Equiv/Sg-empty-inv-map A n)) n) n

Equiv/Sg-empty-left-htpy (A : U) : Htpy' (Σ A (λ_. Empty)) (Σ A (λ_. Empty)) (λz. (Equiv/Sg-empty-inv-map A) (Equiv/Sg-empty-map A z)) (id (Σ A (λ_. Empty))) =
  λn. ex-falso (Path (Σ A (λ_. Empty)) ((Equiv/Sg-empty-inv-map A) (Equiv/Sg-empty-map A n)) n) (n.2)

Equiv/Sg-empty (A : U) : Equiv (Σ A (λ_. Empty)) Empty =
  has-inverse/Equiv (Σ A (λ_. Empty)) Empty (Equiv/Sg-empty-map A)
    (Equiv/Sg-empty-inv-map A, (Equiv/Sg-empty-right-htpy A, Equiv/Sg-empty-left-htpy A))

1.8.10 Σ A Unit is A

Equiv/Sg-base-unit-map (A : U) (u : Σ A (λ_. Unit)) : A = u.1

Equiv/Sg-base-unit-inv-map (A : U) (x : A) : Σ A (λ_. Unit) = (x, star)

Equiv/Sg-base-unit-right-htpy (A : U) : Htpy' A A (λz. (Equiv/Sg-base-unit-map A) (Equiv/Sg-base-unit-inv-map A z)) (id A) =
  λx. refl A x

Equiv/Sg-base-unit-left-htpy (A : U) : Htpy' (Σ A (λ_. Unit)) (Σ A (λ_. Unit))
                                             (λz. (Equiv/Sg-base-unit-inv-map A) (Equiv/Sg-base-unit-map A z)) (id (Σ A (λ_. Unit))) =
  λu. Eq-prod/eq A Unit ((Equiv/Sg-base-unit-inv-map A) (Equiv/Sg-base-unit-map A u)) u (refl A u.1, Unit/all-elements-equal star u.2)

Equiv/Sg-base-unit (A : U) : Equiv (Σ A (λ_. Unit)) A =
  has-inverse/Equiv (Σ A (λ_. Unit)) A (Equiv/Sg-base-unit-map A)
    (Equiv/Sg-base-unit-inv-map A, (Equiv/Sg-base-unit-right-htpy A, Equiv/Sg-base-unit-left-htpy A))

1.8.11 Σ (Σ A B) (C ˆ pr1) is Σ (Σ A C) (B ˆ pr1)

Forward map. 

Equiv/assoc-Sg/map (A : U) (B C : A → U) : Σ (Σ A B) (λt. C t.1) → Σ (Σ A C) (λt. B t.1) =
  λu. ((u.1.1, u.2), u.1.2)

Inverse map. 

Equiv/assoc-Sg/inv-map (A : U) (B C : A → U) : Σ (Σ A C) (λt. B t.1) → Σ (Σ A B) (λt. C t.1) =
  λu. ((u.1.1, u.2), u.1.2)

Right homotopy. 

Equiv/assoc-Sg/right-htpy/sg (A : U) (B C : A → U) (a : A) (b : B a) (c : C a)
                                : Path (Σ (Σ A C) (λt. B t.1)) (Equiv/assoc-Sg/map A B C (Equiv/assoc-Sg/inv-map A B C ((a, c), b))) ((a, c), b) =
  refl (Σ (Σ A C) (λt. B t.1)) ((a, c), b)

Equiv/assoc-Sg/right-htpy (A : U) (B C : A → U) : Htpy' (Σ (Σ A C) (λt. B t.1)) (Σ (Σ A C) (λt. B t.1))
                                                        (λt. Equiv/assoc-Sg/map A B C (Equiv/assoc-Sg/inv-map A B C t)) (id (Σ (Σ A C) (λt. B t.1))) =
  λt. Equiv/assoc-Sg/right-htpy/sg A B C t.1.1 t.2 t.1.2

Left homotopy. 

Equiv/assoc-Sg/left-htpy/sg (A : U) (B C : A → U) (a : A) (b : B a) (c : C a)
                                : Path (Σ (Σ A B) (λt. C t.1)) (Equiv/assoc-Sg/inv-map A B C (Equiv/assoc-Sg/map A B C ((a, b), c))) ((a, b), c) =
  refl (Σ (Σ A B) (λt. C t.1)) ((a, b), c)

Equiv/assoc-Sg/left-htpy (A : U) (B C : A → U) : Htpy' (Σ (Σ A B) (λt. C t.1)) (Σ (Σ A B) (λt. C t.1))
                                                       (λt. Equiv/assoc-Sg/inv-map A B C (Equiv/assoc-Sg/map A B C t)) (id (Σ (Σ A B) (λt. C t.1))) =
  λt. Equiv/assoc-Sg/left-htpy/sg A B C t.1.1 t.1.2 t.2

Thus, it is an equivalence. 

Equiv/assoc-Σ (A : U) (B C : A → U) : Equiv (Σ (Σ A B) (λt. C t.1)) (Σ (Σ A C) (λt. B t.1)) =
  has-inverse/Equiv (Σ (Σ A B) (λt. C t.1)) (Σ (Σ A C) (λt. B t.1))
    (Equiv/assoc-Sg/map A B C) (Equiv/assoc-Sg/inv-map A B C, (Equiv/assoc-Sg/right-htpy A B C, Equiv/assoc-Sg/left-htpy A B C))

1.8.12 Σ (x: A) (Σ (y: B) (C x y)) and Σ (Σ A B) C(x, y)

Maps: 

Equiv/associative-Sg/map (A : U) (B : A → U) (C : (x : A) → B x → U) :
  Σ A (λx. Σ (B x) (λy. C x y)) → Σ (Σ A B) (λt. C t.1 t.2) =
  λt. ((t.1, t.2.1), t.2.2)

Equiv/associative-Sg/inv-map (A : U) (B : A → U) (C :  (x : A) → B x → U) :
  Σ (Σ A B) (λt. C t.1 t.2) → Σ A (λx. Σ (B x) (λy. C x y)) =
  λt. (t.1.1, (t.1.2, t.2))

Homotopies: 

Equiv/associative-Sg/right-htpy (A : U) (B : A → U) (C : (x : A) → B x → U) (t : Σ (Σ A B) (λt. C t.1 t.2))
  : Path (Σ (Σ A B) (λu. C u.1 u.2)) (Equiv/associative-Sg/map A B C (Equiv/associative-Sg/inv-map A B C t)) t =
  refl (Σ (Σ A B) (λu. C u.1 u.2)) t

Equiv/associative-Sg/left-htpy (A : U) (B : A → U) (C : (x : A) → B x → U) (t : Σ A (λx. Σ (B x) (λy. C x y)))
  : Path (Σ A (λx. Σ (B x) (λy. C x y))) (Equiv/associative-Sg/inv-map A B C (Equiv/associative-Sg/map A B C t)) t =
  refl (Σ A (λx. Σ (B x) (λy. C x y))) t

Result: 

BiInv/associative-Σ (A : U) (B : A → U) (C : (x : A) → B x → U)
  : BiInv (Σ A (λx. Σ (B x) (λy. C x y))) (Σ (Σ A B) (λt. C t.1 t.2)) =
  has-inverse/BiInv
    ( Σ A (λx. Σ (B x) (λy. C x y)))
    ( Σ (Σ A B) (λt. C t.1 t.2))
    ( Equiv/associative-Sg/map A B C)
    ( Equiv/associative-Sg/inv-map A B C,
      ( Equiv/associative-Sg/right-htpy A B C,
        Equiv/associative-Sg/left-htpy A B C))

BiInv/associative-Sg' (A : U) (B : A → U) (C : (x : A) → B x → U)
  : BiInv (Σ (Σ A B) (λt. C t.1 t.2)) (Σ A (λx. Σ (B x) (λy. C x y))) =
  BiInv/sym
    ( Σ A (λx. Σ (B x) (λy. C x y)))
    ( Σ (Σ A B) (λt. C t.1 t.2))
    ( BiInv/associative-Σ A B C)


Equiv/associative-Σ (A : U) (B : A → U) (C : (x : A) → B x → U)
  : Equiv (Σ A (λx. Σ (B x) (λy. C x y))) (Σ (Σ A B) (λt. C t.1 t.2)) =
  BiInv/Equiv
    ( Σ A (λx. Σ (B x) (λy. C x y)))
    ( Σ (Σ A B) (λt. C t.1 t.2))
    ( BiInv/associative-Σ A B C)

Equiv/associative-Sg' (A : U) (B : A → U) (C : (x : A) → B x → U)
  : Equiv (Σ (Σ A B) (λt. C t.1 t.2)) (Σ A (λx. Σ (B x) (λy. C x y))) =
  BiInv/Equiv
    ( Σ (Σ A B) (λt. C t.1 t.2))
    ( Σ A (λx. Σ (B x) (λy. C x y)))
    ( BiInv/associative-Sg' A B C)

1.8.13 Σ A (Σ B (C x y)) ≃ Σ B (Σ A (C x y))

The same result but where B is not a family of types over A. 

Equiv/assoc-non-dep-Sg/map (A B : U) (C : A → B → U) (t : Σ A (λx. Σ B (C x))) : Σ B (λy. Σ A (λx. C x y)) =
  (t.2.1, (t.1, t.2.2))

Equiv/assoc-non-dep-Sg/inv-map (A B : U) (C : A → B → U) (t : Σ B (λy. Σ A (λx. C x y))) : Σ A (λx. Σ B (C x)) =
  (t.2.1, (t.1, t.2.2))

Equiv/assoc-non-dep-Σ (A B : U) (C : A → B → U) : Equiv (Σ A (λx. Σ B (C x))) (Σ B (λy. Σ A (λx. C x y))) =
  has-inverse/Equiv
    ( Σ A (λx. Σ B (C x)))
    ( Σ B (λy. Σ A (λx. C x y)))
    ( Equiv/assoc-non-dep-Sg/map A B C)
    ( Equiv/assoc-non-dep-Sg/inv-map A B C,
      ( λt. refl (Σ B (λy. Σ A (λx. C x y))) t,
        λt. refl (Σ A (λx. Σ B (C x))) t))

Equiv/assoc-non-dep-Sg' (A B : U) (C : A → B → U) : Equiv (Σ B (λy. Σ A (λx. C x y))) (Σ A (λx. Σ B (C x))) =
  has-inverse/Equiv
    ( Σ B (λy. Σ A (λx. C x y)))
    ( Σ A (λx. Σ B (C x)))
    ( Equiv/assoc-non-dep-Sg/inv-map A B C)
    ( Equiv/assoc-non-dep-Sg/map A B C,
      ( λt. refl (Σ A (λx. Σ B (C x))) t,
        λt. refl (Σ B (λy. Σ A (λx. C x y))) t))

1.8.14 Σ A B and Σ A C whenever B is equivalent to C

Equiv/Sg-fam/map' (A : U) (B C : A → U) (f : (x : A) → (B x) → (C x)) : Σ A B → Σ A C =
  λt. (t.1, (f t.1) t.2)

Equiv/Sg-fam/map (A : U) (B C : A → U) (e : (x : A) → Equiv (B x) (C x)) : Σ A B → Σ A C =
  λt. Equiv/Sg-fam/map' A B C (λx. Equiv/map (B x) (C x) (e x)) t

Equiv/Sg-fam/inv-map (A : U) (B C : A → U) (e : (x : A) → Equiv (B x) (C x)) : Σ A C → Σ A B =
  λt. (t.1, Equiv/inv-map (B t.1) (C t.1) (e t.1) t.2)

Equiv/Sg-fam/right-htpy/sg (A : U) (B C : A → U) (e : (x : A) → Equiv (B x) (C x)) (a : A) (c : C a)
                              : Path (Σ A C) (Equiv/Sg-fam/map A B C e (Equiv/Sg-fam/inv-map A B C e (a, c))) (a, c) =
  SgPathO→PathΣ A C
    ( Equiv/Sg-fam/map A B C e (Equiv/Sg-fam/inv-map A B C e (a, c))) (a, c)
    ( refl A a,
      PathO/refl A a C
        ( Equiv/map (B a) (C a) (e a) (Equiv/inv-map (B a) (C a) (e a) c)) c
        ( Equiv/inv-right-htpy (B a) (C a) (e a) c))

Equiv/Sg-fam/right-htpy (A : U) (B C : A → U) (e : (x : A) → Equiv (B x) (C x)) (t : Σ A C)
                           : Path (Σ A C) (Equiv/Sg-fam/map A B C e (Equiv/Sg-fam/inv-map A B C e t)) t =
  Equiv/Sg-fam/right-htpy/sg A B C e t.1 t.2

Equiv/Sg-fam/left-htpy/sg (A : U) (B C : A → U) (e : (x : A) → Equiv (B x) (C x)) (a : A) (b : B a)
                             : Path (Σ A B) (Equiv/Sg-fam/inv-map A B C e (Equiv/Sg-fam/map A B C e (a, b))) (a, b) =
  SgPathO→PathΣ A B
    ( Equiv/Sg-fam/inv-map A B C e (Equiv/Sg-fam/map A B C e (a, b))) (a, b)
    ( refl A a,
      PathO/refl A a B
        ( Equiv/inv-map (B a) (C a) (e a) (Equiv/map (B a) (C a) (e a) b)) b
        ( Equiv/inv-left-htpy (B a) (C a) (e a) b))

Equiv/Sg-fam/left-htpy (A : U) (B C : A → U) (e : (x : A) → Equiv (B x) (C x)) (t : Σ A B)
                          : Path (Σ A B) (Equiv/Sg-fam/inv-map A B C e (Equiv/Sg-fam/map A B C e t)) t =
  Equiv/Sg-fam/left-htpy/sg A B C e t.1 t.2

is-equiv/Sg-fam (A : U) (B C : A → U) (e : (x : A) → Equiv (B x) (C x)) : is-equiv (Σ A B) (Σ A C) (Equiv/Sg-fam/map A B C e) =
  has-inverse/is-equiv
    ( Σ A B)
    ( Σ A C)
    ( Equiv/Sg-fam/map A B C e)
    ( Equiv/Sg-fam/inv-map A B C e,
      ( Equiv/Sg-fam/right-htpy A B C e,
        Equiv/Sg-fam/left-htpy A B C e))

Equiv/Sg-fam (A : U) (B C : A → U) (e : (x : A) → Equiv (B x) (C x)) : Equiv (Σ A B) (Σ A C) =
  ( Equiv/Sg-fam/map A B C e,
    is-equiv/Sg-fam A B C e)

1.8.15 Σ A B is A if B is contractible

Because if B is contractible, B ≃ Unit, and by previous results: Σ(x:A)Unit ≃ A. The result is in the file Lib/Prop/Proposition.

1.8.16 A × B and A' × B

If A is equivalent to C and B is equivalent to D, then A × B is equivalent to C × D. 

Equiv/prod/map (A A' B : U) (e : Equiv A A') : (A * B) → (A' * B) =
  λt. (Equiv/map A A' e t.1, t.2)

Equiv/prod/inv-map (A A' B : U) (e : Equiv A A') : (A' * B) → (A * B) =
  λt. (Equiv/inv-map A A' e t.1, t.2)

Equiv/prod/right-htpy/sg (A A' B : U) (e : Equiv A A') (x : A') (y : B)
                              : Path (A' * B) (Equiv/prod/map A A' B e (Equiv/prod/inv-map A A' B e (x, y))) (x, y) =
  Eq-prod/eq A' B
    ( Equiv/prod/map A A' B e (Equiv/prod/inv-map A A' B e (x, y)))
    ( x, y)
    ( Equiv/inv-right-htpy A A' e x,
      refl B y)

Equiv/prod/right-htpy (A A' B : U) (e : Equiv A A') (t : A' * B)
                              : Path (A' * B) (Equiv/prod/map A A' B e (Equiv/prod/inv-map A A' B e t)) t =
  Equiv/prod/right-htpy/sg A A' B e t.1 t.2

Equiv/prod/left-htpy/sg (A A' B : U) (e : Equiv A A') (x : A) (y : B)
                                : Path (A * B) (Equiv/prod/inv-map A A' B e (Equiv/prod/map A A' B e (x, y))) (x, y) =
  Eq-prod/eq A B
    ( Equiv/prod/inv-map A A' B e (Equiv/prod/map A A' B e (x, y)))
    ( x, y)
    ( Equiv/inv-left-htpy A A' e x,
      refl B y)

Equiv/prod/left-htpy (A A' B : U) (e : Equiv A A') (t : A * B)
                             : Path (A * B) (Equiv/prod/inv-map A A' B e (Equiv/prod/map A A' B e t)) t =
  Equiv/prod/left-htpy/sg A A' B e t.1 t.2

Equiv/prod/is-equiv (A A' B : U) (e : Equiv A A') : is-equiv (A * B) (A' * B) (Equiv/prod/map A A' B e) =
  has-inverse/is-equiv
    ( A * B)
    ( A' * B)
    ( Equiv/prod/map A A' B e)
    ( Equiv/prod/inv-map A A' B e,
      ( Equiv/prod/right-htpy A A' B e,
        Equiv/prod/left-htpy A A' B e))

Equiv/prod (A A' B : U) (e : Equiv A A') : Equiv (A * B) (A' * B) =
  ( Equiv/prod/map A A' B e,
    Equiv/prod/is-equiv A A' B e)

1.8.17 A × B and A × B'

If A is equivalent to C and B is equivalent to D, then A × B is equivalent to C × D. 

Equiv/prod'/map (A B B' : U) (e : Equiv B B') : (A * B) → (A * B') =
  λt. (t.1, Equiv/map B B' e t.2)

Equiv/prod'/inv-map (A B B' : U) (e : Equiv B B') : (A * B') → (A * B) =
  λt. (t.1, Equiv/inv-map B B' e t.2)

Equiv/prod'/right-htpy/sg (A B B' : U) (e : Equiv B B') (x : A) (y : B')
                               : Path (A * B') (Equiv/prod'/map A B B' e (Equiv/prod'/inv-map A B B' e (x, y))) (x, y) =
  Eq-prod/eq A B'
    ( Equiv/prod'/map A B B' e (Equiv/prod'/inv-map A B B' e (x, y)))
    ( x, y)
    ( refl A x,
      Equiv/inv-right-htpy B B' e y)

Equiv/prod'/right-htpy (A B B' : U) (e : Equiv B B') (t : A * B')
                               : Path (A * B') (Equiv/prod'/map A B B' e (Equiv/prod'/inv-map A B B' e t)) t =
  Equiv/prod'/right-htpy/sg A B B' e t.1 t.2

Equiv/prod'/left-htpy/sg (A B B' : U) (e : Equiv B B') (x : A) (y : B)
                                : Path (A * B) (Equiv/prod'/inv-map A B B' e (Equiv/prod'/map A B B' e (x, y))) (x, y) =
  Eq-prod/eq A B
    ( Equiv/prod'/inv-map A B B' e (Equiv/prod'/map A B B' e (x, y)))
    ( x, y)
    ( refl A x,
      Equiv/inv-left-htpy B B' e y)

Equiv/prod'/left-htpy (A B B' : U) (e : Equiv B B') (t : A * B)
                              : Path (A * B) (Equiv/prod'/inv-map A B B' e (Equiv/prod'/map A B B' e t)) t =
  Equiv/prod'/left-htpy/sg A B B' e t.1 t.2

Equiv/prod'/is-equiv (A B B' : U) (e : Equiv B B') : is-equiv (A * B) (A * B') (Equiv/prod'/map A B B' e) =
  has-inverse/is-equiv
    ( A * B)
    ( A * B')
    ( Equiv/prod'/map A B B' e)
    ( Equiv/prod'/inv-map A B B' e,
      ( Equiv/prod'/right-htpy A B B' e,
        Equiv/prod'/left-htpy A B B' e))

Equiv/prod' (A B B' : U) (e : Equiv B B') : Equiv (A * B) (A * B') =
  ( Equiv/prod'/map A B B' e,
    Equiv/prod'/is-equiv A B B' e)

1.8.18 A × B and A' × B'a

Equiv/double-prod (A B A' B' : U) (eA : Equiv A A') (eB : Equiv B B') : Equiv (A * B) (A' * B') =
  Equiv/trans
    ( A * B)
    ( A' * B)
    ( A' * B')
    ( Equiv/prod A A' B eA)
    ( Equiv/prod' A' B B' eB)

1.8.19 Πx:AB x and Πx: A'B(e(x)) whenever A is equivalent to A'

Equiv/dependent/map (A B : U) (P : B → U) (e : Equiv A B) : ((y : B) → P y) → (x : A) → P (Equiv/map A B e x) =
  λh x. h (Equiv/map A B e x)

Equiv/dependent/inv-map (A B : U) (P : B → U) (e : Equiv A B) : ((x : A) → P (Equiv/map A B e x)) → (y : B) → P y =
  λh y. tr B
    ( Equiv/map A B e (Equiv/inv-map A B e y)) y
    ( htpy/half-adjoint/htpy A B
      ( Equiv/map A B e)
      ( Equiv/inv-map A B e)
      ( Equiv/inv-right-htpy A B e)
      ( Equiv/inv-left-htpy A B e) y) P
    ( h (Equiv/inv-map A B e y))

Equiv/dependent/right-htpy (A B : U) (P : B → U) (e : Equiv A B) (h : (x : A) → P (Equiv/map A B e x)) 
                                : Path ((x : A) → P (Equiv/map A B e x))
                                       (Equiv/dependent/map A B P e (Equiv/dependent/inv-map A B P e h)) h =
  let f : A → B = Equiv/map A B e
      g : B → A = Equiv/inv-map A B e
      G : Htpy' B B (λx. f (g x)) (id B) = Equiv/inv-right-htpy A B e
      H : Htpy' A A (λx. g (f x)) (id A) = Equiv/inv-left-htpy A B e
      G' : Htpy' B B (λy. f (g y)) (id B) = htpy/half-adjoint/htpy A B f g G H
  in
  eq-htpy A
    ( λx. P (f x))
    ( Equiv/dependent/map A B P e (Equiv/dependent/inv-map A B P e h)) h
    ( λx. comp-n 
        ( P (f x)) three-Nat
        ( tr B (f (g (f x))) (f x) (G' (f x)) P (h (g (f x))))
        ( tr B (f (g (f x))) (f x) (ap A B f (g (f x)) x (H x)) P (h (g (f x))))
        ( ap (Path B (f (g (f x))) (f x)) (P (f x)) (λp. tr B (f (g (f x))) (f x) p P (h (g (f x)))) (G' (f x)) (ap A B f (g (f x)) x (H x))
          ( htpy/half-adjoint' A B f g G H x))
        ( tr A (g (f x)) x (H x) (λz. P (f z)) (h (g (f x))))
        ( tr/ap A B f P (g (f x)) x (H x) (h (g (f x))))
        ( h x)
        ( apd A
          ( λz. P (f z)) h
          ( g (f x)) x
          ( H x)))

Equiv/dependent/left-htpy (A B : U) (P : B → U) (e : Equiv A B) (h : (y : B) → P y)
                                 : Path ((y : B) → P y)
                                        (Equiv/dependent/inv-map A B P e (Equiv/dependent/map A B P e h)) h =
  let f : A → B = Equiv/map A B e
      g : B → A = Equiv/inv-map A B e
      G : Htpy' B B (λx. f (g x)) (id B) = Equiv/inv-right-htpy A B e
      H : Htpy' A A (λx. g (f x)) (id A) = Equiv/inv-left-htpy A B e
      G' : Htpy' B B (λy. f (g y)) (id B) = htpy/half-adjoint/htpy A B f g G H
  in
  eq-htpy B P
    ( Equiv/dependent/inv-map A B P e (Equiv/dependent/map A B P e h)) h
    ( λy. apd B P h
          ( f (g y)) y
          ( G' y))

Equiv/dependent (A B : U) (P : B → U) (e : Equiv A B)
                     : Equiv ((y : B) → P y) ((x : A) → P (Equiv/map A B e x)) =
  has-inverse/Equiv
    ( (y : B) → P y)
    ( (x : A) → P (Equiv/map A B e x))
    ( Equiv/dependent/map A B P e)
    ( Equiv/dependent/inv-map A B P e,
      ( Equiv/dependent/right-htpy A B P e,
        Equiv/dependent/left-htpy A B P e))

1.8.20 Πx: UnitB x and B star

Equiv/pi-Unit/map (B : Unit → U) : ((u : Unit) → B u) → B star =
  λf. f star

Equiv/pi-Unit/inv-map (B : Unit → U) (b : B star) : (u : Unit) → B u = split
  star → b

Equiv/pi-Unit/right-htpy (B : Unit → U) (b : B star) : Path (B star) (Equiv/pi-Unit/map B (Equiv/pi-Unit/inv-map B b)) b =
  refl (B star) b

Equiv/pi-Unit/left-htpy/star (B : Unit → U) (f : (u : Unit) → B u) : (u : Unit) → Path (B u) (Equiv/pi-Unit/inv-map B (Equiv/pi-Unit/map B f) u) (f u) = split
  star → refl (B star) (f star)

Equiv/pi-Unit/left-htpy (B : Unit → U) (f : (u : Unit) → B u) : Path ((u : Unit) → B u) (Equiv/pi-Unit/inv-map B (Equiv/pi-Unit/map B f)) f =
  eq-htpy Unit B
    ( Equiv/pi-Unit/inv-map B (Equiv/pi-Unit/map B f)) f
    ( Equiv/pi-Unit/left-htpy/star B f)

Equiv/pi-Unit/is-equiv (B : Unit → U) : is-equiv ((u : Unit) → B u) (B star) (Equiv/pi-Unit/map B) =
  has-inverse/is-equiv
    ( (u : Unit) → B u)
    ( B star)
    ( Equiv/pi-Unit/map B)
    ( Equiv/pi-Unit/inv-map B,
      ( Equiv/pi-Unit/right-htpy B,
        Equiv/pi-Unit/left-htpy B))

Equiv/pi-Unit (B : Unit → U) : Equiv ((u : Unit) → B u) (B star) =
  ( Equiv/pi-Unit/map B,
    Equiv/pi-Unit/is-equiv B)

1.8.21 (x, y) = (x', y') is Σp: x = x'trB(p, y) = y'

This result is more or less direct from the one in the prelude. 

PathSg/Equiv (A : U) (B : A → U) (u v : Σ A B) : Equiv (Path (Σ A B) u v) (SgPathO A B u v) =
  path-to-equiv
    ( Path (Σ A B) u v)
    ( SgPathO A B u v)
    ( PathSg-eq-SgPathO A B u v)

PathSg/Equiv' (A : U) (B : A → U) (u v : Σ A B) : Equiv (SgPathO A B u v) (Path (Σ A B) u v) =
  Equiv/sym
    ( Path (Σ A B) u v)
    ( SgPathO A B u v)
    ( PathSg/Equiv A B u v)

1.8.22 (x, y) = (x', y') is x = x' if the type of y, y' is proposition

See the file Levels.org.

1.8.23 Σ A B is (B a) whenever A is contractible

We define the function fiber-inclusion that will be useful later on. 

fiber-inclusion (A : U) (B : A → U) (a : A) : B a → Σ A B =
  λb. (a, b)

The inverse map can be defined using a transport. 

Equiv/is-contr-total-space/inv-map (A : U) (B : A → U) (H : is-contr A) (a : A) (t : Σ A B) : B a =
  tr A t.1 a
    ( is-contr/all-elements-equal A H t.1 a) B t.2

We show that these maps are inverse to each other. 

Equiv/is-contr-total-space/right-htpy (A : U) (B : A → U) (H : is-contr A) (a : A) (t : Σ A B)
  : Path (Σ A B) (fiber-inclusion A B a (Equiv/is-contr-total-space/inv-map A B H a t)) t =
  let p : Path A t.1 a = is-contr/all-elements-equal A H t.1 a
      q : Path A a t.1 = inv A t.1 a p in
  SgPathO→PathΣ A B
    ( fiber-inclusion A B a (Equiv/is-contr-total-space/inv-map A B H a t)) t
    ( q,
      tr/left-inv A B t
      ( fiber-inclusion A B a (Equiv/is-contr-total-space/inv-map A B H a t)) p)

Equiv/is-contr-total-space/left-htpy (A : U) (B : A → U) (H : is-contr A) (a : A) (b : B a)
  : Path (B a) (Equiv/is-contr-total-space/inv-map A B H a (fiber-inclusion A B a b)) b =
  comp
    ( B a)
    ( tr A a a (is-contr/all-elements-equal A H a a) B b)
    ( tr A a a (refl A a) B b)
    ( ap (Path A a a) (B a) (λp. tr A a a p B b) (is-contr/all-elements-equal A H a a)
         (refl A a) (comp/inv-l A (center A H) a (contraction A H a)))
    b ( tr/refl-path A a B b)

Hence, B a is equivalent to Σ A B. 

Equiv/is-contr-total-space (A : U) (B : A → U) (H : is-contr A) (a : A)
                              : Equiv (B a) (Σ A B) =
  has-inverse/Equiv
    ( B a)
    ( Σ A B)
    ( fiber-inclusion A B a)
    ( Equiv/is-contr-total-space/inv-map A B H a,
      ( Equiv/is-contr-total-space/right-htpy A B H a,
        Equiv/is-contr-total-space/left-htpy A B H a))

Equiv/is-contr-total-space' (A : U) (B : A → U) (H : is-contr A) (a : A)
                               : Equiv (Σ A B) (B a) =
  has-inverse/Equiv
    ( Σ A B)
    ( B a)
    ( Equiv/is-contr-total-space/inv-map A B H a)
    ( fiber-inclusion A B a,
      ( Equiv/is-contr-total-space/left-htpy A B H a,
        Equiv/is-contr-total-space/right-htpy A B H a))

1.8.24 Σ(z: B(x))(x, y) = (a, z) ≃ x = a

See the result in the file Lib/Prop/Proposition as it needs that Σ A B ≃ A whenever B is contractible.

1.9 Closure of truncation levels under equivalence

If B is of level k and A is equivalent to B, then A is also of level k. 

is-of-lvl/closed-equiv (A B : U) (e : Equiv A B) : (k : Nat) → (H : is-of-lvl k B) → is-of-lvl k A = split
  zero → λH. is-contr/is-contr-equiv A B e H
  suc k →
    let f : A → B = Equiv/map A B e in
    λH x y. is-of-lvl/closed-equiv (Path A x y) (Path B (f x) (f y)) (Equiv/Equiv-id A B e x y) k (H (f x) (f y))

is-of-lvl/closed-equiv' (A B : U) (e : Equiv A B) (k : Nat) (H : is-of-lvl k A) : is-of-lvl k B =
  is-of-lvl/closed-equiv B A (Equiv/sym A B e) k H

1.10 Double inverse of equivalence

lock has-inverse/is-equiv

Equiv/sym/sym (A B : U) (e : Equiv A B)
                   : Path (Equiv A B) (Equiv/inv-equiv B A (Equiv/inv-equiv A B e)) e =
  SgPath-prop
    ( A → B)
    ( is-equiv A B)
    ( is-equiv/is-prop A B)
    ( Equiv/inv-equiv B A (Equiv/inv-equiv A B e)) e
    ( eq-htpy' A B
        ( Equiv/map A B
          ( Equiv/inv-equiv B A
            ( Equiv/inv-equiv A B e)))
        ( Equiv/map A B e)
        ( λx.
            let e' : Equiv B A = Equiv/inv-equiv A B e
                e'' : Equiv A B = Equiv/inv-equiv B A e'
                f : A → B = Equiv/map A B e
                f' : B → A = Equiv/map B A e'
                f'' : A → B = Equiv/map A B e''
            in
            comp B
              ( f'' x)
              ( f'' (f' (f x)))
              ( ap A B f'' x
                ( f' (f x))
                ( inv A
                  ( f' (f x)) x
                  ( Equiv/inv-left-htpy A B e x)))
              ( f x)
              ( Equiv/inv-left-htpy B A e' (f x))))


Equiv/sym/sym' (A B : U) (e : Equiv A B)
                   : Path (Equiv A B) e (Equiv/inv-equiv B A (Equiv/inv-equiv A B e)) =
  inv
    ( Equiv A B)
    ( Equiv/inv-equiv B A
      ( Equiv/inv-equiv A B e)) e
    ( Equiv/sym/sym A B e)

unlock has-inverse/is-equiv

Author: Johann Rosain

Created: 2024-07-23 Tue 13:51

Validate