(co)partial dependent functions

src/foundation/copartial-functions.lagda.md

@@ -79,12 +79,37 @@ experimental.
 
 ## Definitions
 
+### Copartial dependent functions
+
+```agda
+copartial-dependent-function :
+  {l1 l2 : Level} (l3 : Level) (A : UU l1) → (A → UU l2) →
+  UU (l1 ⊔ l2 ⊔ lsuc l3)
+copartial-dependent-function l3 A B = (x : A) → copartial-element l3 (B x)
+```
+
 ### Copartial functions
 
 ```agda
 copartial-function :
   {l1 l2 : Level} (l3 : Level) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ lsuc l3)
-copartial-function l3 A B = A → copartial-element l3 B
+copartial-function l3 A B = copartial-dependent-function l3 A (λ _ → B)
+```
+
+### Erased values of copartial dependent functions
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
+  (f : copartial-dependent-function l3 A B) (a : A)
+  where
+
+  is-erased-prop-copartial-dependent-function : Prop l3
+  is-erased-prop-copartial-dependent-function =
+    is-erased-prop-copartial-element (f a)
+
+  is-erased-copartial-dependent-function : UU l3
+  is-erased-copartial-dependent-function = is-erased-copartial-element (f a)
 ```
 
 ### Erased values of copartial functions
@@ -97,10 +122,24 @@ module _
 
   is-erased-prop-copartial-function : Prop l3
   is-erased-prop-copartial-function =
-    is-erased-prop-copartial-element (f a)
+    is-erased-prop-copartial-dependent-function f a
 
   is-erased-copartial-function : UU l3
-  is-erased-copartial-function = is-erased-copartial-element (f a)
+  is-erased-copartial-function =
+    is-erased-copartial-dependent-function f a
+```
+
+### Copartial dependent functions obtained from dependent functions
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x)
+  where
+
+  copartial-dependent-function-dependent-function :
+    copartial-dependent-function lzero A B
+  copartial-dependent-function-dependent-function a =
+    unit-copartial-element (f a)
 ```
 
 ### Copartial functions obtained from functions
@@ -111,5 +150,6 @@ module _
   where
 
   copartial-function-function : copartial-function lzero A B
-  copartial-function-function a = unit-copartial-element (f a)
+  copartial-function-function =
+    copartial-dependent-function-dependent-function f
 ```

src/foundation/partial-functions.lagda.md

@@ -46,15 +46,42 @@ where the composition operation is
 
 ## Definitions
 
+### Partial dependent functions
+
+```agda
+partial-dependent-function :
+  {l1 l2 : Level} (l3 : Level) (A : UU l1) (B : A → UU l2) →
+  UU (l1 ⊔ l2 ⊔ lsuc l3)
+partial-dependent-function l3 A B =
+  (x : A) → partial-element l3 (B x)
+```
+
 ### Partial functions
 
 ```agda
 partial-function :
   {l1 l2 : Level} (l3 : Level) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ lsuc l3)
-partial-function l3 A B = A → partial-element l3 B
+partial-function l3 A B = partial-dependent-function l3 A (λ _ → B)
 ```
 
-### The predicate of being defined at an element in the domain
+### The predicate on partial dependent functions of being defined at an element in the domain
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2}
+  (f : partial-dependent-function l3 A B) (a : A)
+  where
+
+  is-defined-prop-partial-dependent-function : Prop l3
+  is-defined-prop-partial-dependent-function =
+    is-defined-prop-partial-element (f a)
+
+  is-defined-partial-dependent-function : UU l3
+  is-defined-partial-dependent-function =
+    type-Prop is-defined-prop-partial-dependent-function
+```
+
+### The predicate on partial functions of being defined at an element in the domain
 
 ```agda
 module _
@@ -63,10 +90,25 @@ module _
   where
 
   is-defined-prop-partial-function : Prop l3
-  is-defined-prop-partial-function = is-defined-prop-partial-element (f a)
+  is-defined-prop-partial-function =
+    is-defined-prop-partial-dependent-function f a
 
   is-defined-partial-function : UU l3
-  is-defined-partial-function = type-Prop is-defined-prop-partial-function
+  is-defined-partial-function =
+    is-defined-partial-dependent-function f a
+```
+
+### The partial dependent function obtained from a dependent function
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x)
+  where
+
+  partial-dependent-function-dependent-function :
+    partial-dependent-function lzero A B
+  partial-dependent-function-dependent-function a =
+    unit-partial-element (f a)
 ```
 
 ### The partial function obtained from a function
@@ -77,7 +119,7 @@ module _
   where
 
   partial-function-function : partial-function lzero A B
-  partial-function-function a = unit-partial-element (f a)
+  partial-function-function = partial-dependent-function-dependent-function f
 ```
 
 ## See also