Skip to content

Commit

Permalink
fix links
Browse files Browse the repository at this point in the history
  • Loading branch information
EgbertRijke committed Dec 7, 2023
1 parent 3fb79e5 commit c11416a
Show file tree
Hide file tree
Showing 2 changed files with 35 additions and 2 deletions.
21 changes: 19 additions & 2 deletions src/foundation/copartial-functions.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -26,13 +26,30 @@ function is a map
```

where `- * Q` is the
[closed modality](orthogonal-factorization-systems.closed-modalities.md).
[closed modality](orthogonal-factorization-systems.closed-modalities.md), which
is defined by the [join operation](synthetic-homotopy-theory.joins-of-types.md).

A value of a copartial function `f` at `a : A` is said to be
{{#concept "erased" Disambiguation="copartial function" Agda=is-erased-copartial-function}}
if the copartial element `f a` of `B` is erased.

{{#concept "Composition of copartial functions"}} can be defined by
A copartial function is [equivalently](foundation-core.equivalences.md)
described as a [morphism of arrows](foundation.morphisms-arrows.md)

```text
A B 1
| | |
id | ⇒ | □ | T
V V V
A 1 Prop
```

where `□` is the
[pushout-product](synthetic-homotopy-theory.pushout-products.md). Indeed, the
domain of the pushout-product `B □ T` is the type of copartial elements of `B`.

{{#concept "Composition" Disambiguation="copartial functions"}} of copartial
functions can be defined by

```text
Σ (Q : Prop), (Σ (P : Prop), C * P) * Q
Expand Down
16 changes: 16 additions & 0 deletions src/foundation/partial-functions.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,22 @@ Given a partial function `f : A → B` and an element `a : A`, we say that `f` i
{{#concept "defined" Disambiguation="partial function"}} at `a` if the partial
element `f a` of `A` is defined.

Partial functions can be described
[equivalently](foundation-core.equivalences.md) as
[morphisms of arrows](foundation.morphisms-arrows.md)

```text
1
| | |
| ⇒ | ∘ |
V V V
A Prop B
```

where the composition operation is
[composition](species.composition-cauchy-series-species-of-types.md) of
[polynomial endofunctors](trees.polynomial-endofunctors.md).

## Definitions

### Partial functions
Expand Down

0 comments on commit c11416a

Please sign in to comment.