UniAgda.Core.PathSpaces.Identity

Table of Contents

1 Prelude

2 Paths in Identity Types

private
  lemma₁ : {i j : Level} {A : Type i} {B : Type j} (f : A  B) (g : B  A) (α : f o g ~ id) (a a' : A) (p : a  a')
            ap f p  ((whisker-r α f a ^)  (ap f (ap (g o f) p)))  whisker-r α f a'
  lemma₁ f g α a .a refl = p=qr^-to-pr=q (whisker-r α f a ^  refl) refl (whisker-r α f a) (p-refl (α (f a) ^)) ^

  lemma₂ : {i j : Level} {A : Type i} {B : Type j} (f : A  B) (g : B  A) (β : g o f ~ id) (a a' : A) (p : a  a')
            ap (g o f) p  β a  p  β a' ^
  lemma₂ f g β a .a refl = pp^ (β a) ^

  lemma₄ : {i j : Level} {A : Type i} {B : Type j} (f : A  B) (g : B  A) (α : f o g ~ id) (β : g o f ~ id) (a a' : A) (p : a  a')
            ((whisker-r α f a ^)  (ap f (ap (g o f) p)))  whisker-r α f a'  ((whisker-r α f a ^)  (ap f (β a  p  β a' ^)))  whisker-r α f a'
  lemma₄ f g α β a .a refl = p=q-to-pr=qr (p=q-to-rp=rq (transport  t  refl  ap f (t)) ((pp^ (β a)) ^) refl) (α (f a) ^) ) (whisker-r α f a)

  lemma₅a : {i : Level} {A : Type i} {x y z w : A}
             (p : x  y) (r : x  z) (s : z  w)
             p  (p ^  r  s)  s ^  r
  lemma₅a refl refl refl = refl


  lemma₅ : {i j : Level} {A : Type i} {B : Type j} (f : A  B) (g : B  A) (α : f o g ~ id) (β : g o f ~ id) (a a' : A) (p' : g (f a)  g (f a'))
          ((whisker-r α f a ^)  (ap f (β a  (β a ^  p'  β a')  β a' ^)))  whisker-r α f a'  ((whisker-r α f a ^)  ap f p')  (whisker-r α f a')
  lemma₅ f g α β a a' p' = p=q-to-pr=qr (p=q-to-rp=rq (ap  p  ap f p) (lemma₅a (β a) p' (β a'))) (α (f a) ^)) (whisker-r α f a')

  lemma₆ : {i j : Level} {A : Type i} {B : Type j} (f : A  B) (g : B  A) (α : f o g ~ id) (a a' : A) (q : f a  f a')
          ((whisker-r α f a ^)  ap f (ap g q))  (whisker-r α f a')  q
  lemma₆ f g α a a' q = (ass-l (whisker-r α f a ^) (ap f (ap g q)) (whisker-r α f a')  p=qr-to-q^p=r (ap f (ap g q)  whisker-r α f a') (ap id q) (whisker-r α f a) (ap  p  p  whisker-r α f a') ((ap-gf f g q) ^)  (homotopy-natural α q ) ^))  ap-id q

  thm2-11-1-inv : {i j : Level} {A : Type i} {B : Type j} (f : A  B) (g : B  A) (α : f o g ~ id) (β : g o f ~ id) (a a' : A)
                   f a  f a'  a  a'
  thm2-11-1-inv f g α β a a' X = (β a) ^  ap g X  β a'

  thm2-11-1-τ : {i j : Level} {A : Type i} {B : Type j} (f : A  B) (g : B  A) (α : f o g ~ id) (β : g o f ~ id) (a a' : A) (q : f a  f a')
                 ap f (β a ^  ap g q  β a')  q
  thm2-11-1-τ f g α β a a' q = lemma₁ f g α a a' (β a ^  ap g q  β a') 
    lemma₄ f g α β a a' (β a ^  ap g q  β a') 
    lemma₅ f g α β a a' (ap g q) 
    lemma₆ f g α a a' q

  thm2-11-1-ε : {i j : Level} {A : Type i} {B : Type j} (f : A  B) (g : B  A) (β : g o f ~ id) (a a' : A) (p : a  a')
                 β a ^  ap g (ap f p)  β a'  p
  thm2-11-1-ε f g β a .a refl = p^p (β a)
thm2-11-1 : {i j : Level} {A : Type i} {B : Type j} {f : A  B} {a a' : A}
             isEquiv f
             isEquiv  (p : a  a')  ap f p)
thm2-11-1 {i} {j} {A} {B} {f} {a} {a'} X =
  let g = pr₁ X
      β = pr₁ (pr₂ X)
      α = pr₁ (pr₂ (pr₂ X))
  in
  isequiv-adjointify
    (thm2-11-1-inv f g α β a a' ,
    thm2-11-1-τ f g α β a a' ,
    thm2-11-1-ε f g β a a')

3 Other results

Author: James Leslie

Created: 2021-03-27 Sat 10:47