Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

rm a couple of the functor #141

Merged
merged 1 commit into from
Aug 13, 2024
Merged

rm a couple of the functor #141

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 8 additions & 23 deletions impredicative_set/imonad_lib.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -221,6 +221,7 @@ Proof. by rewrite functor_o. Qed.

Section id_natural_transformation.
Variables C : functor.

Definition NId := fun A => @idfun (C A).
Let natural_id : naturality C C NId. Proof. by []. Qed.

Expand Down Expand Up @@ -525,47 +526,31 @@ Qed.

End composite_adjoint.

Definition operation (E : functor) (M : monad) := [the functor of E \o M] ~> M.
Definition operation (E : functor) (M : monad) := E \o M ~> M.
Notation "E .-operation M" := (operation E M).

Section algebraicity.
Variables (E : functor) (M : monad).
Definition algebraicity (op : (*E.-operation M*)E \o M ~~> M) :=
Definition algebraicity (op : E \o M ~~> M) :=
forall (A B : UU0) (f : A -> M B) (t : E (M A)),
op A t >>= f = op B ((E # (fun m => m >>= f)) t).
End algebraicity.

HB.mixin Record isAOperation (E : functor) (M : monad) (op : E \o M ~~> M) := {
algebraic : algebraicity op }.

#[short(type=aoperation)]
HB.structure Definition AOperation (E : functor) (M : monad) :=
{op of isAOperation E M op &
isNatural [the functor of E \o M] M op (*NB: this is an operation in fact*)}.
Notation aoperation := AOperation.type.
Arguments algebraic {E} {M} s.
isNatural (E \o M) M op (*NB: this is an operation in fact*)}.

(*Module AOperation.
Section aoperation.
Variables (E : functor) (M : monad).
Record mixin_of (op : E \O M ~> M) := Mixin { _ : algebraicity op }.
Record class_of (op : E \O M ~~> M) := Class {
base : Natural.mixin_of op ;
mixin : mixin_of (Natural.Pack base) }.
Structure t := Pack { m : E \O M ~~> M ; class : class_of m }.
Definition baseType (o : t) := Natural.Pack (base (class o)).
End aoperation.
Module Exports.
Arguments m {E} {M}.
Notation aoperation := t.
Coercion baseType : aoperation >-> nattrans.
Canonical baseType.
End Exports.
End AOperation.
Export AOperation.Exports.*)
Arguments algebraic {E} {M} s.

Notation "E .-aoperation M" := (aoperation E M).

Section algebraic_operation_interface.
Variables (E : functor) (M : monad) (op : E.-aoperation M).

Lemma aoperation_ext (f g : E.-aoperation M) :
f = g <-> forall a, (f a = g a :> (_ -> _)).
Proof.
Expand Down
Loading
Loading