clutch.prob.monad.identity

#[warning="-notation-incompatible-prefix -hiding-delimiting-key"]
  From mathcomp Require Import all_boot all_algebra finmap.
#[warning="-notation-incompatible-prefix"]
From mathcomp Require Import mathcomp_extra boolp classical_sets functions reals interval_inference.
From mathcomp Require Import cardinality fsbigop.
From mathcomp.analysis Require Import ereal normedtype esum numfun measure lebesgue_measure lebesgue_integral.
From HB Require Import structures.

From clutch.prob.monad Require Export types.

From Stdlib.Logic Require Import FunctionalExtensionality.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Set Default Proof Using "Type".

Section MeasurableMap_id.
  Context {d} {T : measurableType d}.
  Local Open Scope classical_set_scope.

  Local Definition m_id_def : T -> T := id.

  Local Lemma m_id_def_measurable :
    @measurable_fun _ _ T T setT m_id_def.
  Proof. apply measurable_id. Qed.

  HB.instance Definition _ :=
    isMeasurableMap.Build _ _ T T m_id_def m_id_def_measurable.
End MeasurableMap_id.

Definition m_id {d} {T : measurableType d} : measurable_map T T :=
  m_id_def.

Definition m_id_eval {d} {T : measurableType d} :
    forall t : T, m_id t = t.
Proof. done. Qed.