From 67094341fae6c48c36665f962b3cae8bdcc0497d Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Wed, 30 Jul 2025 13:29:08 -0400
Subject: [PATCH 1/4] Starting

---
 src/partialMapClassifierDraft.agda | 63 ++++++++++++++++++++++++++++++
 1 file changed, 63 insertions(+)
 create mode 100644 src/partialMapClassifierDraft.agda

diff --git a/src/partialMapClassifierDraft.agda b/src/partialMapClassifierDraft.agda
new file mode 100644
index 0000000000..ef774fb7e4
--- /dev/null
+++ b/src/partialMapClassifierDraft.agda
@@ -0,0 +1,63 @@
+module partialMapClassifierDraft where
+
+open import Level
+
+open import Data.Product
+open import Data.Empty
+open import Data.Unit
+open import Relation.Binary.PropositionalEquality
+open import Function.Bundles using (_↔_; Inverse)
+
+-- The type of partial elements
+record ↯ {ℓ} (A : Set ℓ) (ℓ' : Level) : Set (ℓ ⊔ suc ℓ') where
+  field
+    Dom : Set ℓ'
+    elt : Dom → A
+
+open ↯
+
+private variable
+  ℓ ℓ' : Level
+  A B : Set ℓ
+
+
+-- Examples : 
+never : ↯ A zero
+never .Dom = ⊥
+never .elt = ⊥-elim
+
+always : A → ↯ A zero
+always a .Dom = ⊤
+always a .elt _ = a
+
+-- The bind propertie
+bind : ↯ A ℓ → (A → ↯ B ℓ') → ↯ B (ℓ ⊔ ℓ')
+bind a↯ f .Dom = Σ[ a↓ ∈ a↯ .Dom ] f (a↯ .elt a↓) .Dom
+bind a↯ f .elt (a↓ , fa↓) = f (a↯ .elt a↓) .elt fa↓
+
+--
+part-map : (A → B) → ↯ A ℓ → ↯ B ℓ
+part-map f a↯ .Dom = a↯ .Dom
+part-map f a↯ .elt d = f (a↯ .elt d)
+
+-- 
+part-ap : ↯ (A → B) ℓ → ↯ A ℓ → ↯ B ℓ
+part-ap a→b↯ a↯ .Dom = a→b↯ .Dom × a↯ .Dom
+part-ap a→b↯ a↯ .elt (f↓ , a↓) = a→b↯ .elt f↓ (a↯ .elt a↓)
+
+-- With different level : 
+part-ap-diff : ↯ (A → B) ℓ → ↯ A ℓ' → ↯ B (ℓ ⊔ ℓ')
+part-ap-diff a→b↯ a↯ .Dom = a→b↯ .Dom × a↯ .Dom
+part-ap-diff a→b↯ a↯ .elt (f↓ , a↓) = a→b↯ .elt f↓ (a↯ .elt a↓)
+
+------------------------------------------------------------------------
+
+-- Extensionality for partial maps
+part-ext : {A : Set ℓ} {x y : ↯ A ℓ'} 
+         → (iso : x .Dom ↔  y .Dom)
+         → (∀ (xd : x .Dom) → x .elt xd ≡ y .elt (Inverse.to iso xd))
+         → x ≡ y
+part-ext = {!   !}
+
+
+

From 8cdf3e106efb09b001d66d53b0cd06337da7004a Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Wed, 30 Jul 2025 15:32:35 -0400
Subject: [PATCH 2/4] modif path

---
 src/Effect/Monad/Partial.agda      | 46 ++++++++++++++++++++++
 src/partialMapClassifierDraft.agda | 63 ------------------------------
 2 files changed, 46 insertions(+), 63 deletions(-)
 create mode 100644 src/Effect/Monad/Partial.agda
 delete mode 100644 src/partialMapClassifierDraft.agda

diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda
new file mode 100644
index 0000000000..0b7b3f7150
--- /dev/null
+++ b/src/Effect/Monad/Partial.agda
@@ -0,0 +1,46 @@
+module Partial where
+
+open import Level
+
+open import Data.Product
+open import Data.Empty
+open import Data.Unit
+
+-- The type of partial elements
+record ↯ {ℓ} (A : Set ℓ) (ℓ' : Level) : Set (ℓ ⊔ suc ℓ') where
+  field
+    Dom : Set ℓ'
+    elt : Dom → A
+
+open ↯
+
+private variable
+  ℓ ℓ' : Level
+  A B : Set ℓ
+
+
+-- 
+never : ↯ A zero
+never .Dom = ⊥
+never .elt = ⊥-elim
+
+always : A → ↯ A zero
+always a .Dom = ⊤
+always a .elt _ = a
+
+----------------------- 
+↯-bind : ↯ A ℓ → (A → ↯ B ℓ') → ↯ B (ℓ ⊔ ℓ')
+↯-bind a↯ f .Dom = Σ[ a↓ ∈ a↯ .Dom ] f (a↯ .elt a↓) .Dom
+↯-bind a↯ f .elt (a↓ , fa↓) = f (a↯ .elt a↓) .elt fa↓
+
+-----------------------
+↯-map : (A → B) → ↯ A ℓ → ↯ B ℓ
+↯-map f a↯ .Dom = a↯ .Dom
+↯-map f a↯ .elt d = f (a↯ .elt d)
+
+-----------------------
+↯-ap : ↯ (A → B) ℓ → ↯ A ℓ' → ↯ B (ℓ ⊔ ℓ')
+↯-ap a→b↯ a↯ .Dom = a→b↯ .Dom × a↯ .Dom
+↯-ap a→b↯ a↯ .elt (f↓ , a↓) = a→b↯ .elt f↓ (a↯ .elt a↓)
+
+
diff --git a/src/partialMapClassifierDraft.agda b/src/partialMapClassifierDraft.agda
deleted file mode 100644
index ef774fb7e4..0000000000
--- a/src/partialMapClassifierDraft.agda
+++ /dev/null
@@ -1,63 +0,0 @@
-module partialMapClassifierDraft where
-
-open import Level
-
-open import Data.Product
-open import Data.Empty
-open import Data.Unit
-open import Relation.Binary.PropositionalEquality
-open import Function.Bundles using (_↔_; Inverse)
-
--- The type of partial elements
-record ↯ {ℓ} (A : Set ℓ) (ℓ' : Level) : Set (ℓ ⊔ suc ℓ') where
-  field
-    Dom : Set ℓ'
-    elt : Dom → A
-
-open ↯
-
-private variable
-  ℓ ℓ' : Level
-  A B : Set ℓ
-
-
--- Examples : 
-never : ↯ A zero
-never .Dom = ⊥
-never .elt = ⊥-elim
-
-always : A → ↯ A zero
-always a .Dom = ⊤
-always a .elt _ = a
-
--- The bind propertie
-bind : ↯ A ℓ → (A → ↯ B ℓ') → ↯ B (ℓ ⊔ ℓ')
-bind a↯ f .Dom = Σ[ a↓ ∈ a↯ .Dom ] f (a↯ .elt a↓) .Dom
-bind a↯ f .elt (a↓ , fa↓) = f (a↯ .elt a↓) .elt fa↓
-
---
-part-map : (A → B) → ↯ A ℓ → ↯ B ℓ
-part-map f a↯ .Dom = a↯ .Dom
-part-map f a↯ .elt d = f (a↯ .elt d)
-
--- 
-part-ap : ↯ (A → B) ℓ → ↯ A ℓ → ↯ B ℓ
-part-ap a→b↯ a↯ .Dom = a→b↯ .Dom × a↯ .Dom
-part-ap a→b↯ a↯ .elt (f↓ , a↓) = a→b↯ .elt f↓ (a↯ .elt a↓)
-
--- With different level : 
-part-ap-diff : ↯ (A → B) ℓ → ↯ A ℓ' → ↯ B (ℓ ⊔ ℓ')
-part-ap-diff a→b↯ a↯ .Dom = a→b↯ .Dom × a↯ .Dom
-part-ap-diff a→b↯ a↯ .elt (f↓ , a↓) = a→b↯ .elt f↓ (a↯ .elt a↓)
-
-------------------------------------------------------------------------
-
--- Extensionality for partial maps
-part-ext : {A : Set ℓ} {x y : ↯ A ℓ'} 
-         → (iso : x .Dom ↔  y .Dom)
-         → (∀ (xd : x .Dom) → x .elt xd ≡ y .elt (Inverse.to iso xd))
-         → x ≡ y
-part-ext = {!   !}
-
-
-

From 55a34ee34ff2e1ec9dca1740830605a3207f689f Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Wed, 30 Jul 2025 15:34:28 -0400
Subject: [PATCH 3/4] correction

---
 src/Effect/Monad/Partial.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda
index 0b7b3f7150..62a49d066e 100644
--- a/src/Effect/Monad/Partial.agda
+++ b/src/Effect/Monad/Partial.agda
@@ -1,4 +1,4 @@
-module Partial where
+module Effect.Monad.Partial where
 
 open import Level
 

From c9c4dbe8e8cbf588c3c3529baa9eb0c42cef3345 Mon Sep 17 00:00:00 2001
From: e-mniang <mariam.niang.etu@gmail.com>
Date: Wed, 30 Jul 2025 21:02:09 -0400
Subject: [PATCH 4/4] formating file

---
 src/Effect/Monad/Partial.agda | 33 +++++++++++++++++++--------------
 1 file changed, 19 insertions(+), 14 deletions(-)

diff --git a/src/Effect/Monad/Partial.agda b/src/Effect/Monad/Partial.agda
index 62a49d066e..3ea44fd7fa 100644
--- a/src/Effect/Monad/Partial.agda
+++ b/src/Effect/Monad/Partial.agda
@@ -1,12 +1,26 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The partial monad
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
 module Effect.Monad.Partial where
 
-open import Level
+open import Level using (Level; suc; zero;_⊔_)
+open import Data.Product using (_×_; Σ; Σ-syntax; _,_)
+open import Data.Empty using (⊥-elim; ⊥)
+open import Data.Unit using (⊤)
+
+private  
+  variable
+    ℓ ℓ' : Level
+    A B : Set ℓ
 
-open import Data.Product
-open import Data.Empty
-open import Data.Unit
+------------------------------------------------------------------------
+-- The partial monad
 
--- The type of partial elements
 record ↯ {ℓ} (A : Set ℓ) (ℓ' : Level) : Set (ℓ ⊔ suc ℓ') where
   field
     Dom : Set ℓ'
@@ -14,12 +28,6 @@ record ↯ {ℓ} (A : Set ℓ) (ℓ' : Level) : Set (ℓ ⊔ suc ℓ') where
 
 open ↯
 
-private variable
-  ℓ ℓ' : Level
-  A B : Set ℓ
-
-
--- 
 never : ↯ A zero
 never .Dom = ⊥
 never .elt = ⊥-elim
@@ -28,17 +36,14 @@ always : A → ↯ A zero
 always a .Dom = ⊤
 always a .elt _ = a
 
------------------------ 
 ↯-bind : ↯ A ℓ → (A → ↯ B ℓ') → ↯ B (ℓ ⊔ ℓ')
 ↯-bind a↯ f .Dom = Σ[ a↓ ∈ a↯ .Dom ] f (a↯ .elt a↓) .Dom
 ↯-bind a↯ f .elt (a↓ , fa↓) = f (a↯ .elt a↓) .elt fa↓
 
------------------------
 ↯-map : (A → B) → ↯ A ℓ → ↯ B ℓ
 ↯-map f a↯ .Dom = a↯ .Dom
 ↯-map f a↯ .elt d = f (a↯ .elt d)
 
------------------------
 ↯-ap : ↯ (A → B) ℓ → ↯ A ℓ' → ↯ B (ℓ ⊔ ℓ')
 ↯-ap a→b↯ a↯ .Dom = a→b↯ .Dom × a↯ .Dom
 ↯-ap a→b↯ a↯ .elt (f↓ , a↓) = a→b↯ .elt f↓ (a↯ .elt a↓)