Skip to content

Commit e94a07d

Browse files
TOTBWFplt-amy
authored andcommitted
fix: Orthogonal is now exported by Lifts
1 parent 241c2d1 commit e94a07d

File tree

3 files changed

+3
-0
lines changed

3 files changed

+3
-0
lines changed

src/Borceux.lagda.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -90,6 +90,7 @@ open import Cat.Instances.Slice
9090
open import Cat.Functor.Closed
9191
open import Cat.Instances.Free
9292
open import Cat.Instances.Sets
93+
open import Cat.Morphism.Lifts
9394
open import Cat.Diagram.Monad
9495
open import Cat.Functor.Final
9596
open import Cat.Functor.Joint

src/Cat/Displayed/Comprehension/Coproduct/Strong.lagda.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ open import Cat.Displayed.Comprehension
55
open import Cat.Displayed.Cartesian
66
open import Cat.Morphism.Orthogonal
77
open import Cat.Displayed.Base
8+
open import Cat.Morphism.Lifts
89
open import Cat.Prelude
910
1011
import Cat.Reasoning

src/Cat/Morphism/Factorisation/Orthogonal.lagda.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
open import Cat.Morphism.Factorisation
44
open import Cat.Morphism.Orthogonal
55
open import Cat.Morphism.Class
6+
open import Cat.Morphism.Lifts
67
open import Cat.Prelude
78
89
import Cat.Reasoning

0 commit comments

Comments
 (0)