SCT.VolumeI.Chapter02.Section02.MorphismCalculus.CompositionWithIdentifications

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

# Composition with an endpoint identification

Postcomposition with a primitive identification agrees with changing the
target frame. Normalize the identification as a retargeted identity, use
compatibility of composition with endpoint changes, and apply the right
unit law. The comparison retains both endpoint equations.

```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.Section07.FunctorCategories as Categories
import SCT.VolumeI.Chapter01.Section06.PullbackLaws as Laws
import SCT.VolumeI.Chapter02.Section01.WalkingMorphism as Walking
import SCT.VolumeI.Chapter02.Section01.IntervalEndpoints as Endpoints
import SCT.VolumeI.Chapter02.Section02.SegalAxiom as Segal

module SCT.VolumeI.Chapter02.Section02.MorphismCalculus.CompositionWithIdentifications
  {c m a : Level} (𝒯 : Theory c m a) (M : Mapping.MappingAnimae 𝒯)
  (ℱ : Categories.FunctorCategories 𝒯 M) (P : Laws.PullbackStructure 𝒯)
  (I : Walking.WalkingMorphism 𝒯) (E : Endpoints.IntervalEndpoints 𝒯 M ℱ P I)
  (S : Segal.SegalAxiom 𝒯 M ℱ P I E) where

open import SCT.VolumeI.Chapter02.Section02.MorphismCalculus.CompositionExpressions 𝒯 M ℱ P I E S public
open import SCT.VolumeI.Chapter02.Section02.MorphismCalculus.ExpressionIdentifications 𝒯 M ℱ I
open import SCT.VolumeI.Chapter02.Section02.MorphismCalculus.CompositionIdentifications 𝒯 M ℱ P I E S
  using (compose-expression-cong)
open import SCT.VolumeI.Chapter02.Section02.MorphismCalculus.CompositionSubstitution 𝒯 M ℱ P I E S
  using (retarget-composition)
open import SCT.VolumeI.Chapter02.Section02.MorphismCalculus.ExpressionFrameCalculus 𝒯 M ℱ I
  using (retarget-id)
open import SCT.VolumeI.Chapter02.Section02.MorphismCalculus.IsomorphismExpressionOperations 𝒯 M ℱ P I E
  using (isomorphism-normal)
open import SCT.VolumeI.Chapter02.Section02.ExpressionUnitLaws 𝒯 M ℱ P I E S
  using (right-unit)

abstract
  postcompose-identification : {Γ C : CAT} {x y z : MAP Γ C}
    (f : MorphismExpression x y) (κ : y =₁ z) →
    ExpressionIso (compose-expression f (isomorphism-expression κ))
      (retarget-expression f (idIso x) κ)
  postcompose-identification {x = x} {y} f κ = expressionIso-compose
    (retarget-expressionIso (right-unit f) (idIso x) κ)
    (expressionIso-compose
      (retarget-composition f (identity-expression y) (idIso x) (idIso y) κ)
      (compose-expression-cong (expressionIso-inverse (retarget-id f))
        (expressionIso-inverse (isomorphism-normal κ))))
```