Concatenation Properties
Table of Contents
1 Concatenation properties
module Lib.Prop.Comp where
This file contains some useful properties of concatenation of paths.
1.1 Packages imports
The imported packages can be accessed via the following links:
import Stdlib.Prelude import Lib.Data.Nat
1.2 Inversion of paths
comp/inv-r/refl (A : U) (x : A) : Path (Path A x x) (comp A x x (refl A x) x (inv A x x (refl A x))) (refl A x) = comp-n (Path A x x) two-Nat (comp A x x (refl A x) x (inv A x x (refl A x))) (comp A x x (refl A x) x (refl A x)) (\i. (comp A x x (refl A x) x ((inv/refl A x) i))) (refl A x) (comp/ident-r A x x (refl A x)) comp/inv-r (A : U) (x : A) : (y : A) (p : Path A x y) → Path (Path A x x) (comp A x y p x (inv A x y p)) (refl A x) = J A x (λy p. Path (Path A x x) (comp A x y p x (inv A x y p)) (refl A x)) (comp/inv-r/refl A x) comp/inv-r' (A : U) (x y : A) (p : Path A x y) : Path (Path A x x) (refl A x) (comp A x y p x (inv A x y p)) = inv (Path A x x) (comp A x y p x (inv A x y p)) (refl A x) (comp/inv-r A x y p)
inv-l is furnished, but we can state inv-l'.
comp/inv-l' (A : U) (x y : A) (p : Path A x y) : Path (Path A y y) (refl A y) (comp A y x (inv A x y p) y p) = inv (Path A y y) (comp A y x (inv A x y p) y p) (refl A y) (comp/inv-l A x y p)
1.3 Identity right
refl/comp-r (A : U) (x y : A) (p : Path A x y) : Path (Path A x y) p (comp A x y p y (refl A y)) = inv (Path A x y) (comp A x y p y (refl A y)) p (comp/ident-r A x y p)
1.4 On the inverse of refl
refl/sym (A : U) (x : A) : Path (Path A x x) (refl A x) (inv A x x (refl A x)) = (inv (Path A x x) (inv A x x (refl A x)) (refl A x) (inv/refl A x))
1.5 Associativity
comp/assoc' (A : U) (x y : A) (p : Path A x y) (z : A) (q : Path A y z) (w : A) (r : Path A z w) : Path (Path A x w) (comp A x y p w (comp A y z q w r)) (comp A x z (comp A x y p z q) w r) = inv (Path A x w) (comp A x z (comp A x y p z q) w r) (comp A x y p w (comp A y z q w r)) (comp/assoc A x y p z q w r)
1.6 Path with inverse of concatenation
inv/concat/refl (A : U) (x : A) (z : A) (q : Path A x z) (r : Path A x z) (s : Path (Path A x z) (comp A x x (refl A x) z q) r) : Path (Path A x z) q (comp A x x (inv A x x (refl A x)) z r) = comp-n ( Path A x z) four-Nat q ( comp A x x (refl A x) z q) ( comp/ident-l' A x z q) r s ( comp A x x (refl A x) z r) ( comp/ident-l' A x z r) ( comp A x x (inv A x x (refl A x)) z r) ( ap (Path A x x) (Path A x z) (λp. comp A x x p z r) (refl A x) (inv A x x (refl A x)) ( refl/sym A x)) inv/concat (A : U) (x y : A) (p : Path A x y) (z : A) (q : Path A y z) (r : Path A x z) (s : Path (Path A x z) (comp A x y p z q) r) : Path (Path A y z) q (comp A y x (inv A x y p) z r) = J A x ( λy' p'. (q' : Path A y' z) → (s' : Path (Path A x z) (comp A x y' p' z q') r) → Path (Path A y' z) q' (comp A y' x (inv A x y' p') z r)) ( λq' s'. inv/concat/refl A x z q' r s') y p q s