diff --git a/src/commutative-algebra.lagda.md b/src/commutative-algebra.lagda.md
index bfad391a1c..0f1fc660db 100644
--- a/src/commutative-algebra.lagda.md
+++ b/src/commutative-algebra.lagda.md
@@ -39,6 +39,7 @@ open import commutative-algebra.isomorphisms-commutative-rings public
 open import commutative-algebra.joins-ideals-commutative-rings public
 open import commutative-algebra.joins-radical-ideals-commutative-rings public
 open import commutative-algebra.large-commutative-rings public
+open import commutative-algebra.large-function-commutative-rings public
 open import commutative-algebra.local-commutative-rings public
 open import commutative-algebra.maximal-ideals-commutative-rings public
 open import commutative-algebra.multiples-of-elements-commutative-rings public
diff --git a/src/commutative-algebra/large-function-commutative-rings.lagda.md b/src/commutative-algebra/large-function-commutative-rings.lagda.md
new file mode 100644
index 0000000000..b536098e0e
--- /dev/null
+++ b/src/commutative-algebra/large-function-commutative-rings.lagda.md
@@ -0,0 +1,42 @@
+# Large function commutative rings
+
+```agda
+module commutative-algebra.large-function-commutative-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.large-commutative-rings
+
+open import foundation.function-extensionality
+open import foundation.universe-levels
+
+open import ring-theory.large-function-rings
+```
+
+</details>
+
+## Idea
+
+Given a [large commutative ring](commutative-algebra.large-commutative-rings.md)
+`R` and an arbitrary type `A`, `A → R` forms a large commutative ring.
+
+## Definition
+
+```agda
+module _
+  {l1 : Level}
+  {α : Level → Level}
+  {β : Level → Level → Level}
+  (A : UU l1)
+  (R : Large-Commutative-Ring α β)
+  where
+
+  function-Large-Commutative-Ring :
+    Large-Commutative-Ring (λ l → l1 ⊔ α l) (λ l2 l3 → l1 ⊔ β l2 l3)
+  large-ring-Large-Commutative-Ring function-Large-Commutative-Ring =
+    function-Large-Ring A (large-ring-Large-Commutative-Ring R)
+  commutative-mul-Large-Commutative-Ring function-Large-Commutative-Ring f g =
+    eq-htpy (λ a → commutative-mul-Large-Commutative-Ring R (f a) (g a))
+```
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index f63911de8f..931de9244e 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -213,6 +213,8 @@ open import foundation.fixed-points-endofunctions public
 open import foundation.freely-generated-equivalence-relations public
 open import foundation.full-subtypes public
 open import foundation.function-extensionality public
+open import foundation.function-large-equivalence-relations public
+open import foundation.function-large-similarity-relations public
 open import foundation.function-types public
 open import foundation.function-types-with-apartness-relations public
 open import foundation.functional-correspondences public
diff --git a/src/foundation/function-large-equivalence-relations.lagda.md b/src/foundation/function-large-equivalence-relations.lagda.md
new file mode 100644
index 0000000000..d889d2fcf7
--- /dev/null
+++ b/src/foundation/function-large-equivalence-relations.lagda.md
@@ -0,0 +1,55 @@
+# Function large equivalence relations
+
+```agda
+module foundation.function-large-equivalence-relations where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.large-equivalence-relations
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Given a [large equivalence relation](foundation.large-equivalence-relations.md)
+on `X` and a type `A`, there is an induced large equivalence relation on
+`A → X`.
+
+## Definition
+
+```agda
+module _
+  {l1 : Level}
+  {α : Level → Level}
+  {β : Level → Level → Level}
+  {X : (l : Level) → UU (α l)}
+  (A : UU l1)
+  (R : Large-Equivalence-Relation β X)
+  where
+
+  function-Large-Equivalence-Relation :
+    Large-Equivalence-Relation
+      ( λ l2 l3 → l1 ⊔ β l2 l3)
+      ( λ l → A → X l)
+  sim-prop-Large-Equivalence-Relation function-Large-Equivalence-Relation f g =
+    Π-Prop A (λ a → sim-prop-Large-Equivalence-Relation R (f a) (g a))
+  refl-sim-Large-Equivalence-Relation function-Large-Equivalence-Relation f a =
+    refl-sim-Large-Equivalence-Relation R (f a)
+  symmetric-sim-Large-Equivalence-Relation function-Large-Equivalence-Relation
+    f g f~g a =
+    symmetric-sim-Large-Equivalence-Relation R (f a) (g a) (f~g a)
+  transitive-sim-Large-Equivalence-Relation function-Large-Equivalence-Relation
+    f g h g~h f~g a =
+    transitive-sim-Large-Equivalence-Relation
+      ( R)
+      ( f a)
+      ( g a)
+      ( h a)
+      ( g~h a)
+      ( f~g a)
+```
diff --git a/src/foundation/function-large-similarity-relations.lagda.md b/src/foundation/function-large-similarity-relations.lagda.md
new file mode 100644
index 0000000000..748f22e0e6
--- /dev/null
+++ b/src/foundation/function-large-similarity-relations.lagda.md
@@ -0,0 +1,46 @@
+# Function large similarity relations
+
+```agda
+module foundation.function-large-similarity-relations where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.function-extensionality
+open import foundation.function-large-equivalence-relations
+open import foundation.large-similarity-relations
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Given a [large similarity relation](foundation.large-similarity-relations.md) on
+`X` and any type `A`, there is an induced large similarity relation on `A → X`.
+
+## Definition
+
+```agda
+module _
+  {l1 : Level}
+  {α : Level → Level}
+  {β : Level → Level → Level}
+  {X : (l : Level) → UU (α l)}
+  (A : UU l1)
+  (R : Large-Similarity-Relation β X)
+  where
+
+  function-Large-Similarity-Relation :
+    Large-Similarity-Relation
+      ( λ l2 l3 → l1 ⊔ β l2 l3)
+      ( λ l → A → X l)
+  large-equivalence-relation-Large-Similarity-Relation
+    function-Large-Similarity-Relation =
+    function-Large-Equivalence-Relation
+      ( A)
+      ( large-equivalence-relation-Large-Similarity-Relation R)
+  eq-sim-Large-Similarity-Relation function-Large-Similarity-Relation f g f~g =
+    eq-htpy (λ a → eq-sim-Large-Similarity-Relation R (f a) (g a) (f~g a))
+```
diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md
index 9200822653..03ff85ef95 100644
--- a/src/group-theory.lagda.md
+++ b/src/group-theory.lagda.md
@@ -121,6 +121,11 @@ open import group-theory.kernels-homomorphisms-concrete-groups public
 open import group-theory.kernels-homomorphisms-groups public
 open import group-theory.large-abelian-groups public
 open import group-theory.large-commutative-monoids public
+open import group-theory.large-function-abelian-groups public
+open import group-theory.large-function-commutative-monoids public
+open import group-theory.large-function-groups public
+open import group-theory.large-function-monoids public
+open import group-theory.large-function-semigroups public
 open import group-theory.large-groups public
 open import group-theory.large-monoids public
 open import group-theory.large-semigroups public
diff --git a/src/group-theory/large-function-abelian-groups.lagda.md b/src/group-theory/large-function-abelian-groups.lagda.md
new file mode 100644
index 0000000000..6e5b712512
--- /dev/null
+++ b/src/group-theory/large-function-abelian-groups.lagda.md
@@ -0,0 +1,40 @@
+# Large function abelian groups
+
+```agda
+module group-theory.large-function-abelian-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.function-extensionality
+open import foundation.universe-levels
+
+open import group-theory.large-abelian-groups
+open import group-theory.large-function-groups
+```
+
+</details>
+
+## Idea
+
+Given a [large abelian group](group-theory.large-abelian-groups.md) `G` and an
+arbitrary type `A`, `A → G` forms a large abelian group.
+
+## Definition
+
+```agda
+module _
+  {l1 : Level}
+  {α : Level → Level}
+  {β : Level → Level → Level}
+  (A : UU l1)
+  (G : Large-Ab α β)
+  where
+
+  function-Large-Ab : Large-Ab (λ l → l1 ⊔ α l) (λ l2 l3 → l1 ⊔ β l2 l3)
+  large-group-Large-Ab function-Large-Ab =
+    function-Large-Group A (large-group-Large-Ab G)
+  commutative-add-Large-Ab function-Large-Ab f g =
+    eq-htpy (λ a → commutative-add-Large-Ab G (f a) (g a))
+```
diff --git a/src/group-theory/large-function-commutative-monoids.lagda.md b/src/group-theory/large-function-commutative-monoids.lagda.md
new file mode 100644
index 0000000000..0bdffb1644
--- /dev/null
+++ b/src/group-theory/large-function-commutative-monoids.lagda.md
@@ -0,0 +1,42 @@
+# Large function commutative monoids
+
+```agda
+module group-theory.large-function-commutative-monoids where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.function-extensionality
+open import foundation.universe-levels
+
+open import group-theory.large-commutative-monoids
+open import group-theory.large-function-monoids
+```
+
+</details>
+
+## Idea
+
+Given a [large commutative monoid](group-theory.large-commutative-monoids.md)
+`M` and an arbitrary type `A`, `A → M` forms a large commutative monoid.
+
+## Definition
+
+```agda
+module _
+  {l1 : Level}
+  {α : Level → Level}
+  {β : Level → Level → Level}
+  (A : UU l1)
+  (M : Large-Commutative-Monoid α β)
+  where
+
+  function-Large-Commutative-Monoid :
+    Large-Commutative-Monoid (λ l → l1 ⊔ α l) (λ l2 l3 → l1 ⊔ β l2 l3)
+  large-monoid-Large-Commutative-Monoid function-Large-Commutative-Monoid =
+    function-Large-Monoid A (large-monoid-Large-Commutative-Monoid M)
+  commutative-mul-Large-Commutative-Monoid function-Large-Commutative-Monoid
+    f g =
+    eq-htpy ( λ a → commutative-mul-Large-Commutative-Monoid M (f a) (g a))
+```
diff --git a/src/group-theory/large-function-groups.lagda.md b/src/group-theory/large-function-groups.lagda.md
new file mode 100644
index 0000000000..b392b0619d
--- /dev/null
+++ b/src/group-theory/large-function-groups.lagda.md
@@ -0,0 +1,45 @@
+# Large function groups
+
+```agda
+module group-theory.large-function-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.function-extensionality
+open import foundation.universe-levels
+
+open import group-theory.large-function-monoids
+open import group-theory.large-groups
+```
+
+</details>
+
+## Idea
+
+Given a [large group](group-theory.large-groups.md) `G` and an arbitrary type
+`A`, `A → G` forms a large group.
+
+## Definition
+
+```agda
+module _
+  {l1 : Level}
+  {α : Level → Level}
+  {β : Level → Level → Level}
+  (A : UU l1)
+  (G : Large-Group α β)
+  where
+
+  function-Large-Group : Large-Group (λ l → l1 ⊔ α l) (λ l2 l3 → l1 ⊔ β l2 l3)
+  large-monoid-Large-Group function-Large-Group =
+    function-Large-Monoid A (large-monoid-Large-Group G)
+  inv-Large-Group function-Large-Group f a = inv-Large-Group G (f a)
+  preserves-sim-inv-Large-Group function-Large-Group f g f~g a =
+    preserves-sim-inv-Large-Group G (f a) (g a) (f~g a)
+  left-inverse-law-mul-Large-Group function-Large-Group f =
+    eq-htpy (λ a → left-inverse-law-mul-Large-Group G (f a))
+  right-inverse-law-mul-Large-Group function-Large-Group f =
+    eq-htpy (λ a → right-inverse-law-mul-Large-Group G (f a))
+```
diff --git a/src/group-theory/large-function-monoids.lagda.md b/src/group-theory/large-function-monoids.lagda.md
new file mode 100644
index 0000000000..73ea17caf6
--- /dev/null
+++ b/src/group-theory/large-function-monoids.lagda.md
@@ -0,0 +1,54 @@
+# Large function monoids
+
+```agda
+module group-theory.large-function-monoids where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.function-extensionality
+open import foundation.function-large-similarity-relations
+open import foundation.universe-levels
+
+open import group-theory.large-function-semigroups
+open import group-theory.large-monoids
+```
+
+</details>
+
+## Idea
+
+Given a [large monoid](group-theory.large-monoids.md) `M` and an arbitrary type
+`A`, `A → M` forms a large monoid.
+
+## Definition
+
+```agda
+module _
+  {l1 : Level}
+  {α : Level → Level}
+  {β : Level → Level → Level}
+  (A : UU l1)
+  (M : Large-Monoid α β)
+  where
+
+  function-Large-Monoid :
+    Large-Monoid (λ l → l1 ⊔ α l) (λ l2 l3 → l1 ⊔ β l2 l3)
+  large-semigroup-Large-Monoid function-Large-Monoid =
+    function-Large-Semigroup A (large-semigroup-Large-Monoid M)
+  large-similarity-relation-Large-Monoid function-Large-Monoid =
+    function-Large-Similarity-Relation
+      ( A)
+      ( large-similarity-relation-Large-Monoid M)
+  raise-Large-Monoid function-Large-Monoid l f a = raise-Large-Monoid M l (f a)
+  sim-raise-Large-Monoid function-Large-Monoid l2 f a =
+    sim-raise-Large-Monoid M l2 (f a)
+  preserves-sim-mul-Large-Monoid function-Large-Monoid f f' f~f' g g' g~g' a =
+    preserves-sim-mul-Large-Monoid M (f a) (f' a) (f~f' a) (g a) (g' a) (g~g' a)
+  unit-Large-Monoid function-Large-Monoid a = unit-Large-Monoid M
+  left-unit-law-mul-Large-Monoid function-Large-Monoid f =
+    eq-htpy (λ a → left-unit-law-mul-Large-Monoid M (f a))
+  right-unit-law-mul-Large-Monoid function-Large-Monoid f =
+    eq-htpy (λ a → right-unit-law-mul-Large-Monoid M (f a))
+```
diff --git a/src/group-theory/large-function-semigroups.lagda.md b/src/group-theory/large-function-semigroups.lagda.md
new file mode 100644
index 0000000000..eccc5ffe24
--- /dev/null
+++ b/src/group-theory/large-function-semigroups.lagda.md
@@ -0,0 +1,36 @@
+# Large function semigroups
+
+```agda
+module group-theory.large-function-semigroups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.function-extensionality
+open import foundation.sets
+open import foundation.universe-levels
+
+open import group-theory.large-semigroups
+```
+
+</details>
+
+## Idea
+
+Given a [large semigroup](group-theory.large-semigroups.md) `G` and an arbitrary
+type `A`, `A → G` forms a large semigroup.
+
+## Definition
+
+```agda
+function-Large-Semigroup :
+  {l : Level} {α : Level → Level} → UU l → Large-Semigroup α →
+  Large-Semigroup (λ l' → l ⊔ α l')
+function-Large-Semigroup A G =
+  make-Large-Semigroup
+    ( λ l → function-Set A (set-Large-Semigroup G l))
+    ( λ f g a → mul-Large-Semigroup G (f a) (g a))
+    ( λ f g h →
+      eq-htpy (λ a → associative-mul-Large-Semigroup G (f a) (g a) (h a)))
+```
diff --git a/src/ring-theory.lagda.md b/src/ring-theory.lagda.md
index 86b8179244..896f12a557 100644
--- a/src/ring-theory.lagda.md
+++ b/src/ring-theory.lagda.md
@@ -54,6 +54,7 @@ open import ring-theory.joins-ideals-rings public
 open import ring-theory.joins-left-ideals-rings public
 open import ring-theory.joins-right-ideals-rings public
 open import ring-theory.kernels-of-ring-homomorphisms public
+open import ring-theory.large-function-rings public
 open import ring-theory.large-rings public
 open import ring-theory.left-ideals-generated-by-subsets-rings public
 open import ring-theory.left-ideals-rings public
diff --git a/src/ring-theory/large-function-rings.lagda.md b/src/ring-theory/large-function-rings.lagda.md
new file mode 100644
index 0000000000..b5b54bff30
--- /dev/null
+++ b/src/ring-theory/large-function-rings.lagda.md
@@ -0,0 +1,53 @@
+# Large function rings
+
+```agda
+module ring-theory.large-function-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.function-extensionality
+open import foundation.universe-levels
+
+open import group-theory.large-function-abelian-groups
+
+open import ring-theory.large-rings
+```
+
+</details>
+
+## Idea
+
+Given a [large ring](ring-theory.large-rings.md) `R` and an arbitrary type `A`,
+`A → R` forms a large ring.
+
+## Definition
+
+```agda
+module _
+  {l1 : Level}
+  {α : Level → Level}
+  {β : Level → Level → Level}
+  (A : UU l1)
+  (R : Large-Ring α β)
+  where
+
+  function-Large-Ring : Large-Ring (λ l → l1 ⊔ α l) (λ l2 l3 → l1 ⊔ β l2 l3)
+  large-ab-Large-Ring function-Large-Ring =
+    function-Large-Ab A (large-ab-Large-Ring R)
+  mul-Large-Ring function-Large-Ring f g a = mul-Large-Ring R (f a) (g a)
+  preserves-sim-mul-Large-Ring function-Large-Ring f f' f~f' g g' g~g' a =
+    preserves-sim-mul-Large-Ring R (f a) (f' a) (f~f' a) (g a) (g' a) (g~g' a)
+  one-Large-Ring function-Large-Ring a = one-Large-Ring R
+  associative-mul-Large-Ring function-Large-Ring f g h =
+    eq-htpy (λ a → associative-mul-Large-Ring R (f a) (g a) (h a))
+  left-unit-law-mul-Large-Ring function-Large-Ring f =
+    eq-htpy (λ a → left-unit-law-mul-Large-Ring R (f a))
+  right-unit-law-mul-Large-Ring function-Large-Ring f =
+    eq-htpy (λ a → right-unit-law-mul-Large-Ring R (f a))
+  left-distributive-mul-add-Large-Ring function-Large-Ring f g h =
+    eq-htpy (λ a → left-distributive-mul-add-Large-Ring R (f a) (g a) (h a))
+  right-distributive-mul-add-Large-Ring function-Large-Ring f g h =
+    eq-htpy (λ a → right-distributive-mul-add-Large-Ring R (f a) (g a) (h a))
+```