cong-composeNaturalIsomorphism : NaturalIsomorphism (H ⊚ F) (I ⊚ G)
  cong-composeNaturalIsomorphism = record
    { left = record
      { transform = transform (left β) ∘ (H ∙ transform (left α))
      ; naturality = λ {a b f} →
          begin
            (transform (left β) ∘ (H ∙ transform (left α))) ∘ (H ∙ (F ∙ f))
          ≈⟨ sym assoc ⟩
            transform (left β) ∘ ((H ∙ transform (left α)) ∘ (H ∙ (F ∙ f)))
          ≈⟨ cong comp refl (map-∘ H) ⟩
            transform (left β) ∘ (H ∙ (transform (left α) ∘ (F ∙ f)))
          ≈⟨ cong comp refl (H ∙ naturality (left α)) ⟩
            transform (left β) ∘ (H ∙ ((G ∙ f) ∘ transform (left α)))
          ≈⟨ naturality (left β) ⟩
            (I ∙ ((G ∙ f) ∘ transform (left α))) ∘ transform (left β)
          ≈⟨ cong comp (sym (map-∘ I)) refl ⟩
            ((I ∙ (G ∙ f)) ∘ (I ∙ transform (left α))) ∘ transform (left β)
          ≈⟨ sym assoc ⟩
            (I ∙ (G ∙ f)) ∘ ((I ∙ transform (left α)) ∘ transform (left β))
          ≈⟨ cong comp refl (sym (naturality (left β))) ⟩
            (I ∙ (G ∙ f)) ∘ (transform (left β) ∘ (H ∙ transform (left α)))
          ∎
      }
    ; right = record
      { transform = transform (right β) ∘ (I ∙ transform (right α))
      ; naturality = λ {a b f} →
          begin
            (transform (right β) ∘ (I ∙ transform (right α))) ∘ (I ∙ (G ∙ f))
          ≈⟨ sym assoc ⟩
            transform (right β) ∘ ((I ∙ transform (right α)) ∘ (I ∙ (G ∙ f)))
          ≈⟨ cong comp refl (map-∘ I) ⟩
            transform (right β) ∘ (I ∙ (transform (right α) ∘ (G ∙ f)))
          ≈⟨ cong comp refl (I ∙ naturality (right α)) ⟩
            transform (right β) ∘ (I ∙ ((F ∙ f) ∘ transform (right α)))
          ≈⟨ cong comp refl (sym (map-∘ I)) ⟩
            transform (right β) ∘ ((I ∙ (F ∙ f)) ∘ (I ∙ transform (right α)))
          ≈⟨ assoc ⟩
            (transform (right β) ∘ (I ∙ (F ∙ f))) ∘ (I ∙ transform (right α))
          ≈⟨ cong comp (naturality (right β)) refl ⟩
            ((H ∙ (F ∙ f)) ∘ transform (right β)) ∘ (I ∙ transform (right α))
          ≈⟨ sym assoc ⟩
            (H ∙ (F ∙ f)) ∘ (transform (right β) ∘ (I ∙ transform (right α)))
          ∎
      }
    ; isIsomorphism = record
      { cancelLR =
          begin
            (transform (left β) ∘ (H ∙ transform (left α))) ∘
              (transform (right β) ∘ (I ∙ transform (right α)))
          ≈⟨ cong comp (naturality (left β)) refl ⟩
            ((I ∙ transform (left α)) ∘ transform (left β)) ∘
              (transform (right β) ∘ (I ∙ transform (right α)))
          ≈⟨ sym assoc ⟩
            (I ∙ transform (left α)) ∘
              (transform (left β) ∘ (transform (right β) ∘ (I ∙ transform (right α))))
          ≈⟨ cong comp refl assoc ⟩
            (I ∙ transform (left α)) ∘
              ((transform (left β) ∘ transform (right β)) ∘ (I ∙ transform (right α)))
          ≈⟨ cong comp refl (cong comp (cancelLR β) refl) ⟩
            (I ∙ transform (left α)) ∘ (id ∘ (I ∙ transform (right α)))
          ≈⟨ cong comp refl idUnitˡ ⟩
            (I ∙ transform (left α)) ∘ (I ∙ transform (right α))
          ≈⟨ map-∘ I ⟩
            I ∙ (transform (left α) ∘ transform (right α))
          ≈⟨ I ∙ cancelLR α ⟩
            I ∙ id
          ≈⟨ map-id I ⟩
            id
          ∎
      ; cancelRL =
          begin
            (transform (right β) ∘ (I ∙ transform (right α))) ∘
              (transform (left β) ∘ (H ∙ transform (left α)))
          ≈⟨ sym assoc ⟩
            transform (right β) ∘
              (((I ∙ transform (right α))) ∘ (transform (left β) ∘ (H ∙ transform (left α))))
          ≈⟨ cong comp refl assoc ⟩
            transform (right β) ∘
              ((((I ∙ transform (right α))) ∘ transform (left β)) ∘ (H ∙ transform (left α)))
          ≈⟨ cong comp refl (cong comp (sym (naturality (left β))) refl) ⟩
            transform (right β) ∘
              (((transform (left β) ∘ (H ∙ transform (right α)))) ∘ (H ∙ transform (left α)))
          ≈⟨ assoc ⟩
            (transform (right β) ∘ ((transform (left β) ∘ (H ∙ transform (right α))))) ∘
              (H ∙ transform (left α))
          ≈⟨ cong comp assoc refl ⟩
            ((transform (right β) ∘ transform (left β)) ∘ (H ∙ transform (right α))) ∘
              (H ∙ transform (left α))
          ≈⟨ cong comp (cong comp (cancelRL β) refl) refl ⟩
            (id ∘ (H ∙ transform (right α))) ∘ (H ∙ transform (left α))
          ≈⟨ cong comp idUnitˡ refl ⟩
            (H ∙ transform (right α)) ∘ (H ∙ transform (left α))
          ≈⟨ map-∘ H ⟩
            H ∙ (transform (right α) ∘ transform (left α))
          ≈⟨ H ∙ cancelRL α ⟩
            H ∙ id
          ≈⟨ map-id H ⟩
            id
          ∎
      }
    }