SCT.VolumeI.Chapter01.Section08.FunctorPushoutCriterion

Chapter 1, rebuild2, checked 14 October 2026 · source revision b982f5a.

# The actual Fun mapping-out criterion

The cone is chosen by currying evaluation of the actual product square.
Its legs are the selected Fun precomposition maps. Its matching is this
derived currying witness; no equality with the former compositor pasting
is asserted. The arbitrary categorical parameter comparison retains the
complete supplied cell. The converse below uses this same chosen cone.
Both implications use this same chosen cone and retain complete matching
comparisons at arbitrary categorical parameters.

```agda
{-# OPTIONS --without-K --lossy-unification #-}
module SCT.VolumeI.Chapter01.Section08.FunctorPushoutCriterion where

open import SCT.VolumeI.Chapter01.Section01.Vocabulary hiding (_＝_)
import SCT.VolumeI.Chapter01.Section01.Terms as Terms
open Operations
open import SCT.VolumeI.Chapter01.Section02.Coherence using (id₌; comp-assoc; comp-unitʳ; module Composition; module Boundaries)
open Composition
open Boundaries using (SquareCell₌)
open import SCT.VolumeI.Chapter01.Section01.Terminal using (module Constructions)
open Constructions
open import SCT.VolumeI.Chapter01.Section02.Specialization
open import SCT.VolumeI.Chapter01.Section02.IdentificationSquares
open import SCT.VolumeI.Chapter01.Section02.Products using (module Calculus)
open Calculus
open import SCT.VolumeI.Chapter01.Section03.Identifications.Inverses using (cancel-right; comp₌-inverseˡ-One; inverse-composite; inverse-inverse; postWhisker-inverse; preWhisker-inverse)
open import SCT.VolumeI.Chapter01.Section03.Identifications.EndpointTransport using (changeEndpoints-extend-square)
open import SCT.VolumeI.Chapter01.Section03.Identifications.Triangles using (post-square-cell-outer)
open import SCT.VolumeI.Chapter01.Section03.Products.ProductFunctor using (productMap-cong)
open import SCT.VolumeI.Chapter01.Section03.Products.ProductRestriction
open import SCT.VolumeI.Chapter01.Section03.Squares using (Square)
open import SCT.VolumeI.Chapter01.Section06.Cones
open import SCT.VolumeI.Chapter01.Section06.ConeIdentifications using (cone-compose; cone-inverse)
open import SCT.VolumeI.Chapter01.Section06.PullbackSquares using (IsPullback; module UniversalCone; isPullback-from-factor-and-reflection)
open import SCT.VolumeI.Chapter01.Section06.Pullbacks using (Pullback; pullback-cone; pullback-isAn)
open import SCT.VolumeI.Chapter01.Section04.MappingAnimae using (Map; map-isAn; uncurry; mapCurry; mapCurry-β)
open import SCT.VolumeI.Chapter01.Section04.Currying using (uncurry-reflect; uncurry⁼)
open import SCT.VolumeI.Chapter01.Section07.FunctorCategories using (Fun; funEval; funUniversal)
open import SCT.VolumeI.Chapter01.Section07.Functoriality using (funPre; funPre⁼; funPre-comp; funPre-uncurry)

open import SCT.VolumeI.Chapter01.Section07.Currying using (funCurry; funCurry-β; funUncurry; reflect)
open import SCT.VolumeI.Chapter01.Section07.Evaluation
open import SCT.VolumeI.Chapter01.Section08.Cocones
open import SCT.VolumeI.Chapter01.Section08.PushoutSquares using (mappingOut; IsPushout)
open import SCT.VolumeI.Chapter01.Section08.MappingOutEvaluation using (module MappingOutEvaluation; module ParameterizedSquareEvaluation)
open import SCT.VolumeI.Chapter01.Section08.FunctorMappingOutEvaluation using (module NativeRestrictionCocones; module DirectCurriedFunctorSquare; module TransposedRestrictionCocones; module NativeOrdinaryCocones; module OrdinaryMappingCocones; module OrdinaryParameterizedSquareEvaluation; module OrdinaryPostcompositionEncoding; module TransposedOrdinarySquareEvaluation; module NativeOrdinaryReflectedCocone)
open import SCT.VolumeI.Chapter01.Section04.Functoriality using (mapPre)
open import SCT.VolumeI.Chapter01.Section04.Points using (name; decode; decode-name)
open import SCT.VolumeI.Chapter01.Section03.ProductConstructions using (swap; swap-swap; product-unitˡ-inverse)

module _ {Γ : Context} where
  functorOut : {A B C D : CAT Γ} {l : MAP A C} {r : MAP B D}
    (s : Square l r) (E : CAT Γ)
    → Cone (funPre {D = E} (Square.source-map s)) (funPre l) (Fun D E)
  functorOut s E = DirectCurriedFunctorSquare.value s E

  FunctorCriterion : {A B C D : CAT Γ} {l : MAP A C} {r : MAP B D}
    → Square l r → Set (c ⊔ m)
  FunctorCriterion s = (E : CAT Γ) → IsPullback (functorOut s E)


module _ {Γ : Context} where
  module NativeParameterizedSquareEvaluation {P A B C D E : CAT Γ} {l : MAP A C} {r : MAP B D}
    (s : Square l r) (h : MAP P (Fun D E)) where
    module Calculation = DirectCurriedFunctorSquare.Parameterized s E h
    open Calculation public using (source; target)
    identification : CoconeIdentification₁ source target
    identification = Calculation.comparison

private
  module _ {Γ : Context} {X A B C T E : CAT Γ}
    {u : MAP A B} {l : MAP A C} (s : Cocone u l T) where
    open Terms.Equalities X using (_＝_)

    postcomposition-identification : {h k : MAP T E} → h ＝ k
      → CoconeIdentification X (cocone-postcompose h s) (cocone-postcompose k s)
    postcomposition-identification α = record
      { left = α ▷ Cocone.left s
      ; right = α ▷ Cocone.right s
      ; compatible = post-square-cell-outer l (Cocone.right s) (Cocone.left s)
          u (Cocone.match s) α }

private
  module _ {Γ : Context} where
    cocone-compose₁ : {A B C E : CAT Γ} {u : MAP A B} {l : MAP A C}
      {s t v : Cocone u l E} → CoconeIdentification₁ t v → CoconeIdentification₁ s t
      → CoconeIdentification₁ s v
    cocone-compose₁ Ψ Φ = cocone-identification-One
      (cocone-identification-compose (cocone-identification Ψ) (cocone-identification Φ))
    cocone-inverse₁ : {A B C E : CAT Γ} {u : MAP A B} {l : MAP A C}
      {s t : Cocone u l E} → CoconeIdentification₁ s t → CoconeIdentification₁ t s
    cocone-inverse₁ Φ = cocone-identification-One
      (cocone-identification-inverse (cocone-identification Φ))

-- Ordinary cocone universality extracted from the actual Map pushout condition.
-- Intended private supporting argument inside FunctorPushoutCriterion.
private
  module OrdinaryPushout {Γ : Context} {A B C D : CAT Γ}
    {l : MAP A C} {r : MAP B D} (s : Square l r) (hyp : IsPushout s) (T : CAT Γ) where
    private
      u : MAP A B
      u = Square.source-map s
      ordinary : Cocone u l D
      ordinary = square-cocone s
      module O = OrdinaryMappingCocones {E = T} u l
      module Universal = UniversalCone (mappingOut s T) (hyp T)

    module Extension (t : Cocone u l T) where
      point : MAP One (Map D T)
      point = Universal.factor (O.encoded t)
      factor : MAP D T
      factor = decode point
      private
        decoded-beta : CoconeIdentification₁
          (O.decoded (cone-restrict point (mappingOut s T))) (O.decoded (O.encoded t))
        decoded-beta = cocone-identification-One
          (O.decoded-identification (cone-identification (Universal.β (O.encoded t))))
        actual-square : CoconeIdentification₁
          (O.decoded (cone-restrict point (mappingOut s T))) (cocone-postcompose factor ordinary)
        actual-square = OrdinaryParameterizedSquareEvaluation.identification s point
      beta : CoconeIdentification₁ (cocone-postcompose factor ordinary) t
      beta = cocone-compose₁ (O.decoded-encoded t)
        (cocone-compose₁ decoded-beta (cocone-inverse₁ actual-square))

    reflection : (h k : MAP D T)
      → CoconeIdentification₁ (cocone-postcompose h ordinary) (cocone-postcompose k ordinary)
      → h =₁ k
    reflection h k Φ = decode-name k ∙ ((uncurry⁼ named-identification ▷ product-unitˡ-inverse D) ∙
      (decode-name h) ⁻¹)
      where
      named-comparison : ConeIdentification₁
        (cone-restrict (name h) (mappingOut s T)) (cone-restrict (name k) (mappingOut s T))
      named-comparison = cone-compose
        (cone-inverse (OrdinaryPostcompositionEncoding.identification s k))
        (cone-compose (cone-identification-One (O.encoded-identification (cocone-identification Φ)))
          (OrdinaryPostcompositionEncoding.identification s h))
      named-identification : name h =₁ name k
      named-identification = Universal.reflect (name h) (name k) named-comparison
-- Reflection uses only a parameter One for the mapping cone; T is arbitrary categorical.
-- Additional direct imports: Points.name/decode/decode-name, Currying.uncurry⁼,
-- ProductConstructions.product-unitˡ-inverse, both concrete ordinary square adapters.

module FunctorCriterionConverse {Γ : Context} {A B C D : CAT Γ}
  {l : MAP A C} {r : MAP B D} (s : Square l r) (hyp : FunctorCriterion s) (E : CAT Γ) where
  private
    u : MAP A B
    u = Square.source-map s
    v : MAP C D
    v = Square.target-map s
    F : MAP (Map B E) (Map A E)
    F = mapPre {D = E} u
    G : MAP (Map C E) (Map A E)
    G = mapPre {D = E} l
    module Universal = UniversalCone (functorOut s E) (hyp E)

  module At {K : CAT Γ} (kAn : isAn K) where
    private
      module M = MappingOutEvaluation {P = K} {E = E} u l
      module N = NativeRestrictionCocones {P = K} {E = E} u l
      product-cocone : Cocone (product-restriction {P = K} u) (product-restriction l) (K × D)
      product-cocone = square-cocone (product-square {P = K} s)

    module Lift (t : Cone F G K) where
      private
        module Encoded = N.CurriedCocone (M.represented t)
        native-factor : MAP K (Fun D E)
        native-factor = Universal.factor Encoded.value
      factor : MAP K (Map D E)
      factor = mapCurry kAn (funUncurry native-factor)
      private
        native-beta : CoconeIdentification₁
          (N.represented (cone-restrict native-factor (functorOut s E)))
          (N.represented Encoded.value)
        native-beta = cocone-identification-One
          (N.evaluate-identification (cone-identification (Universal.β Encoded.value)))
        native-product : CoconeIdentification₁
          (cocone-postcompose (funUncurry native-factor) product-cocone) (M.represented t)
        native-product = cocone-compose₁
          {s = cocone-postcompose (funUncurry native-factor) product-cocone}
          {t = N.represented Encoded.value} {v = M.represented t}
          Encoded.comparison
          (cocone-compose₁
            {s = cocone-postcompose (funUncurry native-factor) product-cocone}
            {t = N.represented (cone-restrict native-factor (functorOut s E))}
            {v = N.represented Encoded.value}
            native-beta
            (cocone-inverse₁
              {s = N.represented (cone-restrict native-factor (functorOut s E))}
              {t = cocone-postcompose (funUncurry native-factor) product-cocone}
              (NativeParameterizedSquareEvaluation.identification s native-factor)))
        factor-image : CoconeIdentification₁
          (cocone-postcompose (uncurry factor) product-cocone)
          (cocone-postcompose (funUncurry native-factor) product-cocone)
        factor-image = cocone-identification-One
          (postcomposition-identification product-cocone
            (mapCurry-β kAn (funUncurry native-factor)))
        product-beta : CoconeIdentification₁
          (M.represented (cone-restrict factor (mappingOut s E))) (M.represented t)
        product-beta = cocone-compose₁ native-product
          (cocone-compose₁ factor-image (ParameterizedSquareEvaluation.identification s factor))
      beta : ConeIdentification₁ (cone-restrict factor (mappingOut s E)) t
      beta = cone-identification-One
        (M.RecoveredIdentification.identification kAn
          (cone-restrict factor (mappingOut s E)) t (cocone-identification product-beta))

  private
    S : CAT Γ
    S = Map D E
    module M = MappingOutEvaluation {P = S} {E = E} u l
    module N = NativeRestrictionCocones {P = S} {E = E} u l
    product-cocone : Cocone (product-restriction {P = S} u) (product-restriction l) (S × D)
    product-cocone = square-cocone (product-square {P = S} s)

  module Reflection (h k : MAP S S)
    (Φ : ConeIdentification₁ (cone-restrict h (mappingOut s E)) (cone-restrict k (mappingOut s E))) where
    native-h : MAP S (Fun D E)
    native-h = funCurry (uncurry h)
    native-k : MAP S (Fun D E)
    native-k = funCurry (uncurry k)
    beta-h : funUncurry native-h =₁ uncurry h
    beta-h = funCurry-β (uncurry h)
    beta-k : funUncurry native-k =₁ uncurry k
    beta-k = funCurry-β (uncurry k)
    h-image : CoconeIdentification₁
      (cocone-postcompose (funUncurry native-h) product-cocone)
      (cocone-postcompose (uncurry h) product-cocone)
    h-image = cocone-identification-One
      (postcomposition-identification product-cocone beta-h)
    k-image : CoconeIdentification₁
      (cocone-postcompose (funUncurry native-k) product-cocone)
      (cocone-postcompose (uncurry k) product-cocone)
    k-image = cocone-identification-One
      (postcomposition-identification product-cocone beta-k)
    map-comparison : CoconeIdentification₁
      (M.represented (cone-restrict h (mappingOut s E)))
      (M.represented (cone-restrict k (mappingOut s E)))
    map-comparison = cocone-identification-One (M.evaluate-identification (cone-identification Φ))
    native-product-comparison : CoconeIdentification₁
      (N.represented (cone-restrict native-h (functorOut s E)))
      (N.represented (cone-restrict native-k (functorOut s E)))
    native-product-comparison = cocone-compose₁
      (cocone-inverse₁ (NativeParameterizedSquareEvaluation.identification s native-k))
      (cocone-compose₁ (cocone-inverse₁ k-image)
        (cocone-compose₁ (ParameterizedSquareEvaluation.identification s k)
          (cocone-compose₁ map-comparison
            (cocone-compose₁ (cocone-inverse₁ (ParameterizedSquareEvaluation.identification s h))
              (cocone-compose₁ h-image (NativeParameterizedSquareEvaluation.identification s native-h))))))
    native-comparison : ConeIdentification₁
      (cone-restrict native-h (functorOut s E)) (cone-restrict native-k (functorOut s E))
    native-comparison = cone-identification-One
      (N.ReflectedCocone.value (cone-restrict native-h (functorOut s E))
        (cone-restrict native-k (functorOut s E))
        (cocone-identification
          {s = N.represented (cone-restrict native-h (functorOut s E))}
          {t = N.represented (cone-restrict native-k (functorOut s E))}
          native-product-comparison))
    native-identification : native-h =₁ native-k
    native-identification = Universal.reflect native-h native-k native-comparison
    map-image : uncurry h =₁ uncurry k
    map-image = beta-k ∙
      (evaluate-cong (funEval {C = D} {D = E}) native-identification ∙ beta-h ⁻¹)

  reflection : (h k : MAP S S)
    → ConeIdentification₁ (cone-restrict h (mappingOut s E)) (cone-restrict k (mappingOut s E))
    → h =₁ k
  reflection h k Φ = uncurry-reflect (map-isAn D E) h k (Reflection.map-image h k Φ)

  private
    pullback-anima : isAn (Pullback F G)
    pullback-anima = pullback-isAn F G (map-isAn B E) (map-isAn C E) (map-isAn A E)

    chosen-factor : MAP (Pullback F G) (Map D E)
    chosen-factor = At.Lift.factor pullback-anima (pullback-cone F G)

    chosen-beta : ConeIdentification₁ (cone-restrict chosen-factor (mappingOut s E)) (pullback-cone F G)
    chosen-beta = At.Lift.beta pullback-anima (pullback-cone F G)

    chosen-reflection : (h k : MAP (Map D E) (Map D E))
      → ConeIdentification₁ (cone-restrict h (mappingOut s E)) (cone-restrict k (mappingOut s E))
      → h =₁ k
    chosen-reflection = reflection

  comparison-isPullback : IsPullback (mappingOut s E)
  comparison-isPullback = isPullback-from-factor-and-reflection (mappingOut s E)
    chosen-factor chosen-beta chosen-reflection

module _ {Γ : Context} where
  functor-criterion→pushout : {A B C D : CAT Γ} {l : MAP A C} {r : MAP B D}
    (s : Square l r) → FunctorCriterion s → IsPushout s
  functor-criterion→pushout s hyp E = FunctorCriterionConverse.comparison-isPullback s hyp E

-- Full forward criterion, intended after OrdinaryPushout and concrete adapters.
module FunctorCriterionForward {Γ : Context} {A B C D : CAT Γ}
  {l : MAP A C} {r : MAP B D} (s : Square l r) (hyp : IsPushout s) (E : CAT Γ) where
  private
    u = Square.source-map s
    F = funPre {D = E} u
    G = funPre {D = E} l
  module At (P : CAT Γ) where
    private
      module N = NativeRestrictionCocones {P = P} {E = E} u l
        using (represented; evaluate-identification; module ReflectedCocone)
      module T = TransposedRestrictionCocones {P = P} {E = E} u l
        using (transposed; untranspose-identification; transpose-identification; transpose-roundtrip; module CurriedCocone)
      module O = NativeOrdinaryCocones {P = P} {E = E} u l
        using (represented; evaluate-identification)
      module Universal = OrdinaryPushout s hyp (Fun P E) using (module Extension; reflection)
      product = square-cocone (product-square {P = P} s)
      ordinary = square-cocone s
      pD : MAP (D × P) (P × D)
      pD = swap
      qD : MAP (P × D) (D × P)
      qD = swap
    module Lift (t : Cone F G P) where
      private
        module Encoded = T.CurriedCocone (N.represented t) using (value; comparison)
        module Chosen = Universal.Extension Encoded.value using (factor; beta)
        g : MAP D (Fun P E)
        g = Chosen.factor
        k : MAP (P × D) E
        k = funUncurry g ∘ qD
      factor : MAP P (Fun D E)
      factor = funCurry k
      private
        factor-image : funUncurry factor =₁ k
        factor-image = funCurry-β k
        transposed-actual : CoconeIdentification₁
          (T.transposed (cocone-postcompose (funUncurry factor) product))
          (O.represented (cocone-postcompose g ordinary))
        transposed-actual = cocone-compose₁
          (TransposedOrdinarySquareEvaluation.comparison s g)
          (cocone-identification-One (T.transpose-identification
            (postcomposition-identification product factor-image)))
        evaluated-beta : CoconeIdentification₁
          (O.represented (cocone-postcompose g ordinary)) (O.represented Encoded.value)
        evaluated-beta = cocone-identification-One
          (O.evaluate-identification (cocone-identification Chosen.beta))
        transposed-beta : CoconeIdentification₁
          (T.transposed (cocone-postcompose (funUncurry factor) product)) (T.transposed (N.represented t))
        transposed-beta = cocone-compose₁
          {s = T.transposed (cocone-postcompose (funUncurry factor) product)}
          {t = O.represented Encoded.value} {v = T.transposed (N.represented t)}
          Encoded.comparison
          (cocone-compose₁
            {s = T.transposed (cocone-postcompose (funUncurry factor) product)}
            {t = O.represented (cocone-postcompose g ordinary)}
            {v = O.represented Encoded.value}
            evaluated-beta transposed-actual)
        product-beta : CoconeIdentification₁ (cocone-postcompose (funUncurry factor) product) (N.represented t)
        product-beta = cocone-compose₁ (T.transpose-roundtrip (N.represented t))
          (cocone-compose₁
            (cocone-identification-One (T.untranspose-identification (cocone-identification transposed-beta)))
            (cocone-inverse₁ (T.transpose-roundtrip (cocone-postcompose (funUncurry factor) product))))
        native-beta : CoconeIdentification₁ (N.represented (cone-restrict factor (functorOut s E))) (N.represented t)
        native-beta = cocone-compose₁ product-beta (NativeParameterizedSquareEvaluation.identification s factor)
      beta : ConeIdentification₁ (cone-restrict factor (functorOut s E)) t
      beta = cone-identification-One (N.ReflectedCocone.value (cone-restrict factor (functorOut s E)) t
        (cocone-identification
          {s = N.represented (cone-restrict factor (functorOut s E))}
          {t = N.represented t} native-beta))

    module Reflection (h k : MAP P (Fun D E))
      (Φ : ConeIdentification₁ (cone-restrict h (functorOut s E)) (cone-restrict k (functorOut s E))) where
      private
        ordinary-h : MAP D (Fun P E)
        ordinary-h = funCurry (funUncurry h ∘ pD)
        ordinary-k : MAP D (Fun P E)
        ordinary-k = funCurry (funUncurry k ∘ pD)
        restore : (a : MAP P (Fun D E))
          → (funUncurry (funCurry (funUncurry a ∘ pD)) ∘ qD) =₁ funUncurry a
        restore a = comp-unitʳ (funUncurry a) ∙
          ((funUncurry a ◁ swap-swap P D) ∙
            (comp-assoc qD pD (funUncurry a) ∙ (funCurry-β (funUncurry a ∘ pD) ▷ qD)))
        ordinary-comparison : (a : MAP P (Fun D E))
          → CoconeIdentification₁ (T.transposed (cocone-postcompose (funUncurry a) product))
              (O.represented (cocone-postcompose (funCurry (funUncurry a ∘ pD)) ordinary))
        ordinary-comparison a = cocone-compose₁
          (TransposedOrdinarySquareEvaluation.comparison s (funCurry (funUncurry a ∘ pD)))
          (cocone-identification-One (T.transpose-identification
            (postcomposition-identification product ((restore a) ⁻¹))))
        native-comparison : CoconeIdentification₁
          (N.represented (cone-restrict h (functorOut s E))) (N.represented (cone-restrict k (functorOut s E)))
        native-comparison = cocone-identification-One (N.evaluate-identification (cone-identification Φ))
        product-comparison : CoconeIdentification₁
          (cocone-postcompose (funUncurry h) product) (cocone-postcompose (funUncurry k) product)
        product-comparison = cocone-compose₁ (NativeParameterizedSquareEvaluation.identification s k)
          (cocone-compose₁ native-comparison (cocone-inverse₁ (NativeParameterizedSquareEvaluation.identification s h)))
        evaluated-comparison : CoconeIdentification₁
          (O.represented (cocone-postcompose ordinary-h ordinary))
          (O.represented (cocone-postcompose ordinary-k ordinary))
        evaluated-comparison = cocone-compose₁ (ordinary-comparison k)
          (cocone-compose₁
            (cocone-identification-One (T.transpose-identification (cocone-identification product-comparison)))
            (cocone-inverse₁ (ordinary-comparison h)))
        recovered : CoconeIdentification₁
          (cocone-postcompose ordinary-h ordinary) (cocone-postcompose ordinary-k ordinary)
        recovered = cocone-identification-One
          (NativeOrdinaryReflectedCocone.value u l (cocone-postcompose ordinary-h ordinary)
            (cocone-postcompose ordinary-k ordinary) (cocone-identification evaluated-comparison))
        ordinary-identification : ordinary-h =₁ ordinary-k
        ordinary-identification = Universal.reflection ordinary-h ordinary-k recovered
        map-image : funUncurry h =₁ funUncurry k
        map-image = restore k ∙
          ((evaluate-cong (funEval {C = P} {D = E}) ordinary-identification ▷ qD) ∙ (restore h) ⁻¹)
      identification : h =₁ k
      identification = reflect (funEval {C = D} {D = E}) (funUniversal D E) h k map-image

    reflection : (h k : MAP P (Fun D E))
      → ConeIdentification₁ (cone-restrict h (functorOut s E)) (cone-restrict k (functorOut s E)) → h =₁ k
    reflection h k Φ = Reflection.identification h k Φ

  comparison-isPullback : IsPullback (functorOut s E)
  comparison-isPullback = isPullback-from-factor-and-reflection (functorOut s E)
    (At.Lift.factor (Pullback F G) (pullback-cone F G))
    (At.Lift.beta (Pullback F G) (pullback-cone F G))
    (At.reflection (Fun D E))

module _ {Γ : Context} where
  pushout→functor-criterion : {A B C D : CAT Γ} {l : MAP A C} {r : MAP B D}
    (s : Square l r) → IsPushout s → FunctorCriterion s
  pushout→functor-criterion s hyp E = FunctorCriterionForward.comparison-isPullback s hyp E
-- No anima hypothesis on P, and both directions use the same functorOut.
-- Direct imports additionally: ProductConstructions.swap/swap-swap,
-- Currying.reflect, native ordinary/transposed evaluation/recovery modules.
```