Home

同一視型のreasoning

module foundations.identity-type-reasoning where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.groupoid-laws
open import foundations.functions-are-functors

private variable
  ℓ : Level
  A : Type ℓ
  x y z w : A

infix 12 _∎
_∎ : (x : A) → x ＝ x
_ ∎ = refl

infixr 10 _＝⟨_⟩_
_＝⟨_⟩_ : (x : A) → x ＝ y → y ＝ z → x ＝ z
_ ＝⟨ p ⟩ q = p ∙ q

lelimId : ∀ (p : x ＝ x) (q : x ＝ y)
  → p ＝ refl
  → p ∙ q ＝ q
lelimId p q p＝refl = ap (_∙ q) p＝refl ∙ lunitId q

relimId : ∀ (p : x ＝ y) (q : y ＝ y)
  → q ＝ refl
  → p ∙ q ＝ p
relimId p q q＝refl = ap (p ∙_) q＝refl ∙ runitId p

private variable
  p q r : x ＝ y

rcancelId : ∀ (p q : x ＝ y) (r : y ＝ z)
  → p ∙ r ＝ q ∙ r → p ＝ q
rcancelId p q refl s =
    p
  ＝⟨ sym (runitId p) ⟩
    p ∙ refl
  ＝⟨ s ⟩
    q ∙ refl
  ＝⟨ runitId q ⟩
    q
  ∎

lcancelId : ∀ (r : x ＝ y) (p q : y ＝ z)
  → r ∙ p ＝ r ∙ q → p ＝ q
lcancelId refl p q s =
    p
  ＝⟨ sym (lunitId p) ⟩
    refl ∙ p
  ＝⟨ s ⟩
    refl ∙ q
  ＝⟨ lunitId q ⟩
    q
  ∎