Paths Properties

Table of Contents

1 Paths properties

module Lib.Prop.Paths where

This file contains properties on paths.

1.1 Packages imports

The imported packages can be accessed via the following links: 

import Lib.Data.Map
import Lib.Data.Nat
import Lib.Prop.Comp
import Lib.Prop.Set

1.2 Transport of refl

tr/refl-path (A : U) (x : A) (P : A → U) (u : P x) : Path (P x) (tr A x x (refl A x) P u) u =
  λi. tr/refl A x P i u

tr/refl-path' (A : U) (x : A) (P : A → U) (u : P x) : Path (P x) u (tr A x x (refl A x) P u) =
  inv
    ( P x)
    ( tr A x x (refl A x) P u) u
    ( tr/refl-path A x P u)

It generalizes using J. 

tr/path (A : U) (x y : A) (p : Path A x y) (P : U) (u : P) : Path P (tr A x y p (λ_. P) u) u =
  J A x (λz q. Path P (tr A x z q (λ_. P) u) u) (tr/refl-path A x (λ_. P) u) y p

tr/inv-path (A : U) (x y : A) (p : Path A x y) (P : U) (u : P) : Path P u (tr A x y p (λ_. P) u) =
  inv P (tr A x y p (λ_. P) u) u (tr/path A x y p P u)

1.3 Transport of refl with Σ

PathO/refl (A : U) (x : A) (P : A → U) (u v : P x) (q : Path (P x) u v) : PathO A x x (refl A x) P u v =
  comp (P x) (tr A x x (refl A x) P u) u (tr/refl-path A x P u) v q

1.4 Transport identity

The transportation on inv p then on p is the reflexive transportation. 

tr/right-inv/refl (A : U) (B : A → U) (x : A) (y : B x)
                     :  Path (B x) (tr A x x (refl A x) B (tr A x x (inv A x x (refl A x)) B y)) y =
  comp-n (B x) three-Nat (tr A x x (refl A x) B (tr A x x (inv A x x (refl A x)) B y)) (tr A x x (inv A x x (refl A x)) B y)
    (tr/refl-path A x B (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)

tr/right-inv (A : U) (B : A → U) (u v : Σ A B) (p : Path A u.1 v.1)
                : Path (B v.1) (tr A u.1 v.1 p B (tr A v.1 u.1 (inv A u.1 v.1 p) B v.2)) v.2 =
  J A u.1 (λx q. (y : B x) → Path (B x) (tr A u.1 x q B (tr A x u.1 (inv A u.1 x q) B y)) y)
    (λy. tr/right-inv/refl A B u.1 y) v.1 p v.2

It goes the same for left inverse. 

tr/left-inv/refl (A : U) (B : A → U) (x : A) (y : B x)
                     :  Path (B x) (tr A x x (inv A x x (refl A x)) B (tr A x x (refl A x) B y)) y =
  comp-n (B x) three-Nat (tr A x x (inv A x x (refl A x)) B (tr A x x (refl A x) B y)) (tr A x x (refl A x) B (tr A x x (refl A x) B y))
    (ap (Path A x x) (B x) (λp. (tr A x x p B (tr A x x (refl A x) B y))) (inv A x x (refl A x)) (refl A x)
        (inv/refl A x))
    (tr A x x (refl A x) B y)
    (tr/refl-path A x B (tr A x x (refl A x) B y)) 
    y (tr/refl-path A x B y)

tr/left-inv (A : U) (B : A → U) (u v : Σ A B) (p : Path A u.1 v.1)
               : Path (B u.1) (tr A v.1 u.1 (inv A u.1 v.1 p) B (tr A u.1 v.1 p B u.2)) u.2 =
  J A u.1 (λx q. Path (B u.1) (tr A x u.1 (inv A u.1 x q) B (tr A u.1 x q B u.2)) u.2)
    (tr/left-inv/refl A B u.1 u.2) v.1 p

1.5 inv is involutive

inv/involutive (A : U) (x y : A) (p : Path A x y) : Path (Path A x y) (inv A y x (inv A x y p)) p =
  J A x (λz q. Path (Path A x z) (inv A z x (inv A x z q)) q)
        (comp (Path A x x) (inv A x x (inv A x x (refl A x))) (inv A x x (refl A x))
              (ap (Path A x x) (Path A x x) (λq. inv A x x q) (inv A x x (refl A x)) (refl A x) (inv/refl A x))
              (refl A x) (inv/refl A x)) y p

inv/involutive' (A : U) (x y : A) (p : Path A x y) : Path (Path A x y) p (inv A y x (inv A x y p)) =
  inv (Path A x y) (inv A y x (inv A x y p)) p (inv/involutive A x y p)

1.6 Dependent AP

apd (A : U) (B : A → U) (f : (x : A) → B x) (x y : A) (p : Path A x y) : Path (B y) (tr A x y p B (f x)) (f y) =
  J A x (λz q. Path (B z) (tr A x z q B (f x)) (f z)) (tr/refl-path A x B (f x)) y p

1.7 Identity

ap id is id for paths. 

ap/id (A : U) (x y : A) (p : Path A x y) : Path (Path A x y) p (ap A A (id A) x y p) =
  J A x (λy' q. Path (Path A x y') q (ap A A (id A) x y' q))
        (refl (Path A x x) (refl A x)) y p

ap/id' (A : U) (x y : A) (p : Path A x y) : Path (Path A x y) (ap A A (id A) x y p) p =
  inv (Path A x y) p (ap A A (id A) x y p) (ap/id A x y p)

ap id is also clearly bi-invertible. 

is-bi-inv/ap-id-inv-htpy (A : U) (x y : A) : Htpy' (Path A x y) (Path A x y) (λp. (ap A A (id A) x y) (ap A A (id A) x y p)) (id (Path A x y)) =
  λp. comp (Path A x y) ((ap A A (id A) x y) (ap A A (id A) x y p)) (ap A A (id A) x y p)
                        (ap/id' A x y (ap A A (id A) x y p)) p (ap/id' A x y p)

is-bi-inv/ap-id-is-bi-inv (A : U) (x y : A) : is-bi-inv (Path A x y) (Path A x y) (ap A A (id A) x y) =
  ((ap A A (id A) x y, is-bi-inv/ap-id-inv-htpy A x y), (ap A A (id A) x y, is-bi-inv/ap-id-inv-htpy A x y))

A useful lemma is that tr whatever ap id is also bi-invertible. 

is-bi-inv/ap-eq-id (A : U) (f : A → A) (p : Path (A → A) (id A) f) (x y : A)
                      : is-bi-inv (Path A x y) (Path A (f x) (f y)) (ap A A f x y) =
  tr (A → A) (id A) f p (λh. is-bi-inv (Path A x y) (Path A (h x) (h y)) (ap A A h x y))
    (is-bi-inv/ap-id-is-bi-inv A x y)

1.8 Composition

ap g ˆ ap f is ap (g ˆ f). 

ap/comp (A B C : U) (f : A → B) (g : B → C) (x y : A) (p : Path A x y)
               : Path (Path C (g (f x)) (g (f y))) (ap B C g (f x) (f y) (ap A B f x y p)) (ap A C (map/comp A B C g f) x y p) =
  J A x (λz q. Path (Path C (g (f x)) (g (f z))) (ap B C g (f x) (f z) (ap A B f x z q)) (ap A C (map/comp A B C g f) x z q))
        (refl (Path C (g (f x)) (g (f x))) (refl C (g (f x)))) y p

ap/comp' (A B C : U) (f : A → B) (g : B → C) (x y : A) (p : Path A x y)
               : Path (Path C (g (f x)) (g (f y))) (ap A C (map/comp A B C g f) x y p) (ap B C g (f x) (f y) (ap A B f x y p)) =
  inv (Path C (g (f x)) (g (f y))) (ap B C g (f x) (f y) (ap A B f x y p)) (ap A C (map/comp A B C g f) x y p) (ap/comp A B C f g x y p)

1.9 Inverse

ap f p-1 is (ap f p)-1. 

ap/refl/refl (A B : U) (f : A → B) (x : A) : Path (Path B (f x) (f x)) (ap A B f x x (inv A x x (refl A x)))
                                                                       (ap A B f x x (refl A x)) =
  ap (Path A x x) (Path B (f x) (f x)) (ap A B f x x) (inv A x x (refl A x)) (refl A x) (inv/refl A x)

ap/inv (A B : U) (f : A → B) (x y : A) (p : Path A x y)
            : Path (Path B (f y) (f x)) (ap A B f y x (inv A x y p)) (inv B (f x) (f y) (ap A B f x y p)) =
  J A x (λz q. Path (Path B (f z) (f x)) (ap A B f z x (inv A x z q)) (inv B (f x) (f z) (ap A B f x z q)))
        (comp (Path B (f x) (f x)) (ap A B f x x (inv A x x (refl A x)))
                                   (ap A B f x x (refl A x)) (ap/refl/refl A B f x)
                                   (inv B (f x) (f x) (refl B (f x))) (refl/sym B (f x))) y p

1.10 Path between identifiable functions

ap/eq (A B : U) (f g : A → B) (p : Path (A → B) f g) (x y : A) : Path ((Path A x y) → Path B (g x) (g y)) (tr (A → B) f g p (λh. Path A x y → Path B (h x) (h y)) (ap A B f x y))
                                                                      (ap A B g x y) =
  apd (A → B) (λh. Path A x y → Path B (h x) (h y)) (λh. ap A B h x y) f g p

1.11 Path concatenation

ap f (comp p q) is comp (ap f p) (ap f q). 

ap/concat (A B : U) (f : A → B) (x y z : A) (p : Path A x y) (q : Path A y z)
               : Path (Path B (f x) (f z)) (ap A B f x z (comp A x y p z q))
                                         (comp B (f x) (f y) (ap A B f x y p) (f z) (ap A B f y z q)) =
  J A y (λt r. Path (Path B (f x) (f t)) (ap A B f x t (comp A x y p t r))
                                          (comp B (f x) (f y) (ap A B f x y p) (f t) (ap A B f y t r)))
            (comp (Path B (f x) (f y)) (ap A B f x y (comp A x y p y (refl A y)))
                                       (ap A B f x y p) (ap (Path A x y) (Path B (f x) (f y)) (ap A B f x y) (comp A x y p y (refl A y)) p (comp/ident-r A x y p))
                                       (comp B (f x) (f y) (ap A B f x y p) (f y) (refl B (f y))) (refl/comp-r B (f x) (f y) (ap A B f x y p)))
    z q

1.12 Closure under homotopies

We show that if f ∼ g, then ap f and ap g can be used in further computations, by something called the naturality square. We proceed by path induction and need to use the composition properties of Prelude as the judgmental equality in cubical is different than judgmental equality of HoTT. 

naturality (A B : U) (f g : A → B) (H : Htpy' A B f g) (x y : A) (p : Path A x y)
                : Path (Path B (f x) (g y)) (comp B (f x) (g x) (H x) (g y) (ap A B g x y p))
                                            (comp B (f x) (f y) (ap A B f x y p) (g y) (H y)) =
  J A x (λz q. Path (Path B (f x) (g z)) (comp B (f x) (g x) (H x) (g z) (ap A B g x z q))
                                         (comp B (f x) (f z) (ap A B f x z q) (g z) (H z)))
        (comp (Path B (f x) (g x)) (comp B (f x) (g x) (H x) (g x) (refl B (g x))) (H x)
                                   (comp/ident-r B (f x) (g x) (H x)) (comp B (f x) (f x) (refl B (f x)) (g x) (H x))
                                   (comp/ident-l' B (f x) (g x) (H x))) y p

naturality' (A B : U) (f g : A → B) (H : Htpy' A B f g) (x y : A) (p : Path A x y)
                 : Path (Path B (f x) (g y)) (comp B (f x) (f y) (ap A B f x y p) (g y) (H y))
                                             (comp B (f x) (g x) (H x) (g y) (ap A B g x y p)) =
  inv (Path B (f x) (g y)) (comp B (f x) (g x) (H x) (g y) (ap A B g x y p)) (comp B (f x) (f y) (ap A B f x y p) (g y) (H y))
      (naturality A B f g H x y p)

1.13 Squares

square (A : U) (x y1 y2 z : A) (p-left : Path A x y1) (p-bottom : Path A y1 z) (p-top : Path A x y2) (p-right : Path A y2 z) : U =
  Path (Path A x z)
    ( comp A x y1 p-left z p-bottom)
    ( comp A x y2 p-top z p-right)

square-top (A : U) (x y1 y2 z : A) (p1 : Path A x y1) (q1 : Path A y1 z) (p2 : Path A x y2) (p2' : Path A x y2) (s : Path (Path A x y2) p2 p2') (q2 : Path A y2 z)
           (sq : square A x y1 y2 z p1 q1 p2 q2) : square A x y1 y2 z p1 q1 p2' q2 =
  J
    ( Path A x y2) p2
    ( λp _. square A x y1 y2 z p1 q1 p q2) sq p2' s

1.14 f and ap f through homotopy

Using this naturality square, we can show that if H : f ∼ id, then H(f(x)) = apf(H(x)). Indeed: H (f x) = H (f x) . H x . H x-1 = H (f x) . ap id (H x) . H x-1 = ap f (H x) . (H x) . (H x)-1 = ap f (H x) 

nat-htpy (A : U) (f : A → A) (H : Htpy' A A f (id A)) (x : A)
            : Path (Path A (f (f x)) (f x))
                   (H (f x)) (ap A A f (f x) x (H x)) =
  comp-n
    ( Path A (f (f x)) (f x)) eight-Nat
    ( H (f x)) (comp A (f (f x)) (f x) (H (f x)) (f x) (refl A (f x)))
    ( refl/comp-r A (f (f x)) (f x) (H (f x)))
    ( comp A (f (f x)) (f x) (H (f x)) (f x) (comp A (f x) x (H x) (f x) (inv A (f x) x (H x))))
    ( ap (Path A (f x) (f x)) (Path A (f (f x)) (f x)) (λp. (comp A (f (f x)) (f x) (H (f x)) (f x) p)) (refl A (f x)) (comp A (f x) x (H x) (f x) (inv A (f x) x (H x)))
      ( comp/inv-r' A (f x) x (H x)))
    ( comp A (f (f x)) x (comp A (f (f x)) (f x) (H (f x)) x (H x)) (f x) (inv A (f x) x (H x)))
    ( comp/assoc' A (f (f x)) (f x) (H (f x)) x (H x) (f x) (inv A (f x) x (H x)))
    ( comp A (f (f x)) x (comp A (f (f x)) (f x) (H (f x)) x (ap A A (id A) (f x) x (H x))) (f x) (inv A (f x) x (H x)))
    ( ap (Path A (f x) x) (Path A (f (f x)) (f x)) (λp. comp A (f (f x)) x (comp A (f (f x)) (f x) (H (f x)) x p) (f x) (inv A (f x) x (H x))) (H x) (ap A A (id A) (f x) x (H x))
      ( ap/id A (f x) x (H x)))
    ( comp A (f (f x)) x (comp A (f (f x)) (f x) (ap A A f (f x) x (H x)) x (H x)) (f x) (inv A (f x) x (H x)))
    ( ap (Path A (f (f x)) x) (Path A (f (f x)) (f x)) (λp. comp A (f (f x)) x p (f x) (inv A (f x) x (H x)))
      ( comp A (f (f x)) (f x) (H (f x)) x (ap A A (id A) (f x) x (H x))) (comp A (f (f x)) (f x) (ap A A f (f x) x (H x)) x (H x))
      ( naturality A A f (id A) H (f x) x (H x)))
    ( comp A (f (f x)) (f x) (ap A A f (f x) x (H x)) (f x) (comp A (f x) x (H x) (f x) (inv A (f x) x (H x))))
    ( comp/assoc A (f (f x)) (f x) (ap A A f (f x) x (H x)) x (H x) (f x) (inv A (f x) x (H x)))
    ( comp A (f (f x)) (f x) (ap A A f (f x) x (H x)) (f x) (refl A (f x)))
    ( ap (Path A (f x) (f x)) (Path A (f (f x)) (f x)) (λp. comp A (f (f x)) (f x) (ap A A f (f x) x (H x)) (f x) p) (comp A (f x) x (H x) (f x) (inv A (f x) x (H x))) (refl A (f x))
      ( comp/inv-r A (f x) x (H x)))
    ( ap A A f (f x) x (H x))
    ( comp/ident-r A (f (f x)) (f x) (ap A A f (f x) x (H x)))

nat-htpy' (A : U) (f : A → A) (H : Htpy' A A f (id A)) (x : A)
             : Path (Path A (f (f x)) (f x))
                    (ap A A f (f x) x (H x)) (H (f x)) =
  inv
    ( Path A (f (f x)) (f x))
    ( H (f x))
    ( ap A A f (f x) x (H x))
    ( nat-htpy A f H x)

1.15 ap f (H x) and G (f x)

Let f : A → B and g : B → A such that G : f ˆ g ∼ id and H : g ˆ f ∼ id. Then there is a G' : g ˆ f ∼ id such that ap f (H x) = G' (f x). 

htpy/half-adjoint/htpy (A B : U) (f : A → B) (g : B → A) (G : Htpy' B B (λy. f (g y)) (id B)) (H : Htpy' A A (λx. g (f x)) (id A)) (y : B)
                            : Path B (f (g y)) y =
  comp B
    ( f (g y))
    ( f (g (f (g y))))
    ( inv B (f (g (f (g y)))) (f (g y)) (G (f (g y)))) y
    ( comp B
      ( f (g (f (g y))))
      ( f (g y))
      ( ap A B f (g (f (g y))) (g y) (H (g y))) y
      ( G y))

htpy/half-adjoint (A B : U) (f : A → B) (g : B → A) (G : Htpy' B B (λy. f (g y)) (id B)) (H : Htpy' A A (λx. g (f x)) (id A)) (x : A)
                       : Path (Path B (f (g (f x))) (f x)) (ap A B f (g (f x)) x (H x)) (htpy/half-adjoint/htpy A B f g G H (f x)) =
  inv/concat B
    ( f (g (f (g (f x)))))
    ( f (g (f x)))
    ( G (f (g (f x))))
    ( f x)
    ( ap A B f (g (f x)) x (H x))
    ( comp B
      ( f (g (f (g (f x)))))
      ( f (g (f x)))
      ( ap A B f (g (f (g (f x)))) (g (f x)) (H (g (f x))))
      ( f x)
      ( G (f x)))
    ( square-top B
      ( f (g (f (g (f x)))))
      ( f (g (f x)))
      ( f (g (f x)))
      ( f x)
      ( G (f (g (f x))))     
      ( ap A B f (g (f x)) x (H x))
      ( ap A B (λz. (f (g (f z)))) (g (f x)) x (H x))
      ( ap A B f (g (f (g (f x)))) (g (f x)) (H (g (f x))))
      ( comp 
        ( Path B (f (g (f (g (f x))))) (f (g (f x))))
        ( ap A B (λz. (f (g (f z)))) (g (f x)) x (H x))
        ( ap A B f (g (f (g (f x)))) (g (f x)) (ap A A (λz. g (f z)) (g (f x)) x (H x)))
        ( ap/comp' A A B
          ( λz. g (f z)) f
          ( g (f x)) x
          ( H x))
        ( ap A B f (g (f (g (f x)))) (g (f x)) (H (g (f x))))
        ( ap
          ( Path A (g (f (g (f x)))) (g (f x)))
          ( Path B (f (g (f (g (f x))))) (f (g (f x))))
          ( ap A B f (g (f (g (f x)))) (g (f x)))
          ( ap A A (λz. g (f z)) (g (f x)) x (H x))
          ( H (g (f x)))
          ( nat-htpy' A (λz. g (f z)) H x)))
        ( G (f x))
        ( naturality A B (λz. f (g (f z))) f (λz. G (f z)) (g (f x)) x (H x)))

htpy/half-adjoint' (A B : U) (f : A → B) (g : B → A) (G : Htpy' B B (λy. f (g y)) (id B)) (H : Htpy' A A (λx. g (f x)) (id A)) (x : A)
                        : Path (Path B (f (g (f x))) (f x)) (htpy/half-adjoint/htpy A B f g G H (f x)) (ap A B f (g (f x)) x (H x)) =
  inv 
    ( Path B (f (g (f x))) (f x))
    ( ap A B f (g (f x)) x (H x))
    ( htpy/half-adjoint/htpy A B f g G H (f x))
    ( htpy/half-adjoint A B f g G H x)

1.16 Closure of bi-invertibility

This result is in ContrMap.org.

1.17 Transport of ap

We show that trP(apf(p)) ∼ trP ˆ f(p). 

tr/ap/refl (A B : U) (f : A → B) (P : B → U) (x : A) (u : P (f x))
                : Path (P (f x)) (tr B (f x) (f x) (ap A B f x x (refl A x)) P u) (tr A x x (refl A x) (λz. P (f z)) u) =
  comp
    ( P (f x)) 
    ( tr B (f x) (f x) (ap A B f x x (refl A x)) P u) u
    ( tr/refl-path B (f x) P u)
    ( tr A x x (refl A x) (λz. P (f z)) u)
    ( tr/refl-path' A x (λz. P (f z)) u)

tr/ap (A B : U) (f : A → B) (P : B → U) (x y : A) (p : Path A x y) (u : P (f x))
           : Path (P (f y)) (tr B (f x) (f y) (ap A B f x y p) P u) (tr A x y p (λz. P (f z)) u) =
  J A x
    ( λz q. Path (P (f z)) (tr B (f x) (f z) (ap A B f x z q) P u) (tr A x z q (λz'. P (f z')) u))
    ( tr/ap/refl A B f P x u) y p

1.18 Filling of dependent square of a set

Let a0, a1 : A and p, q : a0 = a1 such that α : p = q. We have a full square with sides (refl a0), (refl a1), p, q. Assume now that B : A → Set, and b0 : B a0, b1 : B a1 with p', q' : b0 = b1 (dependent paths). Then we can fill the square in B, that is, p' = q'. 

square/dependent-fill/refl (A : U) (B : A → UU-Set) (x : A) (x' : A) (p : Path A x x') (y : Set/type (B x)) (y' : Set/type (B x'))
                           (p' q' : PathP (i. Set/type (B (p i))) y y') : Path (PathP (i. Set/type (B (p i))) y y') p' q' =
  J A x
    ( λx0 q. (y0 : Set/type (B x)) → (y1 : Set/type (B x0)) → (p0 q0 : PathP (i. Set/type (B (q i))) y0 y1) → Path (PathP (i. Set/type (B (q i))) y0 y1) p0 q0)
    ( Set/is-set (B x)) x' p y y' p' q'

square/dependent-fill (A : U) (B : A → UU-Set) (x x' : A) (p : Path A x x') : (q : Path A x x') → (spq : Path (Path A x x') p q) →
                      (y : Set/type (B x)) → (y' : Set/type (B x')) → (p' : PathP (i. Set/type (B (p i))) y y') → (q' : PathP (i. Set/type (B (q i))) y y')
                      → PathP (i. PathP (j. Set/type (B (spq i j))) y y') p' q' =
  J ( Path A x x') p
    ( λq'' spq0. (y0 : Set/type (B x)) → (y1 : Set/type (B x')) → (p0 : PathP (i. Set/type (B (p i))) y0 y1) → (q0 : PathP (i. Set/type (B (q'' i))) y0 y1)
                 → PathP (i. PathP (j. Set/type (B (spq0 i j))) y0 y1) p0 q0)
    ( square/dependent-fill/refl A B x x' p)

Author: Johann Rosain

Created: 2024-07-23 Tue 13:51

Validate