module foundations.groupoid-laws where
open import foundations.universe open import foundations.identity-type
private variable ℓ : Level A : Type ℓ x y z w : A opaque sym : x ＝ y → y ＝ x sym refl = refl opaque infix 30 _∙_ _∙_ : x ＝ y → y ＝ z → x ＝ z _∙_ refl q = q
ここで、symと_∙_はopaqueに定義されている。したがって以下のような補題を別のモジュールでは使う。
opaque unfolding sym _∙_ symInvolutive : (p : x ＝ y) → sym (sym p) ＝ p symInvolutive refl = refl symRefl : Id (x ＝ x) (sym refl) refl symRefl = refl linvId : (p : x ＝ y) → sym p ∙ p ＝ refl linvId refl = refl rinvId : (p : x ＝ y) → p ∙ sym p ＝ refl rinvId refl = refl lunitId : (p : x ＝ y) → refl ∙ p ＝ p lunitId _ = refl runitId : (p : x ＝ y) → p ∙ refl ＝ p runitId refl = refl assocId : (p : x ＝ y) (q : y ＝ z) (r : z ＝ w) → (p ∙ q) ∙ r ＝ p ∙ (q ∙ r) assocId refl refl _ = refl