diff --git a/README.md b/README.md
index 9129772c60..62f01ee563 100644
--- a/README.md
+++ b/README.md
@@ -82,3 +82,7 @@ This is an easy step to perform in set theory, but requires a lot of work in typ
 We then check that our construction indeed produces a model of TTT by checking that it satisfies a finite axiomatisation of the theory.
 We have chosen to convert Hailperin's finite axiomatisation of NF's comprehension scheme into a finite axiomatisation of TTT, which we present in our [results file](https://leanprover-community.github.io/con-nf/doc/ConNF/Model/Result.html).
 Note, however, that this choice is arbitrary, and any other finite axiomatisation can be easily proven with the infrastructure already in place.
+
+## Dependency graph
+
+![dependency graph](https://leanprover-community.github.io/con-nf/depgraph.png)
diff --git a/docs/index.md b/docs/index.md
index ccdcb8fe3a..c88a9d0453 100644
--- a/docs/index.md
+++ b/docs/index.md
@@ -87,3 +87,8 @@ This is an easy step to perform in set theory, but requires a lot of work in typ
 We then check that our construction indeed produces a model of TTT by checking that it satisfies a finite axiomatisation of the theory.
 We have chosen to convert Hailperin's finite axiomatisation of NF's comprehension scheme into a finite axiomatisation of TTT, which we present in our [results file](https://leanprover-community.github.io/con-nf/doc/ConNF/Model/Result.html).
 Note, however, that this choice is arbitrary, and any other finite axiomatisation can be easily proven with the infrastructure already in place.
+
+## Dependency graph
+
+![dependency graph](https://leanprover-community.github.io/con-nf/depgraph.png)
+