Other Agda modules in this section (27)
- ConeFramings
- ConeIdentifications
- ConeTransport
- ConeUniversality
- Cones
- CoproductDescent
- DiagonalPullbacks
- DisjointCoproducts
- Distributivity
- EmbeddingCharacterizations
- Embeddings
- MappingPullbacks
- NestedPullbacks
- PastingLemma
- PullbackArrowChange
- PullbackAssociativity
- PullbackCancellation
- PullbackConstructions
- PullbackFunctoriality
- PullbackSquares
- PullbackTransfer
- Pullbacks
- Representability
- RepresentabilityDiagonal
- SectionBaseChange
- UniversalConeIdentifications
- UniversalCoproducts
Chapter 1, rebuild2, checked 14 October 2026 · source revision b982f5a.
# Pasting cones Pasting retains the selected inner matching and the selected outer matching. Postcomposing the left leg exposes their composition. Its complete comparison with the restricted outer cone is the input used by nested insertion. ```agda {-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section06.ConePasting where open import SCT.VolumeI.Chapter01.Section01.Vocabulary open Operations open import SCT.VolumeI.Chapter01.Section02.Coherence using (id₌; postWhisker-id₌; preWhisker-id₌; comp-assoc; module Composition; module Boundaries) open Composition open Boundaries using (SquareCell₌) open import SCT.VolumeI.Chapter01.Section02.Specialization open import SCT.VolumeI.Chapter01.Section02.IdentificationSquares open import SCT.VolumeI.Chapter01.Section02.Whiskering using (postWhisker-comp) open import SCT.VolumeI.Chapter01.Section03.Identifications.Inverses using (comp₌-unitˡ-One; comp₌-unitʳ-One; comp₌-inverseʳ-One; postWhisker-inverse; comp₌-inverseˡ-One; inverse-identity; solve-pentagon; preWhisker-inverse) open import SCT.VolumeI.Chapter01.Section03.Identifications.FunctorCoherence using (pentagon-whiskered) open import SCT.VolumeI.Chapter01.Section06.ConeIdentifications using (cone-action-One; cone-compose; cone-inverse; cone-identification-restrict-One; cone-restrict-assoc) open import SCT.VolumeI.Chapter01.Section06.Cones module _ {Γ : Context} where postcompose-cone-left : {A B X Z T : CAT Γ} (f : MAP A B) (g : MAP B Z) {h : MAP X Z} → Cone (g ∘ f) h T → Cone g h T postcompose-cone-left f g s = record { left = f ∘ Cone.left s; right = Cone.right s ; match = Cone.match s ∙ (comp-assoc (Cone.left s) f g) ⁻¹ } postcompose-cone-left-identification : {A B X Z T : CAT Γ} (f : MAP A B) (g : MAP B Z) {h : MAP X Z} {s t : Cone (g ∘ f) h T} → ConeIdentification₁ s t → ConeIdentification₁ (postcompose-cone-left f g s) (postcompose-cone-left f g t) postcompose-cone-left-identification f g Φ = record { left = f ◁ ConeIdentification₁.left Φ ; right = ConeIdentification₁.right Φ ; compatible = paste-square₌ (inverse-square₌ (unconst-sides₌ (postWhisker-comp (ConeIdentification₁.left Φ) f g))) (ConeIdentification₁.compatible Φ) } postcompose-cone-left-reflect : {A B X Z T : CAT Γ} (f : MAP A B) (g : MAP B Z) {h : MAP X Z} (s t : Cone (g ∘ f) h T) (α : Cone.left s =₁ Cone.left t) (β : Cone.right s =₁ Cone.right t) → SquareCell₌ (g ◁ (f ◁ α)) (h ◁ β) (Cone.match (postcompose-cone-left f g s)) (Cone.match (postcompose-cone-left f g t)) → ConeIdentification₁ s t postcompose-cone-left-reflect f g s t α β square = record { left = α; right = β ; compatible = replace-sides₌ (inv-comp-right (Cone.match s) (comp-assoc (Cone.left s) f g)) (inv-comp-right (Cone.match t) (comp-assoc (Cone.left t) f g)) (paste-square₌ (unconst-sides₌ (postWhisker-comp α f g)) square) } postcompose-cone-left-restrict : {A B X Z R T : CAT Γ} (f : MAP A B) (g : MAP B Z) {h : MAP X Z} (r : MAP R T) (s : Cone (g ∘ f) h T) → ConeIdentification₁ (cone-restrict r (postcompose-cone-left f g s)) (postcompose-cone-left f g (cone-restrict r s)) postcompose-cone-left-restrict f g {h} r s = record { left = comp-assoc r (Cone.left s) f ; right = id₌ (Cone.right s ∘ r) ; compatible = comp₌-cong ((postWhisker-id₌ h (Cone.right s ∘ r)) ⁻¹) (id₌ source-match) ∙ ((comp₌-unitˡ-One source-match) ⁻¹ ∙ (source-normal ⁻¹ ∙ target-normal)) } where original-left = comp-assoc (Cone.left s) f g composite-left = comp-assoc r (Cone.left s) (g ∘ f) inner-left = comp-assoc r (f ∘ Cone.left s) g final-left = comp-assoc (Cone.left s ∘ r) f g outer-right = comp-assoc r (Cone.right s) h match-at-r = Cone.match s ▷ r corner = solve-pentagon final-left composite-left (g ◁ comp-assoc r (Cone.left s) f) inner-left (original-left ▷ r) (pentagon-whiskered r (Cone.left s) f g) tail = ((original-left ▷ r) ⁻¹) ∙ (inner-left ⁻¹) source-match = Cone.match (cone-restrict r (postcompose-cone-left f g s)) target-match = Cone.match (postcompose-cone-left f g (cone-restrict r s)) source-normal : source-match =₂ (outer-right ∙ (match-at-r ∙ tail)) source-normal = comp₌-cong (id₌ outer-right) (comp₌-assoc match-at-r ((original-left ▷ r) ⁻¹) (inner-left ⁻¹) ∙ comp₌-cong (comp₌-cong (id₌ match-at-r) (preWhisker-inverse original-left r) ∙ preWhisker-comp₌ (Cone.match s) (original-left ⁻¹) r) (id₌ (inner-left ⁻¹))) target-normal : (target-match ∙ (g ◁ comp-assoc r (Cone.left s) f)) =₂ (outer-right ∙ (match-at-r ∙ tail)) target-normal = comp₌-cong (id₌ outer-right) (comp₌-cong (id₌ match-at-r) (inv-comp-left composite-left tail) ∙ (comp₌-assoc match-at-r (composite-left ⁻¹) (composite-left ∙ tail) ∙ comp₌-cong (id₌ (match-at-r ∙ composite-left ⁻¹)) (corner ⁻¹))) ∙ (comp₌-assoc outer-right (match-at-r ∙ composite-left ⁻¹) ((final-left ⁻¹) ∙ (g ◁ comp-assoc r (Cone.left s) f)) ∙ comp₌-assoc (outer-right ∙ (match-at-r ∙ composite-left ⁻¹)) (final-left ⁻¹) (g ◁ comp-assoc r (Cone.left s) f)) module PasteCones {A B X Z Q : CAT Γ} (f : MAP A B) (g : MAP B Z) {h : MAP X Z} (t : Cone g h Q) where paste : {T : CAT Γ} → Cone f (Cone.left t) T → Cone (g ∘ f) h T paste s = record { left = Cone.left s; right = Cone.right t ∘ Cone.right s ; match = Cone.match (cone-restrict (Cone.right s) t) ∙ ((g ◁ Cone.match s) ∙ comp-assoc (Cone.left s) f g) } paste-match : {T : CAT Γ} (s : Cone f (Cone.left t) T) → Cone.match (postcompose-cone-left f g (paste s)) =₂ (Cone.match (cone-restrict (Cone.right s) t) ∙ (g ◁ Cone.match s)) paste-match s = comp-inv-right (Cone.match (cone-restrict (Cone.right s) t) ∙ (g ◁ Cone.match s)) (comp-assoc (Cone.left s) f g) ∙ comp₌-cong ((comp₌-assoc (Cone.match (cone-restrict (Cone.right s) t)) (g ◁ Cone.match s) (comp-assoc (Cone.left s) f g)) ⁻¹) (id₌ ((comp-assoc (Cone.left s) f g) ⁻¹)) postcompose-paste : {T : CAT Γ} (s : Cone f (Cone.left t) T) → ConeIdentification₁ (postcompose-cone-left f g (paste s)) (cone-restrict (Cone.right s) t) postcompose-paste s = record { left = Cone.match s; right = id₌ (Cone.right t ∘ Cone.right s) ; compatible = comp₌-cong ((postWhisker-id₌ h (Cone.right t ∘ Cone.right s)) ⁻¹) (id₌ (Cone.match (postcompose-cone-left f g (paste s)))) ∙ ((comp₌-unitˡ-One (Cone.match (postcompose-cone-left f g (paste s)))) ⁻¹ ∙ (paste-match s) ⁻¹) } ``` ```agda paste-identification : {T : CAT Γ} {s s′ : Cone f (Cone.left t) T} → ConeIdentification₁ s s′ → ConeIdentification₁ (paste s) (paste s′) paste-identification {s = s} {s′} Φ = postcompose-cone-left-reflect f g (paste s) (paste s′) (ConeIdentification₁.left Φ) (Cone.right t ◁ ConeIdentification₁.right Φ) (replace-sides₌ ((paste-match s) ⁻¹) ((paste-match s′) ⁻¹) (paste-square₌ (post-square₌ g (ConeIdentification₁.compatible Φ)) (ConeIdentification₁.compatible (cone-action-One t (ConeIdentification₁.right Φ))))) ``` ```agda paste-restrict : {S T : CAT Γ} (r : MAP S T) (s : Cone f (Cone.left t) T) → ConeIdentification₁ (cone-restrict r (paste s)) (paste (cone-restrict r s)) paste-restrict r s = postcompose-cone-left-reflect f g _ _ (id₌ (Cone.left s ∘ r)) right-associator (replace-edges₌ left-normal (postWhisker h ◁ right-normal) (ConeIdentification₁.compatible raw)) where right-associator = comp-assoc r (Cone.right s) (Cone.right t) restricted-matching = Cone.match (cone-restrict r s) raw = cone-compose (cone-inverse (postcompose-paste (cone-restrict r s))) (cone-compose (cone-restrict-assoc r (Cone.right s) t) (cone-compose (cone-identification-restrict-One r (postcompose-paste s)) (cone-inverse (postcompose-cone-left-restrict f g r (paste s))))) left-normal : (g ◁ ConeIdentification₁.left raw) =₂ (g ◁ (f ◁ id₌ (Cone.left s ∘ r))) left-normal = postWhisker g ◁ ((postWhisker-id₌ f (Cone.left s ∘ r)) ⁻¹ ∙ comp₌-inverseˡ-One restricted-matching) right-normal : ConeIdentification₁.right raw =₂ right-associator right-normal = comp₌-unitˡ-One right-associator ∙ comp₌-cong (inverse-identity (Cone.right t ∘ (Cone.right s ∘ r))) (comp₌-unitʳ-One right-associator ∙ comp₌-cong (id₌ right-associator) (comp₌-unitˡ-One (id₌ ((Cone.right t ∘ Cone.right s) ∘ r)) ∙ comp₌-cong (preWhisker-id₌ (Cone.right t ∘ Cone.right s) r) (inverse-identity ((Cone.right t ∘ Cone.right s) ∘ r)))) ``` ## Factoring a postcomposed cone A complete comparison with the supplied outer cone determines the top cone by its inverse left leg. Pasting that cone recovers the original cone, with identity left component and the supplied right component. ```agda factor-cone : {T : CAT Γ} (s : Cone (g ∘ f) h T) (k : MAP T Q) → ConeIdentification₁ (cone-restrict k t) (postcompose-cone-left f g s) → Cone f (Cone.left t) T factor-cone s k Φ = record { left = Cone.left s; right = k; match = (ConeIdentification₁.left Φ) ⁻¹ } paste-factor : {T : CAT Γ} (s : Cone (g ∘ f) h T) (k : MAP T Q) (Φ : ConeIdentification₁ (cone-restrict k t) (postcompose-cone-left f g s)) → ConeIdentification₁ (paste (factor-cone s k Φ)) s paste-factor s k Φ = postcompose-cone-left-reflect f g _ _ (id₌ (Cone.left s)) (ConeIdentification₁.right Φ) (comp₌-cong (id₌ (h ◁ ConeIdentification₁.right Φ)) ((paste-match (factor-cone s k Φ)) ⁻¹) ∙ (comp₌-assoc (h ◁ ConeIdentification₁.right Φ) restricted-match (g ◁ left-cell ⁻¹) ∙ (cancellation ⁻¹ ∙ (comp₌-unitʳ-One target-match ∙ comp₌-cong (id₌ target-match) (postWhisker-id₌ g (f ∘ Cone.left s) ∙ (postWhisker g ◁ postWhisker-id₌ f (Cone.left s))))))) where left-cell = ConeIdentification₁.left Φ restricted-match = Cone.match (cone-restrict k t) target-match = Cone.match (postcompose-cone-left f g s) inverse-image = comp₌-inverseʳ-One (g ◁ left-cell) ∙ comp₌-cong (id₌ (g ◁ left-cell)) (postWhisker-inverse g left-cell) cancellation : (((h ◁ ConeIdentification₁.right Φ) ∙ restricted-match) ∙ (g ◁ left-cell ⁻¹)) =₂ target-match cancellation = comp₌-unitʳ-One target-match ∙ (comp₌-cong (id₌ target-match) inverse-image ∙ (comp₌-assoc target-match (g ◁ left-cell) (g ◁ left-cell ⁻¹) ∙ comp₌-cong ((ConeIdentification₁.compatible Φ) ⁻¹) (id₌ (g ◁ left-cell ⁻¹)))) ```