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 is an identity system on a set, then satisfies not only J, but also K: any property for for fixed follows from

Since is equivalent to if is a set, then must be a proposition as well.

  : βˆ€ {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 =
  Equiv→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 and a witness since is a proposition, we can transport to for an arbitrary

  : {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