WIP: Work out the first proof

Author: Victor Miraldo

src/Cheshire/Morphism/Reasoning/Iso.agda

@@ -0,0 +1,38 @@
+-- Copied with minor changes from agda-categories:
+-- https://agda.github.io/agda-categories/Categories.Morphism.Reasoning.Iso.html
+-- which is licensed under the MIT license.
+--   Copyright (c) 2019 Agda Github Community
+
+{-# OPTIONS --safe #-}
+
+open import Cheshire.Core
+open import Cheshire.Signatures
+open import Cheshire.Structures.Core
+import Cheshire.Morphism.Bundles as Bundles
+import Cheshire.Morphism.Reasoning.Core as MorReasoning
+
+module Cheshire.Morphism.Reasoning.Iso
+  {o l} {Q : Quiver o l}
+  {C : Category Q }
+  {e} ⦃ eq : Equivalence Q e ⦄
+  (is-C : IsCategory C)
+  where
+
+open Quiver Q using (_⇒_)
+open Category C
+open IsCategory is-C
+open Definitions C
+open Bundles C
+open HomReasoning
+
+module Switch {A B : Q .Ob}(a-is-b : A ≅ B) where
+  open _≅_ a-is-b
+  open MorReasoning is-C
+
+  switch-fromtoˡ
+    : {X : Q .Ob}{h : X ⇒ A}{k : X ⇒ B}
+    → from ∘ h ≈ k → h ≈ to ∘ k
+  switch-fromtoˡ {h = h} {k = k} hyp = begin
+    h ≈⟨ sym (cancelˡ  isoˡ {f = h}) ⟩
+    to ∘ (from ∘ h) ≈⟨ ∘-resp-≈ refl hyp ⟩
+    to ∘ k ∎