Skip to content

Commit

Permalink
Correct a typo
Browse files Browse the repository at this point in the history
  • Loading branch information
jwiegley committed Jan 31, 2024
1 parent 3908290 commit 16ba1b2
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Adjunction/Natural/Transformation/Universal.v
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ Context {U : C ⟶ D}.

Program Definition Adjunction_from_Transform (A : F ∹ U) : F ⊣ U := {|
adj := fun a b =>
{| to := {| morphism := fun f =>n fmap f ∘ transform[unit[A]] a |}
{| to := {| morphism := fun f => fmap f ∘ transform[unit[A]] a |}
; from := {| morphism := fun f => transform[counit[A]] b ∘ fmap f |} |}
|}.
Next Obligation. proper; now rewrites. Qed.
Expand Down

0 comments on commit 16ba1b2

Please sign in to comment.