Skip to content

Commit

Permalink
wrap lines
Browse files Browse the repository at this point in the history
  • Loading branch information
fredrik-bakke committed Feb 26, 2024
1 parent e16cb15 commit a0b3059
Showing 1 changed file with 8 additions and 4 deletions.
12 changes: 8 additions & 4 deletions src/foundation/universal-property-pullbacks.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -127,7 +127,8 @@ module _
universal-property-pullback j h c
universal-property-pullback i (vertical-map-cone j h c) d
universal-property-pullback (j ∘ i) h (pasting-horizontal-cone i j h c d)
universal-property-pullback-rectangle-universal-property-pullback-left-square c d up-pb-c up-pb-d =
universal-property-pullback-rectangle-universal-property-pullback-left-square
c d up-pb-c up-pb-d =
universal-property-pullback-is-pullback (j ∘ i) h
( pasting-horizontal-cone i j h c d)
( is-pullback-rectangle-is-pullback-left-square i j h c d
Expand All @@ -142,7 +143,8 @@ module _
universal-property-pullback (j ∘ i) h
( pasting-horizontal-cone i j h c d)
universal-property-pullback i (vertical-map-cone j h c) d
universal-property-pullback-left-square-universal-property-pullback-rectangle c d up-pb-c up-pb-rect =
universal-property-pullback-left-square-universal-property-pullback-rectangle
c d up-pb-c up-pb-rect =
universal-property-pullback-is-pullback
( i)
( vertical-map-cone j h c)
Expand Down Expand Up @@ -185,7 +187,8 @@ module _
universal-property-pullback f g c
universal-property-pullback f (g ∘ h) (pasting-vertical-cone f g h c d)
universal-property-pullback (horizontal-map-cone f g c) h d
universal-property-pullback-top-universal-property-pullback-rectangle c d up-pb-c up-pb-dc =
universal-property-pullback-top-universal-property-pullback-rectangle
c d up-pb-c up-pb-dc =
universal-property-pullback-is-pullback
( horizontal-map-cone f g c)
( h)
Expand All @@ -202,7 +205,8 @@ module _
universal-property-pullback f g c
universal-property-pullback (horizontal-map-cone f g c) h d
universal-property-pullback f (g ∘ h) (pasting-vertical-cone f g h c d)
universal-property-pullback-rectangle-universal-property-pullback-top c d up-pb-c up-pb-d =
universal-property-pullback-rectangle-universal-property-pullback-top
c d up-pb-c up-pb-d =
universal-property-pullback-is-pullback
( f)
( g ∘ h)
Expand Down

0 comments on commit a0b3059

Please sign in to comment.