diff --git a/_CoqProject b/_CoqProject
index c8698f0dbfcc8ff21318e20054b67c558ac6bb92..81a1f9bb0253a5c982bc328ea6b6af7618f0c4db 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -47,6 +47,7 @@ algebra/dra.v
 algebra/cofe_solver.v
 algebra/agree.v
 algebra/excl.v
+algebra/functor.v
 program_logic/upred.v
 program_logic/model.v
 program_logic/adequacy.v
@@ -61,7 +62,6 @@ program_logic/pviewshifts.v
 program_logic/resources.v
 program_logic/hoare.v
 program_logic/language.v
-program_logic/functor.v
 program_logic/tests.v
 heap_lang/heap_lang.v
 heap_lang/heap_lang_tactics.v
diff --git a/algebra/agree.v b/algebra/agree.v
index 62ec7ff26efe431e1e7d04ad195aeaa86620024f..bb07a72e9647b863f238d8555d05114f523805d4 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -1,4 +1,5 @@
 Require Export algebra.cmra.
+Require Import algebra.functor.
 Local Hint Extern 10 (_ ≤ _) => omega.
 
 Record agree (A : Type) : Type := Agree {
@@ -174,3 +175,8 @@ Proof.
   intros f g Hfg x; split; simpl; intros; first done.
   by apply dist_le with n; try apply Hfg.
 Qed.
+
+Program Definition agreeF : iFunctor :=
+  {| ifunctor_car := agreeRA; ifunctor_map := @agreeC_map |}.
+Solve Obligations with done.
+
diff --git a/algebra/auth.v b/algebra/auth.v
index f5b396813a344693d4f70d541d5c0ab5ffab0937..29760ee65f234ebf447e5c1d6c1e1fc8025ce2d6 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -1,4 +1,5 @@
 Require Export algebra.excl.
+Require Import algebra.functor.
 Local Arguments validN _ _ _ !_ /.
 
 Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
@@ -198,3 +199,19 @@ Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
   CofeMor (auth_map f).
 Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
 Proof. intros f f' Hf [[a| |] b]; repeat constructor; apply Hf. Qed.
+
+Program Definition authF (Σ : iFunctor) : iFunctor := {|
+  ifunctor_car := authRA ∘ Σ; ifunctor_map A B := authC_map ∘ ifunctor_map Σ
+|}.
+Next Obligation.
+  by intros Σ A B n f g Hfg; apply authC_map_ne, ifunctor_map_ne.
+Qed.
+Next Obligation.
+  intros Σ A x. rewrite /= -{2}(auth_map_id x).
+  apply auth_map_ext=>y; apply ifunctor_map_id.
+Qed.
+Next Obligation.
+  intros Σ A B C f g x. rewrite /= -auth_map_compose.
+  apply auth_map_ext=>y; apply ifunctor_map_compose.
+Qed.
+
diff --git a/algebra/excl.v b/algebra/excl.v
index d0a7df42a4d9f50c76bf5f7ff5394d0af99c0506..f2acac84df0e83272e17cf25105176d19e1f9fde 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -1,4 +1,5 @@
 Require Export algebra.cmra.
+Require Import algebra.functor.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
@@ -181,3 +182,9 @@ Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
   CofeMor (excl_map f).
 Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
 Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
+
+Program Definition exclF : iFunctor :=
+  {| ifunctor_car := exclRA; ifunctor_map := @exclC_map |}.
+Next Obligation. by intros A x; rewrite /= excl_map_id. Qed.
+Next Obligation. by intros A B C f g x; rewrite /= excl_map_compose. Qed.
+
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 9ca47881ee00675aa81c3647642e18d7ebdef24a..b2b65e30d63bfa063e33b1ba657669f9000bd712 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -1,4 +1,5 @@
 Require Export algebra.cmra prelude.gmap algebra.option.
+Require Import algebra.functor.
 
 Section cofe.
 Context `{Countable K} {A : cofeT}.
@@ -246,3 +247,18 @@ Proof.
   intros f g Hf m k; rewrite /= !lookup_fmap.
   destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
 Qed.
+
+Program Definition mapF K `{Countable K} (Σ : iFunctor) : iFunctor := {|
+  ifunctor_car := mapRA K ∘ Σ; ifunctor_map A B := mapC_map ∘ ifunctor_map Σ
+|}.
+Next Obligation.
+  by intros K ?? Σ A B n f g Hfg; apply mapC_map_ne, ifunctor_map_ne.
+Qed.
+Next Obligation.
+  intros K ?? Σ A x. rewrite /= -{2}(map_fmap_id x).
+  apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_id.
+Qed.
+Next Obligation.
+  intros K ?? Σ A B C f g x. rewrite /= -map_fmap_compose.
+  apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_compose.
+Qed.
diff --git a/program_logic/functor.v b/algebra/functor.v
similarity index 51%
rename from program_logic/functor.v
rename to algebra/functor.v
index 1fe9547630a1f9bd4e24266197da53c5195945ac..819ca5b5f398851712ed03e33f6cd4a82dc5048e 100644
--- a/program_logic/functor.v
+++ b/algebra/functor.v
@@ -1,12 +1,7 @@
 Require Export algebra.cmra.
-Require Import algebra.agree algebra.excl algebra.auth.
-Require Import algebra.option algebra.fin_maps.
 
 (** * Functors from COFE to CMRA *)
-(* The Iris program logic is parametrized by a functor from the category of
-COFEs to the category of CMRAs, which is instantiated with [laterC iProp]. The
-[laterC iProp] can be used to construct impredicate CMRAs, such as the stored
-propositions using the agreement CMRA. *)
+(* TODO RJ: Maybe find a better name for this? It is not PL-specific any more. *)
 Structure iFunctor := IFunctor {
   ifunctor_car :> cofeT → cmraT;
   ifunctor_map {A B} (f : A -n> B) : ifunctor_car A -n> ifunctor_car B;
@@ -60,57 +55,3 @@ Next Obligation.
   intros A Σ B1 B2 B3 f1 f2 g. rewrite /= -iprod_map_compose.
   apply iprod_map_ext=> y; apply ifunctor_map_compose.
 Qed.
-
-Program Definition agreeF : iFunctor :=
-  {| ifunctor_car := agreeRA; ifunctor_map := @agreeC_map |}.
-Solve Obligations with done.
-
-Program Definition exclF : iFunctor :=
-  {| ifunctor_car := exclRA; ifunctor_map := @exclC_map |}.
-Next Obligation. by intros A x; rewrite /= excl_map_id. Qed.
-Next Obligation. by intros A B C f g x; rewrite /= excl_map_compose. Qed.
-
-Program Definition authF (Σ : iFunctor) : iFunctor := {|
-  ifunctor_car := authRA ∘ Σ; ifunctor_map A B := authC_map ∘ ifunctor_map Σ
-|}.
-Next Obligation.
-  by intros Σ A B n f g Hfg; apply authC_map_ne, ifunctor_map_ne.
-Qed.
-Next Obligation.
-  intros Σ A x. rewrite /= -{2}(auth_map_id x).
-  apply auth_map_ext=>y; apply ifunctor_map_id.
-Qed.
-Next Obligation.
-  intros Σ A B C f g x. rewrite /= -auth_map_compose.
-  apply auth_map_ext=>y; apply ifunctor_map_compose.
-Qed.
-
-Program Definition optionF (Σ : iFunctor) : iFunctor := {|
-  ifunctor_car := optionRA ∘ Σ; ifunctor_map A B := optionC_map ∘ ifunctor_map Σ
-|}.
-Next Obligation.
-  by intros Σ A B n f g Hfg; apply optionC_map_ne, ifunctor_map_ne.
-Qed.
-Next Obligation.
-  intros Σ A x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_setoid_ext=>y; apply ifunctor_map_id.
-Qed.
-Next Obligation.
-  intros Σ A B C f g x. rewrite /= -option_fmap_compose.
-  apply option_fmap_setoid_ext=>y; apply ifunctor_map_compose.
-Qed.
-
-Program Definition mapF K `{Countable K} (Σ : iFunctor) : iFunctor := {|
-  ifunctor_car := mapRA K ∘ Σ; ifunctor_map A B := mapC_map ∘ ifunctor_map Σ
-|}.
-Next Obligation.
-  by intros K ?? Σ A B n f g Hfg; apply mapC_map_ne, ifunctor_map_ne.
-Qed.
-Next Obligation.
-  intros K ?? Σ A x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_id.
-Qed.
-Next Obligation.
-  intros K ?? Σ A B C f g x. rewrite /= -map_fmap_compose.
-  apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_compose.
-Qed.
diff --git a/algebra/option.v b/algebra/option.v
index 4c443e3a82b8e5df89487e0366a2af83806eb85b..e6fb047af9dac30dcd621f08b25088947c0c35fa 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -1,4 +1,5 @@
 Require Export algebra.cmra.
+Require Import algebra.functor.
 
 (* COFE *)
 Section cofe.
@@ -173,3 +174,19 @@ Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
   CofeMor (fmap f : optionC A → optionC B).
 Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B).
 Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
+
+Program Definition optionF (Σ : iFunctor) : iFunctor := {|
+  ifunctor_car := optionRA ∘ Σ; ifunctor_map A B := optionC_map ∘ ifunctor_map Σ
+|}.
+Next Obligation.
+  by intros Σ A B n f g Hfg; apply optionC_map_ne, ifunctor_map_ne.
+Qed.
+Next Obligation.
+  intros Σ A x. rewrite /= -{2}(option_fmap_id x).
+  apply option_fmap_setoid_ext=>y; apply ifunctor_map_id.
+Qed.
+Next Obligation.
+  intros Σ A B C f g x. rewrite /= -option_fmap_compose.
+  apply option_fmap_setoid_ext=>y; apply ifunctor_map_compose.
+Qed.
+
diff --git a/program_logic/model.v b/program_logic/model.v
index 022e7419e5cd1a151dc308a657a9b1c96a86b149..d6d9721b09bf3ec830670d2dbb1d60b93b53ecae 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -1,6 +1,11 @@
 Require Export program_logic.upred program_logic.resources.
 Require Import algebra.cofe_solver.
 
+(* The Iris program logic is parametrized by a functor from the category of
+COFEs to the category of CMRAs, which is instantiated with [laterC iProp]. The
+[laterC iProp] can be used to construct impredicate CMRAs, such as the stored
+propositions using the agreement CMRA. *)
+
 Module iProp.
 Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT :=
   uPredC (resRA Λ Σ (laterC A)).
diff --git a/program_logic/resources.v b/program_logic/resources.v
index 44edf9de470114ddfd168395659e602c43b0580b..d4c2aebe61560f6aef39fcb7ad45af45bbf378bc 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -1,5 +1,5 @@
-Require Export algebra.fin_maps algebra.agree algebra.excl.
-Require Export program_logic.language program_logic.functor.
+Require Export algebra.fin_maps algebra.agree algebra.excl algebra.functor.
+Require Export program_logic.language.
 
 Record res (Λ : language) (Σ : iFunctor) (A : cofeT) := Res {
   wld : mapRA positive (agreeRA A);