{-# OPTIONS --safe --cubical #-}

module ProbabilityModule.Utils where

open import Cubical.Core.Everything 
open import Cubical.Foundations.Prelude hiding (_≡⟨_⟩_)

variable
  a b c : Level
  A : Set a
  B : Set b
  C : Set c

infixr  _⊔_
_⊔_ = ℓ-max

infixr  ≡˘⟨⟩-syntax _≡⟨⟩_ ≡⟨∙⟩-syntax

≡˘⟨⟩-syntax : ∀ (x : A) {y z} → y ≡ z → y ≡ x → x ≡ z
≡˘⟨⟩-syntax _ y≡z y≡x = sym y≡x ∙ y≡z

syntax ≡˘⟨⟩-syntax x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z

≡⟨∙⟩-syntax : ∀ (x : A) {y z} → y ≡ z → x ≡ y → x ≡ z
≡⟨∙⟩-syntax _ y≡z x≡y = x≡y ∙ y≡z

syntax ≡⟨∙⟩-syntax x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z

_≡⟨⟩_ : ∀ (x : A) {y} → x ≡ y → x ≡ y
_ ≡⟨⟩ x≡y = x≡y

infix  begin[_]_
begin[_]_ : {x y : A} → I → x ≡ y → A
begin[ i ] x≡y = x≡y i