Other Agda modules in this section (52)
Corresponding book passages
# The boundary composites of a framed square
Recover the actual square diagram from its vertical arrow. Its recurrying
comparison transports both vertical endpoint frames before the horizontal
endpoint equations are converted to complete native corner comparisons.
Both triangle restrictions will use one framed diagonal of that same square.
```agda
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter02.Section02.FramedSquareCommutativity where
open import SCT.VolumeI.Chapter01.Section01.Vocabulary
open Operations
open import SCT.VolumeI.Chapter01.Section01.Terminal using (module Constructions)
open Constructions using (const)
open import SCT.VolumeI.Chapter01.Section02.Coherence
using (id₌; comp-assoc; comp-unitʳ; module Composition)
open Composition
open import SCT.VolumeI.Chapter01.Section02.Products using (module Calculus)
open Calculus
open import SCT.VolumeI.Chapter01.Section02.Specialization
using (comp₌-assoc; comp₌-cong; comp-inv-left; comp-inv-right; postWhisker-comp₌)
open import SCT.VolumeI.Chapter01.Section03.Identifications.Inverses
using (cancel-left; cancel-right)
open import SCT.VolumeI.Chapter01.Section06.Cones
using (Cone; ConeIdentification₁)
open import SCT.VolumeI.Chapter01.Section06.ConeFramings using (framed-cone)
open import SCT.VolumeI.Chapter01.Section07.FunctorCategories using (Fun; funEval; funUniversal)
open import SCT.VolumeI.Chapter01.Section07.Currying
using (funCurry; funUncurry; funCurry-β; funCurry-η; curry⁼)
open import SCT.VolumeI.Chapter02.Section01.WalkingMorphism using ([1]; zero; one)
open import SCT.VolumeI.Chapter02.Section01.Morphisms
using (Ar; evAt; ev₀; ev₁; MorphismFamily; MorphismFamilyIdentification)
open import SCT.VolumeI.Chapter02.Section02.SquareCoordinates using (module SquareCoordinates)
open import SCT.VolumeI.Chapter02.Section02.SquareCurrying using (module SquareCurrying)
import SCT.VolumeI.Chapter02.Section02.SquareCornerEndpoints as Endpoints
private
module Recovery {Γ : Context} {P C : CAT Γ} (N : MAP P (Ar (Ar C))) where
private
I : CAT Γ
I = [1]
module Coordinate = SquareCoordinates P
first : MAP (P × (I × I)) (P × I)
first = pair pr₁ (pr₂ ∘ pr₂)
last : MAP (P × (I × I)) I
last = pr₁ ∘ pr₂
backward : MAP (P × (I × I)) ((P × I) × I)
backward = pair first last
parameter : (pr₁ ∘ Coordinate.permute) =₁ (pr₁ ∘ pr₁)
parameter = pair-β₁ Coordinate.parameter Coordinate.rectangle
outer : ((pr₂ ∘ pr₂) ∘ Coordinate.permute) =₁ (pr₂ ∘ pr₁)
outer = pair-β₂ Coordinate.inner Coordinate.outer ∙
((pr₂ ◁ pair-β₂ Coordinate.parameter Coordinate.rectangle) ∙
comp-assoc Coordinate.permute pr₂ pr₂)
inner : (last ∘ Coordinate.permute) =₁ pr₂
inner = pair-β₁ Coordinate.inner Coordinate.outer ∙
((pr₁ ◁ pair-β₂ Coordinate.parameter Coordinate.rectangle) ∙
comp-assoc Coordinate.permute pr₂ pr₁)
backward-forward : (backward ∘ Coordinate.permute) =₁ id ((P × I) × I)
backward-forward = pair-projections ∙
(pair⁼ (pair-η pr₁) (id₌ pr₂) ∙
(pair⁼ (pair⁼ parameter outer ∙ pair-pre pr₁ (pr₂ ∘ pr₂) Coordinate.permute) inner ∙
pair-pre first last Coordinate.permute))
diagram : MAP ((P × I) × I) C
diagram = funUncurry (funUncurry N)
square : MAP P (Fun (I × I) C)
square = funCurry (diagram ∘ backward)
module Curried = SquareCurrying square
private
raw : Curried.reordered =₁ diagram
raw = comp-unitʳ diagram ∙
((diagram ◁ backward-forward) ∙
(comp-assoc Coordinate.permute backward diagram ∙
(funCurry-β (diagram ∘ backward) ▷ Coordinate.permute)))
inner-comparison : Curried.first-curry =₁ funUncurry N
inner-comparison = funCurry-η (funUncurry N) ∙
curry⁼ (funEval {C = I} {D = C}) (funUniversal I C) raw
comparison : Curried.nested =₁ N
comparison = funCurry-η N ∙
curry⁼ (funEval {C = I} {D = Ar C}) (funUniversal I (Ar C)) inner-comparison
module NativeCornerFromEndpoint {Γ : Context} {P C : CAT Γ}
(sigma : MAP P (Fun ([1] × [1]) C))
(a b : MAP One ([1] {Γ = Γ})) (h k : MAP P (Ar C)) {z : MAP P C}
(p : (evAt b ∘ h) =₁ z) (q : (evAt a ∘ k) =₁ z)
(left : Endpoints.At.Curried.Horizontal.side sigma a =₁ h)
(right : Endpoints.At.Curried.Vertical.side sigma b =₁ k) where
module Native = Endpoints.At.NativeCorner sigma a b
private
module Normal = Endpoints.At.EndpointNormalization sigma a b h k p q left right
horizontal-comparison : Native.Horizontal.evaluated =₁ h
horizontal-comparison = left ∙ Native.Horizontal.comparison
vertical-boundary : (evAt b ∘ Endpoints.At.Curried.nested sigma) =₁ k
vertical-boundary = right ∙ Native.Vertical.boundary
point-boundary : (evAt b ∘ Native.Horizontal.evaluated) =₁ (evAt a ∘ k)
point-boundary = (evAt a ◁ vertical-boundary) ∙ Native.postcomposition-point
private
left-image = evAt b ◁ left
right-image = evAt a ◁ right
eta = Native.horizontal-endpoint
boundary-image = evAt a ◁ Native.Vertical.boundary
point = Native.postcomposition-point
K = Native.matching
left-normal : (p ∙ (evAt b ◁ horizontal-comparison)) =₂ ((p ∙ left-image) ∙ eta)
left-normal = Normal.left-normal
right-normal : ((q ∙ (right-image ∙ K)) ∙ eta) =₂ (q ∙ point-boundary)
right-normal = Normal.right-normal
module From
(endpoint : (p ∙ (evAt b ◁ horizontal-comparison)) =₂ (q ∙ point-boundary)) where
private
corner : (p ∙ left-image) =₂ (q ∙ (right-image ∙ K))
corner = cancel-right eta ((right-normal ⁻¹) ∙ (endpoint ∙ (left-normal ⁻¹)))
compatible : ((q ⁻¹ ∙ p) ∙ left-image) =₂ (right-image ∙ K)
compatible = cancel-left q
(corner ∙ (comp₌-cong (comp-inv-left q p) (id₌ left-image) ∙
(comp₌-assoc q (q ⁻¹ ∙ p) left-image) ⁻¹))
value : ConeIdentification₁ Native.cone (framed-cone (evAt b) (evAt a) h k p q)
value = record { left = left; right = right; compatible = compatible }
corner-from-endpoint : {Γ : Context} {P C : CAT Γ}
(sigma : MAP P (Fun ([1] × [1]) C))
(a b : MAP One ([1] {Γ = Γ})) (h k : MAP P (Ar C)) {z : MAP P C}
(p : (evAt b ∘ h) =₁ z) (q : (evAt a ∘ k) =₁ z)
(left : Endpoints.At.Curried.Horizontal.side sigma a =₁ h)
(right : Endpoints.At.Curried.Vertical.side sigma b =₁ k)
→ (p ∙ (evAt b ◁ NativeCornerFromEndpoint.horizontal-comparison sigma a b h k p q left right))
=₂ (q ∙ NativeCornerFromEndpoint.point-boundary sigma a b h k p q left right)
→ ConeIdentification₁ (Endpoints.At.NativeCorner.cone sigma a b)
(framed-cone (evAt b) (evAt a) h k p q)
corner-from-endpoint {Γ = Γ} {P = P} {C = C} sigma a b h k p q left right endpoint =
NativeCornerFromEndpoint.From.value {Γ = Γ} {P = P} {C = C}
sigma a b h k p q left right endpoint
```
The two actual triangle restrictions share the diagonal restriction itself.
Each reflected face comparison has its own computation in the square diagram;
no inverse gluing or replacement of its matching is involved.
```agda
open import SCT.VolumeI.Chapter01.Section03.ProductConstructions using (productMap)
open import SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor using (productMap-cong)
open import SCT.VolumeI.Chapter01.Section03.Products.ProductRestriction using (product-restriction; restriction-compositor)
open import SCT.VolumeI.Chapter01.Section03.Identifications.Triangles using (post-triangle)
open import SCT.VolumeI.Chapter01.Section06.Cones using (cone-restrict)
open import SCT.VolumeI.Chapter01.Section06.ConeIdentifications using (cone-inverse)
open import SCT.VolumeI.Chapter01.Section06.FramedConeTransport using (module Corner)
open import SCT.VolumeI.Chapter01.Section07.Functoriality using (funPre; funPre-uncurry)
open import SCT.VolumeI.Chapter01.Section07.Currying using (reflect; reflect-β-One)
open import SCT.VolumeI.Chapter01.Section07.Evaluation using (evaluate-cong)
open import SCT.VolumeI.Chapter02.Section01.Morphisms using (insert; evAt-cong; evAt-pre)
open import SCT.VolumeI.Chapter02.Section01.WalkingTriangle
using ([2]; d₀; d₁; d₂; vertex₀; vertex₁; vertex₂;
d₂-zero; d₂-one; d₀-zero; d₀-one; d₁-zero; d₁-one)
open import SCT.VolumeI.Chapter02.Section01.SquareGluing
using (j₀; j₁; diagonal; j₀-d₂; j₀-d₀; j₁-d₂; j₁-d₀; j₀-diagonal; j₁-diagonal;
j₀-vertex₀; j₀-vertex₁; j₀-vertex₂; j₁-vertex₀; j₁-vertex₁; j₁-vertex₂)
open import SCT.VolumeI.Chapter02.Section02.SquareCoordinates using (coinsert)
open import SCT.VolumeI.Chapter02.Section02.SquareCorners using (module SquareCorner)
open import SCT.VolumeI.Chapter02.Section02.SquareVertexShapes using (module At)
open import SCT.VolumeI.Chapter02.Section02.TriangleCornerFrames using (module CornerRestriction; module TriangleCornerFrames)
open import SCT.VolumeI.Chapter02.Section01.Triangles using (triangle-cone; triangle-junction-vertex)
open import SCT.VolumeI.Chapter02.Section02.SquareBoundaryCones using (module Endpoint)
open import SCT.VolumeI.Chapter02.Section02.FramedTrianglePresentations using (TrianglePresentation; triangle-presentation)
private
module Geometry {Γ : Context} {P C : CAT Γ} (sigma : MAP P (Fun ([1] × [1]) C)) where
upper : MAP P (Fun [2] C)
upper = funPre j₀ ∘ sigma
lower : MAP P (Fun [2] C)
lower = funPre j₁ ∘ sigma
upper-leg : (funUncurry sigma ∘ product-restriction {P = P} j₀) =₁ funUncurry upper
upper-leg = (funPre-uncurry j₀ sigma) ⁻¹
lower-leg : (funUncurry sigma ∘ product-restriction {P = P} j₁) =₁ funUncurry lower
lower-leg = (funPre-uncurry j₁ sigma) ⁻¹
module Face (j : MAP [2] ([1] × [1]))
(triangle : MAP P (Fun [2] C))
(leg : (funUncurry sigma ∘ product-restriction {P = P} j) =₁ funUncurry triangle)
(d : MAP [1] [2]) (r : MAP [1] ([1] × [1]))
(shape : (j ∘ d) =₁ r) where
source : MAP P (Ar C)
source = funPre {D = C} r ∘ sigma
target : MAP P (Ar C)
target = funPre {D = C} d ∘ triangle
source-beta : funUncurry source =₁ (funUncurry sigma ∘ product-restriction {P = P} r)
source-beta = funPre-uncurry r sigma
target-beta : funUncurry target =₁ (funUncurry triangle ∘ product-restriction {P = P} d)
target-beta = funPre-uncurry d triangle
axis : (product-restriction {P = P} j ∘ product-restriction d) =₁ product-restriction r
axis = productMap-cong (id₌ (id P)) shape ∙ restriction-compositor d j
axis-route : ((funUncurry sigma ∘ product-restriction {P = P} j) ∘ product-restriction d)
=₁ (funUncurry sigma ∘ product-restriction r)
axis-route = post-triangle (funUncurry sigma) (product-restriction {P = P} j)
(product-restriction d) axis
diagram-comparison : funUncurry source =₁ funUncurry target
diagram-comparison = target-beta ⁻¹ ∙
((leg ▷ product-restriction {P = P} d) ∙ (axis-route ⁻¹ ∙ source-beta))
comparison : source =₁ target
comparison = reflect (funEval {C = [1]} {D = C}) (funUniversal [1] C)
source target diagram-comparison
image : evaluate-cong (funEval {C = [1]} {D = C}) comparison =₂ diagram-comparison
image = reflect-β-One (funEval {C = [1]} {D = C}) (funUniversal [1] C)
source target diagram-comparison
module Top = Face j₀ upper upper-leg d₂ (coinsert zero) j₀-d₂
module Right = Face j₀ upper upper-leg d₀ (insert one) j₀-d₀
module Left = Face j₁ lower lower-leg d₂ (insert zero) j₁-d₂
module Bottom = Face j₁ lower lower-leg d₀ (coinsert one) j₁-d₀
module UpperDiagonal = Face j₀ upper upper-leg d₁ diagonal j₀-diagonal
module LowerDiagonal = Face j₁ lower lower-leg d₁ diagonal j₁-diagonal
module Shapes = At {Γ = Γ}
module Frames = TriangleCornerFrames C
module UpperJunction = CornerRestriction ev₁ ev₀ (triangle-cone C)
(evAt-cong d₂-one ∙ evAt-pre one d₂)
(evAt-cong d₀-zero ∙ evAt-pre zero d₀) (triangle-junction-vertex C) upper
module LowerJunction = CornerRestriction ev₁ ev₀ (triangle-cone C)
(evAt-cong d₂-one ∙ evAt-pre one d₂)
(evAt-cong d₀-zero ∙ evAt-pre zero d₀) (triangle-junction-vertex C) lower
module UpperSourceFrames = Frames.Source upper
module LowerSourceFrames = Frames.Source lower
module UpperTargetFrames = Frames.Target upper
module LowerTargetFrames = Frames.Target lower
module TopSource = Endpoint sigma upper j₀ upper-leg
d₂ (coinsert zero) j₀-d₂ zero vertex₀ (SquareCorner.vertex zero zero)
d₂-zero j₀-vertex₀ (SquareCorner.horizontal-vertex zero zero) Shapes.UpperFirstSource.comparison
module TopSourceComparison = TopSource.WithComparison Top.comparison Top.image
module TopTarget = Endpoint sigma upper j₀ upper-leg
d₂ (coinsert zero) j₀-d₂ one vertex₁ (SquareCorner.vertex zero one)
d₂-one j₀-vertex₁ (SquareCorner.horizontal-vertex zero one) Shapes.UpperFirstTarget.comparison
module TopTargetComparison = TopTarget.WithComparison Top.comparison Top.image
module RightSource = Endpoint sigma upper j₀ upper-leg
d₀ (insert one) j₀-d₀ zero vertex₁ (SquareCorner.vertex zero one)
d₀-zero j₀-vertex₁ (SquareCorner.vertical-vertex zero one) Shapes.UpperSecondSource.comparison
module RightSourceComparison = RightSource.WithComparison Right.comparison Right.image
module RightTarget = Endpoint sigma upper j₀ upper-leg
d₀ (insert one) j₀-d₀ one vertex₂ (SquareCorner.vertex one one)
d₀-one j₀-vertex₂ (SquareCorner.vertical-vertex one one) Shapes.UpperSecondTarget.comparison
module RightTargetComparison = RightTarget.WithComparison Right.comparison Right.image
module UpperDiagonalSource = Endpoint sigma upper j₀ upper-leg
d₁ diagonal j₀-diagonal zero vertex₀ (SquareCorner.vertex zero zero)
d₁-zero j₀-vertex₀ (Shapes.diagonal-vertex zero) Shapes.UpperDiagonalSource.comparison
module UpperDiagonalSourceComparison = UpperDiagonalSource.WithComparison UpperDiagonal.comparison UpperDiagonal.image
module UpperDiagonalTarget = Endpoint sigma upper j₀ upper-leg
d₁ diagonal j₀-diagonal one vertex₂ (SquareCorner.vertex one one)
d₁-one j₀-vertex₂ (Shapes.diagonal-vertex one) Shapes.UpperDiagonalTarget.comparison
module UpperDiagonalTargetComparison = UpperDiagonalTarget.WithComparison UpperDiagonal.comparison UpperDiagonal.image
module LeftSource = Endpoint sigma lower j₁ lower-leg
d₂ (insert zero) j₁-d₂ zero vertex₀ (SquareCorner.vertex zero zero)
d₂-zero j₁-vertex₀ (SquareCorner.vertical-vertex zero zero) Shapes.LowerFirstSource.comparison
module LeftSourceComparison = LeftSource.WithComparison Left.comparison Left.image
module LeftTarget = Endpoint sigma lower j₁ lower-leg
d₂ (insert zero) j₁-d₂ one vertex₁ (SquareCorner.vertex one zero)
d₂-one j₁-vertex₁ (SquareCorner.vertical-vertex one zero) Shapes.LowerFirstTarget.comparison
module LeftTargetComparison = LeftTarget.WithComparison Left.comparison Left.image
module BottomSource = Endpoint sigma lower j₁ lower-leg
d₀ (coinsert one) j₁-d₀ zero vertex₁ (SquareCorner.vertex one zero)
d₀-zero j₁-vertex₁ (SquareCorner.horizontal-vertex one zero) Shapes.LowerSecondSource.comparison
module BottomSourceComparison = BottomSource.WithComparison Bottom.comparison Bottom.image
module BottomTarget = Endpoint sigma lower j₁ lower-leg
d₀ (coinsert one) j₁-d₀ one vertex₂ (SquareCorner.vertex one one)
d₀-one j₁-vertex₂ (SquareCorner.horizontal-vertex one one) Shapes.LowerSecondTarget.comparison
module BottomTargetComparison = BottomTarget.WithComparison Bottom.comparison Bottom.image
module LowerDiagonalSource = Endpoint sigma lower j₁ lower-leg
d₁ diagonal j₁-diagonal zero vertex₀ (SquareCorner.vertex zero zero)
d₁-zero j₁-vertex₀ (Shapes.diagonal-vertex zero) Shapes.LowerDiagonalSource.comparison
module LowerDiagonalSourceComparison = LowerDiagonalSource.WithComparison LowerDiagonal.comparison LowerDiagonal.image
module LowerDiagonalTarget = Endpoint sigma lower j₁ lower-leg
d₁ diagonal j₁-diagonal one vertex₂ (SquareCorner.vertex one one)
d₁-one j₁-vertex₂ (Shapes.diagonal-vertex one) Shapes.LowerDiagonalTarget.comparison
module LowerDiagonalTargetComparison = LowerDiagonalTarget.WithComparison LowerDiagonal.comparison LowerDiagonal.image
module UpperMiddle = Corner ev₁ ev₀ (cone-restrict upper (triangle-cone C))
TopTarget.Source.frame RightSource.Source.frame TopTarget.Target.frame RightSource.Target.frame
UpperJunction.compatibility Top.comparison Right.comparison TopTarget.vertex
TopTargetComparison.compatible RightSourceComparison.compatible
module LowerMiddle = Corner ev₁ ev₀ (cone-restrict lower (triangle-cone C))
LeftTarget.Source.frame BottomSource.Source.frame LeftTarget.Target.frame BottomSource.Target.frame
LowerJunction.compatibility Left.comparison Bottom.comparison LeftTarget.vertex
LeftTargetComparison.compatible BottomSourceComparison.compatible
module UpperSource = Corner ev₀ ev₀ (cone-restrict upper (Frames.source-cone))
UpperDiagonalSource.Source.frame TopSource.Source.frame UpperDiagonalSource.Target.frame TopSource.Target.frame
UpperSourceFrames.compatibility UpperDiagonal.comparison Top.comparison UpperDiagonalSource.vertex
UpperDiagonalSourceComparison.compatible TopSourceComparison.compatible
module LowerSource = Corner ev₀ ev₀ (cone-restrict lower (Frames.source-cone))
LowerDiagonalSource.Source.frame LeftSource.Source.frame LowerDiagonalSource.Target.frame LeftSource.Target.frame
LowerSourceFrames.compatibility LowerDiagonal.comparison Left.comparison LowerDiagonalSource.vertex
LowerDiagonalSourceComparison.compatible LeftSourceComparison.compatible
module UpperTarget = Corner ev₁ ev₁ (cone-restrict upper (Frames.target-cone))
UpperDiagonalTarget.Source.frame RightTarget.Source.frame UpperDiagonalTarget.Target.frame RightTarget.Target.frame
UpperTargetFrames.compatibility UpperDiagonal.comparison Right.comparison UpperDiagonalTarget.vertex
UpperDiagonalTargetComparison.compatible RightTargetComparison.compatible
module LowerTarget = Corner ev₁ ev₁ (cone-restrict lower (Frames.target-cone))
LowerDiagonalTarget.Source.frame BottomTarget.Source.frame LowerDiagonalTarget.Target.frame BottomTarget.Target.frame
LowerTargetFrames.compatibility LowerDiagonal.comparison Bottom.comparison LowerDiagonalTarget.vertex
LowerDiagonalTargetComparison.compatible BottomTargetComparison.compatible
x y w z : MAP P C
x = evAt (SquareCorner.vertex zero zero) ∘ sigma
y = evAt (SquareCorner.vertex zero one) ∘ sigma
w = evAt (SquareCorner.vertex one zero) ∘ sigma
z = evAt (SquareCorner.vertex one one) ∘ sigma
top : MorphismFamily x y
top = record { arrow = Top.source; source-frame = TopSource.Source.frame; target-frame = TopTarget.Source.frame }
right : MorphismFamily y z
right = record { arrow = Right.source; source-frame = RightSource.Source.frame; target-frame = RightTarget.Source.frame }
left : MorphismFamily x w
left = record { arrow = Left.source; source-frame = LeftSource.Source.frame; target-frame = LeftTarget.Source.frame }
bottom : MorphismFamily w z
bottom = record { arrow = Bottom.source; source-frame = BottomSource.Source.frame; target-frame = BottomTarget.Source.frame }
long : MorphismFamily x z
long = record { arrow = UpperDiagonal.source; source-frame = UpperDiagonalSource.Source.frame; target-frame = UpperDiagonalTarget.Source.frame }
upper-presentation : TrianglePresentation top right long
upper-presentation = triangle-presentation upper
(Top.comparison ⁻¹) (Right.comparison ⁻¹) (UpperDiagonal.comparison ⁻¹)
(ConeIdentification₁.compatible (cone-inverse UpperMiddle.comparison))
(ConeIdentification₁.compatible (cone-inverse UpperSource.comparison))
(ConeIdentification₁.compatible (cone-inverse UpperTarget.comparison))
lower-presentation : TrianglePresentation left bottom long
lower-presentation = triangle-presentation lower
(Left.comparison ⁻¹) (Bottom.comparison ⁻¹) (LowerDiagonal.comparison ⁻¹)
(ConeIdentification₁.compatible (cone-inverse LowerMiddle.comparison))
(ConeIdentification₁.compatible (cone-inverse LowerSource.comparison))
(ConeIdentification₁.compatible (cone-inverse LowerTarget.comparison))
```
The native corner comparison supplies the change of its vertex. Its other
leg then has that same vertex image by the complete matching equation.
This transfers the two whole presentations to the original four families.
```agda
open import SCT.VolumeI.Chapter01.Section02.Specialization using (inv-comp-left; inv-comp-right)
open import SCT.VolumeI.Chapter02.Section01.MorphismFamilyOperations
using (family-comparison; retarget-family; retarget-family-comparison; module FamilyComparison)
open import SCT.VolumeI.Chapter02.Section01.MorphismFamilyComparisons
using (compose-family-comparisons; inverse-family-comparison; id-family-comparison)
open import SCT.VolumeI.Chapter02.Section01.MorphismFamilyPostcomposition using (post-family-comparison)
open import SCT.VolumeI.Chapter02.Section02.FramedSquares using (FramedSquare; framed-image; module SquareFamily)
open import SCT.VolumeI.Chapter02.Section02.FramedTrianglePresentations
using (module RetargetPresentation; presented-composition)
open import SCT.VolumeI.Chapter02.Section02.TrianglePresentationChange using (module ReplacePresentation)
open import SCT.VolumeI.Chapter02.Section01.Triangles using (short-edges)
import SCT.VolumeI.Chapter02.Section02.MorphismComposition as MC
private
module NativeVertexChange {Γ : Context} {P A B C : CAT Γ}
(f : MAP A C) (g : MAP B C) (native : Cone f g P)
{v z : MAP P C} {h : MAP P A} {k : MAP P B}
(p₀ : (f ∘ Cone.left native) =₁ v) (q₀ : (g ∘ Cone.right native) =₁ v)
(junction : (q₀ ∙ Cone.match native) =₂ p₀)
(p : (f ∘ h) =₁ z) (q : (g ∘ k) =₁ z)
(given : ConeIdentification₁ native (framed-cone f g h k p q)) where
left = ConeIdentification₁.left given
right = ConeIdentification₁.right given
private
L = f ◁ left
R = g ◁ right
K = Cone.match native
vertex : v =₁ z
vertex = q ∙ (R ∙ q₀ ⁻¹)
right-endpoint : (q ∙ R) =₂ (vertex ∙ q₀)
right-endpoint =
(comp₌-cong (id₌ q) (inv-comp-right R q₀) ∙
comp₌-assoc q (R ∙ q₀ ⁻¹) q₀) ⁻¹
private
quotient : (q₀ ⁻¹ ∙ p₀) =₂ K
quotient = inv-comp-left q₀ K ∙ comp₌-cong (id₌ (q₀ ⁻¹)) (junction ⁻¹)
corner : (p ∙ L) =₂ (q ∙ (R ∙ K))
corner = comp₌-cong (id₌ q) (ConeIdentification₁.compatible given) ∙
(comp₌-assoc q (q ⁻¹ ∙ p) L ∙
(comp₌-cong (comp-inv-left q p) (id₌ L)) ⁻¹)
vertex-normal : (vertex ∙ p₀) =₂ (q ∙ (R ∙ K))
vertex-normal = comp₌-cong (id₌ q) (comp₌-cong (id₌ R) quotient) ∙
(comp₌-cong (id₌ q) (comp₌-assoc R (q₀ ⁻¹) p₀) ∙
comp₌-assoc q (R ∙ q₀ ⁻¹) p₀)
left-endpoint : (p ∙ L) =₂ (vertex ∙ p₀)
left-endpoint = vertex-normal ⁻¹ ∙ corner
module RecoverBoundary {Γ : Context} {P C : CAT Γ} {x y z w : MAP P C}
{top : MorphismFamily x y} {right : MorphismFamily y z}
{left : MorphismFamily x w} {bottom : MorphismFamily w z}
(given : FramedSquare top right left bottom) where
module S = SquareFamily given
module N = MorphismFamily S.vertical
module T = MorphismFamily top
module R = MorphismFamily right
module L = MorphismFamily left
module B = MorphismFamily bottom
module Recover = Recovery {Γ = Γ} {P = P} {C = C} N.arrow
module Curried = Recover.Curried
square : MAP P (Fun ([1] × [1]) C)
square = Recover.square
epsilon : Curried.nested =₁ N.arrow
epsilon = Recover.comparison
left-frame : (ev₀ {C = Ar C} ∘ Curried.nested) =₁ L.arrow
left-frame = N.source-frame ∙ (ev₀ ◁ epsilon)
right-frame : (ev₁ {C = Ar C} ∘ Curried.nested) =₁ R.arrow
right-frame = N.target-frame ∙ (ev₁ ◁ epsilon)
left-side : Curried.Vertical.side zero =₁ L.arrow
left-side = left-frame ∙ (Curried.Vertical.boundary zero) ⁻¹
right-side : Curried.Vertical.side one =₁ R.arrow
right-side = right-frame ∙ (Curried.Vertical.boundary one) ⁻¹
recovered-vertical : MorphismFamily L.arrow R.arrow
recovered-vertical = record
{ arrow = Curried.nested
; source-frame = left-side ∙ Curried.Vertical.boundary zero
; target-frame = right-side ∙ Curried.Vertical.boundary one }
vertical-comparison : MorphismFamilyIdentification One recovered-vertical S.vertical
vertical-comparison = family-comparison recovered-vertical S.vertical epsilon
((inv-comp-right left-frame (Curried.Vertical.boundary zero)) ⁻¹)
((inv-comp-right right-frame (Curried.Vertical.boundary one)) ⁻¹)
top-edge : MorphismFamilyIdentification One
(framed-image (ev₀ {C = C}) recovered-vertical L.source-frame R.source-frame) top
top-edge = compose-family-comparisons S.top-edge
(retarget-family-comparison L.source-frame R.source-frame
(post-family-comparison (ev₀ {C = C}) vertical-comparison))
bottom-edge : MorphismFamilyIdentification One
(framed-image (ev₁ {C = C}) recovered-vertical L.target-frame R.target-frame) bottom
bottom-edge = compose-family-comparisons S.bottom-edge
(retarget-family-comparison L.target-frame R.target-frame
(post-family-comparison (ev₁ {C = C}) vertical-comparison))
module Top = FamilyComparison top-edge
module Bottom = FamilyComparison bottom-edge
top-side : Curried.Horizontal.side zero =₁ T.arrow
top-side = Top.identification ∙ (Curried.Horizontal.comparison zero) ⁻¹
bottom-side : Curried.Horizontal.side one =₁ B.arrow
bottom-side = Bottom.identification ∙ (Curried.Horizontal.comparison one) ⁻¹
top-image : (top-side ∙ Curried.Horizontal.comparison zero) =₂ Top.identification
top-image = inv-comp-right Top.identification (Curried.Horizontal.comparison zero)
bottom-image : (bottom-side ∙ Curried.Horizontal.comparison one) =₂ Bottom.identification
bottom-image = inv-comp-right Bottom.identification (Curried.Horizontal.comparison one)
native₀₀ : ConeIdentification₁ (Endpoints.At.NativeCorner.cone square zero zero)
(framed-cone ev₀ ev₀ T.arrow L.arrow T.source-frame L.source-frame)
native₀₀ = corner-from-endpoint {Γ = Γ} {P = P} {C = C} square zero zero T.arrow L.arrow
T.source-frame L.source-frame top-side left-side
(Top.source ∙ comp₌-cong (id₌ T.source-frame) (postWhisker ev₀ ◁ top-image))
native₀₁ : ConeIdentification₁ (Endpoints.At.NativeCorner.cone square zero one)
(framed-cone ev₁ ev₀ T.arrow R.arrow T.target-frame R.source-frame)
native₀₁ = corner-from-endpoint {Γ = Γ} {P = P} {C = C} square zero one T.arrow R.arrow
T.target-frame R.source-frame top-side right-side
(Top.target ∙ comp₌-cong (id₌ T.target-frame) (postWhisker ev₁ ◁ top-image))
native₁₀ : ConeIdentification₁ (Endpoints.At.NativeCorner.cone square one zero)
(framed-cone ev₀ ev₁ B.arrow L.arrow B.source-frame L.target-frame)
native₁₀ = corner-from-endpoint {Γ = Γ} {P = P} {C = C} square one zero B.arrow L.arrow
B.source-frame L.target-frame bottom-side left-side
(Bottom.source ∙ comp₌-cong (id₌ B.source-frame) (postWhisker ev₀ ◁ bottom-image))
native₁₁ : ConeIdentification₁ (Endpoints.At.NativeCorner.cone square one one)
(framed-cone ev₁ ev₁ B.arrow R.arrow B.target-frame R.target-frame)
native₁₁ = corner-from-endpoint {Γ = Γ} {P = P} {C = C} square one one B.arrow R.arrow
B.target-frame R.target-frame bottom-side right-side
(Bottom.target ∙ comp₌-cong (id₌ B.target-frame) (postWhisker ev₁ ◁ bottom-image))
```
```agda
private
module BoundaryPresentations {Γ : Context} {P C : CAT Γ} {x y z w : MAP P C}
{top : MorphismFamily x y} {right : MorphismFamily y z}
{left : MorphismFamily x w} {bottom : MorphismFamily w z}
(given : FramedSquare top right left bottom) where
module Recovered = RecoverBoundary given
module G = Geometry Recovered.square
using (x; y; w; z; top; right; left; bottom; long; upper-presentation; lower-presentation)
module T = MorphismFamily top
module R = MorphismFamily right
module L = MorphismFamily left
module B = MorphismFamily bottom
module NativeFrames (a b : MAP One ([1] {Γ = Γ})) where
module Shape = SquareCorner a b
module E = Shape.Evaluated C
module Frames = CornerRestriction (evAt b) (evAt a) E.cone
E.horizontal E.vertical E.vertex-equation Recovered.square
module Frames₀₀ = NativeFrames zero zero
module Frames₀₁ = NativeFrames zero one
module Frames₁₀ = NativeFrames one zero
module Frames₁₁ = NativeFrames one one
module Vertex₀₀ = NativeVertexChange ev₀ ev₀ (Endpoints.At.NativeCorner.cone Recovered.square zero zero)
Frames₀₀.Frames.left-frame Frames₀₀.Frames.right-frame Frames₀₀.Frames.compatibility
T.source-frame L.source-frame Recovered.native₀₀
module Vertex₀₁ = NativeVertexChange ev₁ ev₀ (Endpoints.At.NativeCorner.cone Recovered.square zero one)
Frames₀₁.Frames.left-frame Frames₀₁.Frames.right-frame Frames₀₁.Frames.compatibility
T.target-frame R.source-frame Recovered.native₀₁
module Vertex₁₀ = NativeVertexChange ev₀ ev₁ (Endpoints.At.NativeCorner.cone Recovered.square one zero)
Frames₁₀.Frames.left-frame Frames₁₀.Frames.right-frame Frames₁₀.Frames.compatibility
B.source-frame L.target-frame Recovered.native₁₀
module Vertex₁₁ = NativeVertexChange ev₁ ev₁ (Endpoints.At.NativeCorner.cone Recovered.square one one)
Frames₁₁.Frames.left-frame Frames₁₁.Frames.right-frame Frames₁₁.Frames.compatibility
B.target-frame R.target-frame Recovered.native₁₁
x-change : G.x =₁ x
x-change = Vertex₀₀.vertex
y-change : G.y =₁ y
y-change = Vertex₀₁.vertex
w-change : G.w =₁ w
w-change = Vertex₁₀.vertex
z-change : G.z =₁ z
z-change = Vertex₁₁.vertex
top-comparison : MorphismFamilyIdentification One (retarget-family G.top x-change y-change) top
top-comparison = family-comparison _ top Recovered.top-side
Vertex₀₀.left-endpoint Vertex₀₁.left-endpoint
right-comparison : MorphismFamilyIdentification One (retarget-family G.right y-change z-change) right
right-comparison = family-comparison _ right Recovered.right-side
Vertex₀₁.right-endpoint Vertex₁₁.right-endpoint
left-comparison : MorphismFamilyIdentification One (retarget-family G.left x-change w-change) left
left-comparison = family-comparison _ left Recovered.left-side
Vertex₀₀.right-endpoint Vertex₁₀.right-endpoint
bottom-comparison : MorphismFamilyIdentification One (retarget-family G.bottom w-change z-change) bottom
bottom-comparison = family-comparison _ bottom Recovered.bottom-side
Vertex₁₀.left-endpoint Vertex₁₁.left-endpoint
long : MorphismFamily x z
long = retarget-family G.long x-change z-change
upper : TrianglePresentation top right long
upper = ReplacePresentation.value
(RetargetPresentation.value G.upper-presentation x-change y-change z-change)
top-comparison right-comparison (id-family-comparison long)
lower : TrianglePresentation left bottom long
lower = ReplacePresentation.value
(RetargetPresentation.value G.lower-presentation x-change w-change z-change)
left-comparison bottom-comparison (id-family-comparison long)
module _ {Γ : Context} where
comparison : (C : CAT Γ) (segal : IsEquiv (short-edges C))
{P : CAT Γ} {x y z w : MAP P C}
{top : MorphismFamily x y} {right : MorphismFamily y z}
{left : MorphismFamily x w} {bottom : MorphismFamily w z}
→ FramedSquare top right left bottom
→ MorphismFamilyIdentification One
(MC.Composition.compose C segal bottom left)
(MC.Composition.compose C segal right top)
comparison C segal {top = top} {right} {left} {bottom} given =
compose-family-comparisons
(inverse-family-comparison (presented-composition segal top right Presentations.long Presentations.upper))
(presented-composition segal left bottom Presentations.long Presentations.lower)
where module Presentations = BoundaryPresentations given using (long; upper; lower)
```