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)$ is an identity system on a set, then $R$ satisfies not only J, but also K: any property $P(x)$ for $x : R(a,a)$, for fixed $a$, follows from $P(r)$.

Since $(R, r)$ is equivalent to $(\equiv_A, \mathrm{refl})$, if $A$ is a set, then $R$ 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) \to \mathrm{Type}$ and a witness $w : P(r(a))$, since $R(-,-)$ is a proposition, we can transport $w$ to $P(s)$ for an arbitrary $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)