πŸ“₯ Download raw
{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProvingBasics.Equality.Reasoning.Core where

open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General

infix  3 _∎
infixr 2 _β‰‘βŸ¨_⟩_ _β‰‘Λ˜βŸ¨_⟩_ _β‰‘βŸ¨βŸ©_
infix  1 begin_

_β‰‘βŸ¨_⟩_ : {A : Set} {y z : A} β†’ (x : A) β†’ x ≑ y β†’ y ≑ z β†’ x ≑ z
x β‰‘βŸ¨ p ⟩ q = trans p q

_β‰‘Λ˜βŸ¨_⟩_ : {A : Set} {y z : A} β†’ (x : A) β†’ y ≑ x β†’ y ≑ z β†’ x ≑ z
x β‰‘Λ˜βŸ¨ p ⟩ q = trans (sym p) q

_β‰‘βŸ¨βŸ©_ : {A : Set} {y : A} β†’ (x : A) β†’ x ≑ y β†’ x ≑ y
x β‰‘βŸ¨βŸ© q = q

_∎ : {A : Set} β†’ (x : A) β†’ x ≑ x
x ∎ = refl

begin_ : {A : Set} {x y : A} β†’ x ≑ y β†’ x ≑ y
begin p = p