Skip to content

Commit

Permalink
same lemma for functions
Browse files Browse the repository at this point in the history
  • Loading branch information
EgbertRijke committed Dec 8, 2023
1 parent e03764c commit 1d7d68d
Showing 1 changed file with 29 additions and 0 deletions.
29 changes: 29 additions & 0 deletions src/foundation/copartial-functions.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ module foundation.copartial-functions where

```agda
open import foundation.copartial-elements
open import foundation.partial-functions
open import foundation.propositions
open import foundation.universe-levels
```
Expand Down Expand Up @@ -155,6 +156,34 @@ module _
copartial-dependent-function-dependent-function f
```

## Properties

### The underlying partial dependent function of a copartial dependent function

```agda
module _
{l1 l2 l3 : Level} {A : UU l1} {B : A UU l2}
(f : copartial-dependent-function l3 A B)
where

partial-dependent-function-copartial-dependent-function :
partial-dependent-function l3 A B
partial-dependent-function-copartial-dependent-function a =
partial-element-copartial-element (f a)
```

### The underlying partial function of a copartial function

```agda
module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : copartial-function l3 A B)
where

partial-function-copartial-function : partial-function l3 A B
partial-function-copartial-function a =
partial-element-copartial-element (f a)
```

## See also

- [Partial functions](foundation.partial-functions.md)

0 comments on commit 1d7d68d

Please sign in to comment.