UniAgda.Core.PathAlgebra

Table of Contents

1 Prelude

2 Groupoid Properties

We show complete the proof that identity types give a groupoid structure. We have that \(\text{refl}_A\) is an identity:

p-refl :  {i} {A : Type i} {a b : A}
         (p : a  b)
          p  refl  p
p-refl refl = refl


refl-p :  {i} {A : Type i} {a b : A}
         (p : a  b)
          refl  p  p
refl-p refl = refl

Inverses:

pp^ :  {i} {A : Type i} {a b : A}
      (p : a  b)
       p  p ^  refl
pp^ refl = refl

p^p :  {i} {A : Type i} {a b : A}
      (p : a  b)
       p ^  p  refl
p^p refl = refl

Associativity of concatenation:

ass-l :  {i} {A : Type i} {a b c d : A}
        (p : a  b) (q : b  c) (r : c  d)
         (p  q)  r  p  (q  r)
ass-l refl q r = refl


ass-r :  {i} {A : Type i} {a b c d : A}
        (p : a  b) (q : b  c) (r : c  d)
         p  (q  r)  (p  q)  r
ass-r refl q r = refl

3 TODO Cancelling inverses

4 Composites with \(\text{refl}\)

5 Rearranging inverses

6 General lemmas

7 Inverses and concatenation

8 Ap properties

9 Transport properties

Author: James Leslie

Created: 2021-03-27 Sat 10:47