SCT.VolumeI.Chapter01.Section07.FunctorConeRestriction

Other Agda modules in this section (16)
Chapter 1, rebuild2, checked 14 October 2026 · source revision b982f5a.
Corresponding book passages
Uncurrying respects the specified matching
# Restricting a natively evaluated cone

The complete restriction comparison uses the actual postcomposition
substitution squares and native evaluation of the specified matching.
Endpoint transport assembles their square. The component comparisons are
the existing selected `evaluate-restrict` triangles.

```agda
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter01.Section07.FunctorConeRestriction where

open import SCT.VolumeI.Chapter01.Section01.Vocabulary hiding (_＝_)
import SCT.VolumeI.Chapter01.Section01.Terms as Terms
open Terms using (Equal)
open Operations
open import SCT.VolumeI.Chapter01.Section01.Terminal
open Constructions
open import SCT.VolumeI.Chapter01.Section02.Coherence using (id₌; inv₌; 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.Section03.ProductConstructions
open import SCT.VolumeI.Chapter01.Section03.Identifications.EndpointTransport
open import SCT.VolumeI.Chapter01.Section03.Identifications.Inverses
  using (inverse-unique; preWhisker-inverse)
open import SCT.VolumeI.Chapter01.Section06.Cones
open import SCT.VolumeI.Chapter01.Section07.Evaluation
open import SCT.VolumeI.Chapter01.Section07.EvaluationRepresentation using (evaluate-restrict-inputs)
open import SCT.VolumeI.Chapter01.Section07.FunctorCategories
open import SCT.VolumeI.Chapter01.Section07.Functoriality
open import SCT.VolumeI.Chapter01.Section07.FunctorCones
open import SCT.VolumeI.Chapter01.Section07.PostEvaluationSubstitution

private
  module _ {Γ : Context} {F K D : CAT Γ} (e : MAP (F × K) D) where
    evaluate-composite : {T : CAT Γ} {f g h : MAP T F} (β : g =₁ h) (α : f =₁ g)
      → evaluate-cong e (β ∙ α) =₂ (evaluate-cong e β ∙ evaluate-cong e α)
    evaluate-composite β α = comp₌-cong (evaluate⁼-absolute e β) (evaluate⁼-absolute e α) ∙
      (evaluate⁼-composition e β α ∙ (evaluate⁼-absolute e (β ∙ α)) ⁻¹)

    module _ {X T : CAT Γ} where
      open Terms.Equalities X using (_＝_)
      evaluate-inverse-family : {f g : MAP T F} (α : f ＝ g)
        → evaluate⁼ e (α ⁻¹) =₁ (evaluate⁼ e α) ⁻¹
      evaluate-inverse-family {f} α = (inverse-unique (evaluate⁼ e α) (evaluate⁼ e (α ⁻¹))
        (evaluate⁼-identity e f ∙
          (evaluate⁼-cong e (comp₌-inverseˡ α) ∙ (evaluate⁼-composition e (α ⁻¹) α) ⁻¹))) ⁻¹

    evaluate-inverse : {T : CAT Γ} {f g : MAP T F} (α : f =₁ g)
      → evaluate-cong e (α ⁻¹) =₂ (evaluate-cong e α) ⁻¹
    evaluate-inverse α = (inv₌ ◁ evaluate⁼-absolute e α) ∙
      (evaluate-inverse-family α ∙ (evaluate⁼-absolute e (α ⁻¹)) ⁻¹)

    evaluate-endpoints : {T : CAT Γ} {x x′ y y′ : MAP T F}
      (p : x =₁ x′) (q : y =₁ y′) (α : x =₁ y)
      → evaluate-cong e (changeEndpoints p q α) =₂
          changeEndpoints (evaluate-cong e p) (evaluate-cong e q) (evaluate-cong e α)
    evaluate-endpoints p q α = comp₌-cong (id₌ (evaluate-cong e q))
      (comp₌-cong (id₌ (evaluate-cong e α)) (evaluate-inverse p) ∙ evaluate-composite α (p ⁻¹)) ∙
      evaluate-composite q (α ∙ p ⁻¹)

    evaluate-identification-restrict : {R T : CAT Γ} {f g : MAP T F} (α : f =₁ g) (r : MAP R T)
      → SquareCell₌ (evaluate-cong e (α ▷ r)) (evaluate-cong e α ▷ productMap r (id K))
          (evaluate-restrict e f r) (evaluate-restrict e g r)
    evaluate-identification-restrict α r = unconst-sides₌
      (replace-edges₌ (evaluate⁼-absolute e (α ▷ r))
        (preWhisker (productMap r (id K)) ◁ evaluate⁼-absolute e α) (evaluate-restrict-inputs e α r))

  module _ {Γ : Context} {R T D : CAT Γ} where
    pre-endpoints : {x x′ y y′ : MAP T D}
      (p : x =₁ x′) (q : y =₁ y′) (α : x =₁ y) (r : MAP R T)
      → (changeEndpoints p q α ▷ r) =₂ changeEndpoints (p ▷ r) (q ▷ r) (α ▷ r)
    pre-endpoints p q α r = comp₌-cong (id₌ (q ▷ r))
      (comp₌-cong (id₌ (α ▷ r)) (preWhisker-inverse p r) ∙ preWhisker-comp₌ α (p ⁻¹) r) ∙
      preWhisker-comp₌ q (α ∙ p ⁻¹) r

module FunctorConeRestriction {Γ : Context} (K : CAT Γ) {C D E T R : CAT Γ}
  (f : MAP C E) (g : MAP D E) (r : MAP R T)
  (s : Cone (funPost {C = K} f) (funPost {C = K} g) T) where
  open FunctorCones K f g
  private
    p = Cone.left s
    q = Cone.right s
    τ = Cone.match s
    F = funPost {C = K} f
    G = funPost {C = K} g
    eC = funEval {C = K} {D = C}
    eD = funEval {C = K} {D = D}
    eE = funEval {C = K} {D = E}
    change = productMap r (id K)
    af = comp-assoc r p F
    ag = comp-assoc r q G
    Ef = funPost-uncurry {C = K} {D = C} {E = E} f (p ∘ r) ∙ evaluate-cong eE af
    Eg = funPost-uncurry {C = K} {D = D} {E = E} g (q ∘ r) ∙ evaluate-cong eE ag
    Ef′ = comp-assoc change (evaluate eC p) f ∙ (funPost-uncurry {C = K} {D = C} {E = E} f p ▷ change)
    Eg′ = comp-assoc change (evaluate eD q) g ∙ (funPost-uncurry {C = K} {D = D} {E = E} g q ▷ change)
    bf = evaluate-restrict eE (F ∘ p) r
    bg = evaluate-restrict eE (G ∘ q) r

  source = uncurryCone (cone-restrict r s)
  target = cone-restrict change (uncurryCone s)
  left = evaluate-restrict eC p r
  right = evaluate-restrict eD q r

  private
    rawSource = changeEndpoints Ef Eg (evaluate-cong eE (τ ▷ r))
    rawTarget = changeEndpoints Ef′ Eg′ (evaluate-cong eE τ ▷ change)
    source-normal : Cone.match source =₂ rawSource
    source-normal = changeEndpoints-iterated (evaluate-cong eE af) (evaluate-cong eE ag)
      (funPost-uncurry {C = K} {D = C} {E = E} f (p ∘ r)) (funPost-uncurry {C = K} {D = D} {E = E} g (q ∘ r)) (evaluate-cong eE (τ ▷ r)) ∙
      changeEndpoints-cong (funPost-uncurry {C = K} {D = C} {E = E} f (p ∘ r)) (funPost-uncurry {C = K} {D = D} {E = E} g (q ∘ r))
        (evaluate-endpoints eE af ag (τ ▷ r))
    target-normal : Cone.match target =₂ rawTarget
    target-normal = changeEndpoints-iterated (funPost-uncurry {C = K} {D = C} {E = E} f p ▷ change) (funPost-uncurry {C = K} {D = D} {E = E} g q ▷ change)
      (comp-assoc change (evaluate eC p) f) (comp-assoc change (evaluate eD q) g)
      (evaluate-cong eE τ ▷ change) ∙
      changeEndpoints-cong (comp-assoc change (evaluate eC p) f) (comp-assoc change (evaluate eD q) g)
        (pre-endpoints (funPost-uncurry {C = K} {D = C} {E = E} f p) (funPost-uncurry {C = K} {D = D} {E = E} g q) (evaluate-cong eE τ) change)
    raw-square : SquareCell₌ (f ◁ left) (g ◁ right) rawSource rawTarget
    raw-square = transport-square Ef Ef′ Eg Eg′ (evaluate-cong eE (τ ▷ r)) (evaluate-cong eE τ ▷ change)
      bf bg (f ◁ left) (g ◁ right)
      ((funPost-uncurry-restrict {K = K} {C = C} {D = E} {T = T} {R = R} f p r) ⁻¹ ∙
        comp₌-assoc (comp-assoc change (evaluate eC p) f)
          (funPost-uncurry {C = K} {D = C} {E = E} f p ▷ change) bf)
      ((funPost-uncurry-restrict {K = K} {C = D} {D = E} {T = T} {R = R} g q r) ⁻¹ ∙
        comp₌-assoc (comp-assoc change (evaluate eD q) g)
          (funPost-uncurry {C = K} {D = D} {E = E} g q ▷ change) bg)
      (transpose-square₌ (evaluate-identification-restrict eE τ r))

  comparison : ConeIdentification₁ source target
  comparison = record
    { left = left; right = right
    ; compatible = replace-sides₌ (source-normal ⁻¹) (target-normal ⁻¹) raw-square }

module _ {Γ : Context} (K : CAT Γ) {C D E T R : CAT Γ} (f : MAP C E) (g : MAP D E) where
  uncurryCone-restrict : (r : MAP R T) (s : Cone (funPost {C = K} f) (funPost {C = K} g) T)
    → ConeIdentification₁ (FunctorCones.uncurryCone K f g (cone-restrict r s))
        (cone-restrict (productMap r (id K)) (FunctorCones.uncurryCone K f g s))
  uncurryCone-restrict = FunctorConeRestriction.comparison K f g
```