diff --git a/_CoqProject b/_CoqProject
index 593d05a767bb0b09ed06d032b742c615c9c1db8b..76621c1e8aa95d1abc505a9ccc7186e3c406837e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -34,6 +34,7 @@ theories/base_logic/hlist.v
 theories/base_logic/soundness.v
 theories/base_logic/double_negation.v
 theories/base_logic/deprecated.v
+theories/base_logic/fix.v
 theories/base_logic/lib/iprop.v
 theories/base_logic/lib/own.v
 theories/base_logic/lib/saved_prop.v
diff --git a/theories/base_logic/fix.v b/theories/base_logic/fix.v
new file mode 100644
index 0000000000000000000000000000000000000000..291de0f979600eb829511f2f05f504a57af175d4
--- /dev/null
+++ b/theories/base_logic/fix.v
@@ -0,0 +1,43 @@
+From iris.base_logic Require Import base_logic.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
+Import uPred.
+
+(** Greatest fixpoint of a monotone function, defined entirely inside
+    the logic.
+    TODO: Also do least fixpoint.
+*)
+
+Definition uPred_mono_pred {M A} (F : (A → uPred M) → (A → uPred M)) :=
+  ∀ P Q, ((□ ∀ x, P x -∗ Q x) -∗ ∀ x, F P x -∗ F Q x)%I.
+
+Definition iGFix {M A} (F : (A → uPred M) → (A → uPred M)) (x : A) : uPred M :=
+  (∃ P, □ (∀ x, P x -∗ F P x) ∧ P x)%I.
+
+Section iGFix.
+  Context {M : ucmraT} {A} (F : (A → uPred M) → (A → uPred M)) (Hmono : uPred_mono_pred F).
+
+  Lemma iGFix_implies_F_iGFix x : iGFix F x ⊢ F (iGFix F) x.
+  Proof.
+    iDestruct 1 as (P) "[#Hincl HP]".
+    iApply (Hmono P (iGFix F)).
+    - iAlways. iIntros (y) "Hy". iExists P. by iSplit.
+    - by iApply "Hincl".
+  Qed.
+
+  Lemma F_iGFix_implies_iGFix x : F (iGFix F) x ⊢ iGFix F x.
+  Proof.
+    iIntros "HF". iExists (F (iGFix F)).
+    iIntros "{$HF} !#"; iIntros (y) "Hy". iApply (Hmono with "[] Hy").
+    iAlways. iIntros (z). by iApply iGFix_implies_F_iGFix.
+  Qed.
+
+  Corollary iGFix_unfold x : iGFix F x ≡ F (iGFix F) x.
+  Proof.
+    apply (anti_symm _); auto using iGFix_implies_F_iGFix, F_iGFix_implies_iGFix.
+  Qed.
+
+  Lemma Fix_coind (P : A → uPred M) (x : A) :
+    □ (∀ y, P y -∗ F P y) -∗ P x -∗ iGFix F x.
+  Proof. iIntros "#HP Hx". iExists P. by iIntros "{$Hx} !#". Qed.
+End iGFix.