{-# 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 2 _⊔_
_⊔_ = ℓ-max

infixr 2 ≡˘⟨⟩-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 1 begin[_]_
begin[_]_ : {x y : A}  I  x  y  A
begin[ i ] x≡y = x≡y i