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)