Fiberwise orthogonal maps and closure properties of the right class (#…

…1152) This is the replacement for #1032.
UniMath · Jun 4, 2024 · b4aac3c · b4aac3c
1 parent 8ad6a6a
commit b4aac3c
Show file tree

Hide file tree

Showing 3 changed files with 426 additions and 4 deletions.
diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md
@@ -22,6 +22,7 @@ open import orthogonal-factorization-systems.factorization-operations-global-fun
 open import orthogonal-factorization-systems.factorizations-of-maps public
 open import orthogonal-factorization-systems.factorizations-of-maps-function-classes public
 open import orthogonal-factorization-systems.factorizations-of-maps-global-function-classes public
+open import orthogonal-factorization-systems.fiberwise-orthogonal-maps public
 open import orthogonal-factorization-systems.function-classes public
 open import orthogonal-factorization-systems.functoriality-higher-modalities public
 open import orthogonal-factorization-systems.functoriality-pullback-hom public