Skip to content

Commit

Permalink
typo
Browse files Browse the repository at this point in the history
  • Loading branch information
EgbertRijke committed Dec 8, 2023
1 parent 3dfffe2 commit e03764c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/foundation/copartial-functions.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ The map going down is defined by the join operation on copartial elements, i.e.,
the pushout-product algebra structure of the map `T : 1 Prop`. The main idea
behind composition of copartial functions is that a composite of copartial
function is denied on the union of the subtypes where each factor is denied.
Indeed, if `f` is denied at `a` or `map-copartial-eleemnt g` is denied at the
Indeed, if `f` is denied at `a` or `map-copartial-element g` is denied at the
copartial element `f a` of `B`, then the composite of copartial functions
`g ∘ f` should be denied at `a`.

Expand Down

0 comments on commit e03764c

Please sign in to comment.