diff --git a/_CoqProject b/_CoqProject
index 0b2786915d69ec4acae71fb98fc95bcf00067bee..c473ac8e45f0116d2a75a2c4ed24da0cbfdf4b8e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -67,6 +67,7 @@ program_logic/hoare.v
 program_logic/language.v
 program_logic/tests.v
 program_logic/ghost_ownership.v
+program_logic/global_functor.v
 program_logic/saved_prop.v
 program_logic/auth.v
 program_logic/sts.v
diff --git a/barrier/barrier.v b/barrier/barrier.v
index 97efedbb5ddd488123dc7f6b9e29f73cf7972ef7..5f4e29df23e36742ce6ec2d669414aaeffe3d428 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -125,7 +125,7 @@ End barrier_proto.
 Import barrier_proto.
 
 (* The functors we need. *)
-Definition barrierGFs := stsGF sts `::` agreeF `::` pnil.
+Definition barrierGFs : iFunctors := [stsGF sts; agreeF].
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
diff --git a/barrier/client.v b/barrier/client.v
index 47bf44ebda396288d69e3051036e134bd0cddab9..5db27c1786908ad504e85ce821a315702cb76dbb 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -26,7 +26,7 @@ Section client.
 End client.
 
 Section ClosedProofs.
-  Definition Σ : iFunctorG := heapGF .:: barrierGFs .++ endGF.
+  Definition Σ : iFunctorG := #[ heapGF ; barrierGFs ].
   Notation iProp := (iPropG heap_lang Σ).
 
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 71a7f35afcf8a355dc348151fb6b1fc7953a87d8..9377ee66d54a3c6f8b90b35affe8230909762af2 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -76,7 +76,7 @@ Section LiftingTests.
 End LiftingTests.
 
 Section ClosedProofs.
-  Definition Σ : iFunctorG := heapGF .:: endGF.
+  Definition Σ : iFunctorG := #[ heapGF ].
   Notation iProp := (iPropG heap_lang Σ).
 
   Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}.
diff --git a/prelude/functions.v b/prelude/functions.v
index d0205d343a5772fbad16131c1767b7ddf05b3d1f..4842faa626e01a2dc7802273a4d59cb4af84ab50 100644
--- a/prelude/functions.v
+++ b/prelude/functions.v
@@ -27,45 +27,4 @@ Section functions.
   Lemma fn_lookup_alter_ne (g : T → T) (f : A → T) a b :
     a ≠ b → alter g a f b = f b.
   Proof. unfold alter, fn_alter. by destruct (decide (a = b)). Qed.
-
 End functions.
-
-(** "Cons-ing" of functions from nat to T *)
-(* Coq's standard lists are not universe polymorphic. Hence we have to re-define them. Ouch.
-   TODO: If we decide to end up going with this, we should move this elsewhere. *)
-Polymorphic Inductive plist {A : Type} : Type :=
-| pnil : plist
-| pcons: A → plist → plist.
-Arguments plist : clear implicits.
-
-Polymorphic Fixpoint papp {A : Type} (l1 l2 : plist A) : plist A :=
-  match l1 with
-  | pnil => l2
-  | pcons a l => pcons a (papp l l2)
-  end.
-
-(* TODO: Notation is totally up for debate. *)
-Infix "`::`" := pcons (at level 60, right associativity) : C_scope.
-Infix "`++`" := papp (at level 60, right associativity) : C_scope.
-
-Polymorphic Definition fn_cons {T : Type} (t : T) (f: nat → T) : nat → T :=
-  λ n, match n with
-       | O => t
-       | S n => f n
-       end.
-
-Polymorphic Fixpoint fn_mcons {T : Type} (ts : plist T) (f : nat → T) : nat → T :=
-  match ts with
-  | pnil => f
-  | pcons t ts => fn_cons t (fn_mcons ts f)
-  end.
-
-(* TODO: Notation is totally up for debate. *)
-Infix ".::" := fn_cons (at level 60, right associativity) : C_scope.
-Infix ".++" := fn_mcons (at level 60, right associativity) : C_scope.
-
-Polymorphic Lemma fn_mcons_app {T : Type} (ts1 ts2 : plist T) f :
-  (ts1 `++` ts2) .++ f = ts1 .++ (ts2 .++ f).
-Proof.
-  induction ts1; simpl; eauto. congruence.
-Qed.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index d056d51cc600daa1a2672b2a6ee06a74394ff96f..a582173d88fd29c469db3e2877d5a82be686fd8f 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -1,5 +1,5 @@
 From algebra Require Export auth.
-From program_logic Require Export invariants ghost_ownership.
+From program_logic Require Export invariants global_functor.
 Import uPred.
 
 Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index d66734f70e0e86ff4256e3d21b38b8221d6591d8..f6fc64e5813aa567be66ef059f90e9971c66684a 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -6,13 +6,17 @@ Import uPred.
 
 (** Index of a CMRA in the product of global CMRAs. *)
 Definition gid := nat.
+
 (** Name of one instance of a particular CMRA in the ghost state. *)
 Definition gname := positive.
+
 (** The global CMRA: Indexed product over a gid i to (gname --fin--> Σ i) *)
 Definition globalF (Σ : gid → iFunctor) : iFunctor :=
   iprodF (λ i, mapF gname (Σ i)).
+Notation iFunctorG := (gid → iFunctor).
+Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
 
-Class inG (Λ : language) (Σ : gid → iFunctor) (A : cmraT) := InG {
+Class inG (Λ : language) (Σ : iFunctorG) (A : cmraT) := InG {
   inG_id : gid;
   inG_prf : A = Σ inG_id (laterC (iPreProp Λ (globalF Σ)))
 }.
@@ -25,32 +29,6 @@ Instance: Params (@to_globalF) 5.
 Instance: Params (@own) 5.
 Typeclasses Opaque to_globalF own.
 
-Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
-Notation iFunctorG := (gid → iFunctor).
-
-(** We need another typeclass to identify the *functor* in the Σ. Basing inG on
-   the functor breaks badly because Coq is unable to infer the correct
-   typeclasses, it does not unfold the functor. *)
-Class inGF (Λ : language) (Σ : gid → iFunctor) (F : iFunctor) := InGF {
-  inGF_id : gid;
-  inGF_prf : F = Σ inGF_id;
-}.
-(* Avoid eager type class search: this line ensures that type class search
-is only triggered if the first two arguments of inGF do not contain evars. Since
-instance search for [inGF] is restrained, instances should always have [inGF] as
-their first argument to avoid loops. For example, the instances [authGF_inGF]
-and [auth_identity] otherwise create a cycle that pops up arbitrarily. *)
-Hint Mode inGF + + - : typeclass_instances.
-
-Lemma inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (laterC (iPreProp Λ (globalF Σ)))).
-Proof. exists inGF_id. by rewrite -inGF_prf. Qed.
-Instance inGF_here {Λ Σ} (F: iFunctor) : inGF Λ (F .:: Σ) F.
-Proof. by exists 0. Qed.
-Instance inGF_further {Λ Σ} (F F': iFunctor) : inGF Λ Σ F → inGF Λ (F' .:: Σ) F.
-Proof. intros [i ?]. by exists (S i). Qed.
-
-Definition endGF : iFunctorG := const (constF unitRA).
-
 (** Properties about ghost ownership *)
 Section global.
 Context `{i : inG Λ Σ A}.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 1d17c0906f29b0cbe30b75f5970e71d8acdec912..fa01192112ecb1d5f52e882b2334d20b73e7fb80 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -1,5 +1,5 @@
 From algebra Require Export agree.
-From program_logic Require Export ghost_ownership.
+From program_logic Require Export global_functor.
 Import uPred.
 
 Notation savedPropG Λ Σ :=
diff --git a/program_logic/sts.v b/program_logic/sts.v
index e118a20b145d6365c5247ceae3c85f85debace46..a2716da5cff0b57ab0965bf4d40c0b97f9431a2c 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -1,5 +1,5 @@
 From algebra Require Export sts.
-From program_logic Require Export invariants ghost_ownership.
+From program_logic Require Export invariants global_functor.
 Import uPred.
 
 Class stsG Λ Σ (sts : stsT) := StsG {