module 1Lab.Path.IdentitySystem.Strict where

Strict Identity SystemsπŸ”—

Since identity systems are a tool for classifying identity types, the relation underlying an identity system enjoys any additional property that the type’s own identity type enjoys. As a prominent example, if (R,r)(R, r) is an identity system on a set, then RR satisfies not only J, but also K: any property P(x)P(x) for x:R(a,a)x : R(a,a), for fixed aa, follows from P(r)P(r).

Since (R,r)(R, r) is equivalent to (≑A,refl)(\equiv_A, \mathrm{refl}), if AA is a set, then RR must be a proposition as well.

set-identity-is-prop
  : βˆ€ {r : (a : A) β†’ R a a} {a b : A}
  β†’ is-identity-system R r
  β†’ is-set A
  β†’ is-prop (R a b)
set-identity-is-prop {R = R} {a = a} {b = b} ids set =
  is-hlevel≃ 1 (identity-system-gives-path ids) (set a b)

This immediately gives us the K eliminator for an identity system over a set: Given a type family P:R(a,a)β†’TypeP : R(a, a) \to \mathrm{Type} and a witness w:P(r(a))w : P(r(a)), since R(βˆ’,βˆ’)R(-,-) is a proposition, we can transport ww to P(s)P(s) for an arbitrary s:R(a,a)s : R(a,a).

IdsK
  : {r : (a : A) β†’ R a a} {a : A}
  β†’ is-identity-system R r
  β†’ is-set A
  β†’ (P : R a a β†’ Type β„“β€²β€²) β†’ P (r a) β†’ βˆ€ s β†’ P s
IdsK {r = r} {a = a} ids set P pr s =
  transport (Ξ» i β†’ P (set-identity-is-prop ids set (r a) s i)) pr