SCT.VolumeI.Chapter01.Section06.MappingCalculus.MappingProofs

Complete compiler-highlighted source. Follow a symbol to its declaration.

# Opaque uncurrying coherence proofs

The cone calculations use these checked statements without unfolding the
underlying evaluation and product proofs. All comparison maps retain their
definitions.

```agda
{-# OPTIONS --safe --without-K #-}
open import Agda.Primitive using (Level)
open import SCT.VolumeI.Chapter01.Theory using (Theory)
import SCT.VolumeI.Chapter01.Section04.MappingAnimae as Mapping
import SCT.VolumeI.Chapter01.Section05.Setup as Setup
import SCT.VolumeI.Chapter01.Section04.Substitution.Compatibility as Compatibility
import SCT.VolumeI.Chapter01.Section04.Substitution.ParameterChange as ParameterChange

module SCT.VolumeI.Chapter01.Section06.MappingCalculus.MappingProofs
  {c m a : Level} (𝒯 : Theory c m a) (M : Mapping.MappingAnimae 𝒯) where

module Original = Setup 𝒯 M
open Original hiding (mapUncurryIso-comp)
module Change = ParameterChange 𝒯 M
module Compatible = Compatibility 𝒯 M

abstract
  mapUncurryIso-comp : {X C D : CAT} {f g h : MAP X (Map C D)}
    (β : g =₁ h) (α : f =₁ g) →
    (mapUncurryIso (β ∙ α)) =₂ (mapUncurryIso β ∙ mapUncurryIso α)
  mapUncurryIso-comp = Original.mapUncurryIso-comp

  mapUncurryIso-inverse : {X C D : CAT} {f g : MAP X (Map C D)} (α : f =₁ g) →
    (mapUncurryIso (α ⁻¹)) =₂ ((mapUncurryIso α) ⁻¹)
  mapUncurryIso-inverse = Change.mapUncurryIso-inverse

  mapUncurry-restrict-inputs : {Y X C D : CAT} {f g : MAP X (Map C D)}
    (α : f =₁ g) (σ : MAP Y X) →
    (mapUncurry-restrict g σ ∙ mapUncurryIso (α ▷ σ)) =₂
      ((mapUncurryIso α ▷ productMap σ (id C)) ∙ mapUncurry-restrict f σ)
  mapUncurry-restrict-inputs = Compatible.mapUncurry-restrict-inputs
```