UniAgda.Core.Equivalences

Table of Contents

1 Prelude

2 Quasi-inverses

2.1 Definition

A quasi-inverse is what we would call an isomorphism if we were dealing with sets. It is a map with another map that is a left and right inverse.

qinv :  {i j} {A : Type i} {B : Type j}
       (f : A  B)
        Type (i  j)
qinv {A = A} {B = B} f = Σ[ g  (B  A)] (((f o g) ~ id) × ((g o f) ~ id))

A quasi-equivalence between two types is then a map with a proof that it is a quasi-inverse.

qequiv :  {i j}
         (A : Type i) (B : Type j)
          Type (i  j)
qequiv A B = Σ[ f  (A  B) ] (qinv f)
_q≃_ = qequiv
infix 6 _q≃_

3 Half adjoint equivalences

3.1 Definition

Half adjoint equivalences will be our candidate for equivalences.

isHae :  {i j} {A : Type i} {B : Type j}
        (f : A  B)
         Type (i  j)
isHae {A = A} {B = B} f = Σ[ g  (B  A) ] (Σ[ η  (g o f ~ id) ] (Σ[ ε  (f o g ~ id) ] ((x : A)  ap f (η x)  ε (f x))))

isEquiv = isHae

equiv :  {i j}
        (A : Type i) (B : Type j)
         Type (i  j)
equiv A B = Σ[ f  (A  B) ] (isEquiv f)
_≃_ = equiv
infix 31 _≃_

We also define the following which will be useful when proving relations between the different types of equivalence.

linv :  {i j} {A : Type i} {B : Type j}
       (f : A  B)
        Type (i  j)
linv {_} {_} {A} {B} f = Σ[ g  (B  A) ] (g o f ~ id)

rinv :  {i j} {A : Type i} {B : Type j}
       (f : A  B)
        Type (i  j)
rinv {_} {_} {A} {B} f = Σ[ g  (B  A) ] (f o g ~ id)
lcoh :  {i j} {A : Type i} {B : Type j}
       (f : A  B) (X : linv f)
        Type (i  j)
lcoh {i} {j} {A} {B} f (g , η) = Σ[ ε  (f o g ~ id) ] ((y : B)  ap g (ε y)  η (g y))

rcoh :  {i j} {A : Type i} {B : Type j}
       (f : A  B) (Y : rinv f)
        Type (i  j)
rcoh {i} {j} {A} {B} f (g , ε) = Σ[ η  (g o f ~ id) ] ((x : A)  ap f (η x)  ε (f x))

4 Bi-invertible maps

A bi-invertible map is one with both a left and right inverse.

isBiinv :  {i j} {A : Type i} {B : Type j}
        (f : A  B)
         Type (i  j)
isBiinv f = linv f × rinv f


biequiv :  {i j}
          (A : Type i) (B : Type j)
           Type (i  j)
biequiv A B = Σ[ f  (A  B) ] (isBiinv f)
_bi≃_ = biequiv
infix 6 _bi≃_

5 Contractible fibres

5.1 Definition

We first need to define the fibre of a map and a point.

fibre :  {i j} {A : Type i} {B : Type j}
        (f : A  B) (y : B)
         Type (i  j)
fibre {A = A} f y = Σ[ x  A ] (f x  y)
fib = fibre

We say that a map is contractible when all of its fibres are contractible.

isContrmap : {i j : Level} {A : Type i} {B : Type j}
           (f : A  B)  Type (i  j)
isContrmap {_} {_} {A} {B} f = (y : B)  isContr (fib f y)

5.2 Relation to isEquiv

isContrmap-to-isEquiv : {i j : Level} {A : Type i} {B : Type j} {f : A  B}
                    isContrmap f
                    isHae f
isContrmap-to-isEquiv {_} {_} {A} {B} {f} P = let g =  y  pr₁ (pr₁ (P y)))
                                                  ε =  y  pr₂ (pr₁ (P y)))
                                                  τ =  x  (pr₂ (P (f x)) (g(f(x)) , ε (f x))) ^  (pr₂ (P (f x)) (x , refl)))
                                              in isequiv-adjointify (g , ε ,  λ x  ap pr₁ (τ x))

More will be proven about this later, in another section. We need results about contractible types to do this.

6 Useful results

We can take an equivalence, a term of the first type then construct a term of the second.

e-ap :  {i j} {A : Type i} {B : Type j}
       A  B  A
       B
e-ap X a = pr₁ X a

We want to be able to compare elements of equivalent types. This doesn't really make sense on the nose though, so the following is the closest that we have.

equiv-types-eq :  {i j} {A : Type i} {B : Type j}
        {x y : B} (F : A  B)
         pr₁ (pr₂ F) x  pr₁ (pr₂ F) y  x  y
equiv-types-eq {x = x} {y = y} (f , g , η , ε , τ) p = ε x ^  (ap f p)  ε y

Another useful result is that if we know two types are equivalent, then \(\Pi\) and \(\Sigma\) types over one of the equivalent types are logically equivalent, in the following sense:

equiv-base-Pi :  {i j k} {A : Type i} {A' : Type j} {B : A  Type k}
      (F : A  A')
       ((x : A')  B o (pr₁ (pr₂ F)) $ x)  ((x : A)  B x)
equiv-base-Pi {B = B} (f , g , α , β , γ) Q a = transport B (α a) (Q (f a))

equiv-base-Sigma :  {i j k} {A : Type i} {A' : Type j} {B : A  Type k}
                   (F : A  A')
                    (Σ[ x'  A' ] (B o pr₁ (pr₂ F) $ x'))  (Σ[ x  A ] B x)
equiv-base-Sigma (f , g , α , β , γ) (a' , b') = g a' , b'

Note that with univalence, these types are equivalent (I don't know if we need univalence for this, but logical equivalence is sufficient for our needs).

A result we expect is for the type of paths \(a = b\) to be equivalent to the type of paths \(b = a\).

a=b≃b=a :  {i} {A : Type i} {a b : A}
           (a  b)  (b  a)
a=b≃b=a = equiv-adjointify
  ((λ { refl  refl}) ,
   { refl  refl}) ,
   { refl  refl}) ,
  λ { refl  refl})

Author: James Leslie

Created: 2021-03-27 Sat 10:47