open import 1Lab.Path.IdentitySystem
open import 1Lab.HLevel.Closure
open import 1Lab.HLevel
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.Path.IdentitySystem.Strict where

private variable
  β„“ β„“' β„“'' : Level
  A : Type β„“'
  R : A β†’ A β†’ Type β„“'
  r : βˆ€ a β†’ R a a

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.

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 =
  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 

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

IdsK-refl
  : βˆ€ {β„“ β„“' β„“''} {A : Type β„“} {R : A β†’ A β†’ Type β„“'} {r : βˆ€ a β†’ R a a} {a : A}
  β†’ (ids : is-identity-system R r)
  β†’ (set : is-set A)
  β†’ (P : R a a β†’ Type β„“'')
  β†’ (x : P (r a))
  β†’ IdsK ids set P x (r a) ≑ x
IdsK-refl {R = R} {r = r} {a = a} ids set P x =
  transport (Ξ» i β†’ P (set-identity-is-prop ids set (r a) (r a) i)) x β‰‘βŸ¨βŸ©
  subst P (set-identity-is-prop ids set (r a) (r a)) x               β‰‘βŸ¨ ap (Ξ» Ο• β†’ subst P Ο• x) lemma βŸ©β‰‘
  transport (Ξ» i β†’ P (r a)) x                                        β‰‘βŸ¨ transport-refl x βŸ©β‰‘
  x ∎
  where
    lemma : set-identity-is-prop ids set (r a) (r a) ≑ refl
    lemma = is-prop→is-set (set-identity-is-prop ids set) (r a) (r a) _ _

module StrictIds
  {β„“ β„“'} {A : Type β„“} {R : A β†’ A β†’ Type β„“'} {r : βˆ€ a β†’ R a a}
  (ids : is-identity-system R r)
  (set : is-set A)
  where

  K : βˆ€ {β„“''} {a} β†’ (P : R a a β†’ Type β„“'') β†’ P (r a) β†’ βˆ€ s β†’ P s
  K = IdsK ids set

  K-refl : βˆ€ {β„“''} {a} β†’ (P : R a a β†’ Type β„“'') β†’ (x : P (r a)) β†’ K P x (r a) ≑ x
  K-refl = IdsK-refl ids set

  instance
    R-H-level : βˆ€ {a b} {n} β†’ H-Level (R a b) (1 + n)
    R-H-level = prop-instance (set-identity-is-prop ids set)