blob: fa31fcb3ac4bbfbe6e052b26f94a5fca4937c602 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
{-# OPTIONS --without-K --safe #-}
open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory)
module Category.Monoidal.Instance.Cospans.Lift {o ℓ e} where
open import Category.Instance.Cospans using (Cospans; Cospan; Same)
open import Categories.Category.Core using (Category)
import Categories.Diagram.Pushout as PushoutDiagram
import Categories.Diagram.Pushout.Properties as PushoutProperties
import Categories.Morphism as Morphism
import Categories.Morphism.Reasoning as ⇒-Reasoning
import Category.Diagram.Pushout as PushoutDiagram′
import Functor.Instance.Cospan.Embed as CospanEmbed
open import Categories.Category using (_[_,_]; _[_≈_]; _[_∘_]; module Definitions)
open import Categories.Functor.Core using (Functor)
open import Categories.Functor.Properties using ([_]-resp-≅)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; _≃_)
open import Functor.Exact using (RightExactFunctor; IsPushout⇒Pushout)
module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} {𝒟 : FinitelyCocompleteCategory o ℓ e} where
module 𝒞 = FinitelyCocompleteCategory 𝒞
module 𝒟 = FinitelyCocompleteCategory 𝒟
open CospanEmbed 𝒟 using (L; B₁; B∘L; R∘B; ≅-L-R)
module Square {F G : Functor 𝒞.U 𝒟.U} (F≃G : F ≃ G) where
module L = Functor L
module F = Functor F
module G = Functor G
open NaturalIsomorphism F≃G
open Morphism using (module ≅) renaming (_≅_ to _[_≅_])
FX≅GX′ : ∀ {Z : 𝒞.Obj} → Cospans 𝒟 [ F.₀ Z ≅ G.₀ Z ]
FX≅GX′ = [ L ]-resp-≅ FX≅GX
module FX≅GX {Z} = _[_≅_] (FX≅GX {Z})
module FX≅GX′ {Z} = _[_≅_] (FX≅GX′ {Z})
module _ {X Y : 𝒞.Obj} (fg : Cospans 𝒞 [ X , Y ]) where
open ⇒-Reasoning (Cospans 𝒟) using (switch-tofromˡ; switch-fromtoʳ)
open ⇒-Reasoning 𝒟.U using (switch-fromtoˡ)
module Cospans = Category (Cospans 𝒟)
open Cospans.HomReasoning using (refl⟩∘⟨_; _○_; _⟩∘⟨refl)
open Cospan fg renaming (f₁ to f; f₂ to g)
open 𝒟 using (_∘_)
squares⇒cospan : Cospans 𝒟 [ B₁ (G.₁ f ∘ FX≅GX.from) (G.₁ g ∘ FX≅GX.from) ≈ B₁ (F.₁ f) (F.₁ g) ]
squares⇒cospan = record
{ ≅N = ≅.sym 𝒟.U FX≅GX
; from∘f₁≈f₁′ = sym (switch-fromtoˡ FX≅GX (⇒.commute f))
; from∘f₂≈f₂′ = sym (switch-fromtoˡ FX≅GX (⇒.commute g))
}
where
open 𝒟.Equiv using (sym)
from : Cospans 𝒟 [ Cospans 𝒟 [ L.₁ (⇒.η Y) ∘ B₁ (F.₁ f) (F.₁ g) ] ≈ Cospans 𝒟 [ B₁ (G.₁ f) (G.₁ g) ∘ L.₁ (⇒.η X) ] ]
from = sym (switch-tofromˡ FX≅GX′ (refl⟩∘⟨ B∘L ○ ≅-L-R FX≅GX ⟩∘⟨refl ○ R∘B ○ squares⇒cospan))
where
open Cospans.Equiv using (sym)
to : Cospans 𝒟 [ Cospans 𝒟 [ L.₁ (⇐.η Y) ∘ B₁ (G.₁ f) (G.₁ g) ] ≈ Cospans 𝒟 [ B₁ (F.₁ f) (F.₁ g) ∘ L.₁ (⇐.η X) ] ]
to = switch-fromtoʳ FX≅GX′ (pullʳ B∘L ○ ≅-L-R FX≅GX ⟩∘⟨refl ○ R∘B ○ squares⇒cospan)
where
open ⇒-Reasoning (Cospans 𝒟) using (pullʳ)
|
