open import 1Lab.Path.IdentitySystem
open import 1Lab.HLevel.Retracts
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Data.Dec.Base

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

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)