Other Agda modules in this section (6)
Corresponding book passages
# Functor categories of groupoids
The native exponential comparisons identify constant diagrams after exchanging
the two diagram variables. Both evaluations retain their specified beta
triangles. Their argument maps agree by the two product projections.
Specializing the constant variable to the walking morphism proves closure
of groupoids under functor categories, for arbitrary source category.
```agda
{-# OPTIONS --without-K #-}
module SCT.VolumeI.Chapter02.Section04.FunctorGroupoids where
open import SCT.VolumeI.Chapter01.Section01.Vocabulary
open Operations
open import SCT.VolumeI.Chapter01.Section02.Coherence
using (comp-unitˡ; comp-assoc; module Composition)
open Composition
open import SCT.VolumeI.Chapter01.Section02.Products using (module Calculus)
open Calculus
open import SCT.VolumeI.Chapter01.Section03.ProductConstructions
using (productMap; swap; swap-isEquiv; module Associativity)
open import SCT.VolumeI.Chapter01.Section03.Equivalences
using (equiv-compose; equiv-transport; equiv-cancel-left)
open import SCT.VolumeI.Chapter01.Section07.FunctorCategories using (Fun; funEval; funUniversal)
open import SCT.VolumeI.Chapter01.Section07.Evaluation using (evaluate-cong)
open import SCT.VolumeI.Chapter01.Section07.Currying using (funUncurry; reflect)
open import SCT.VolumeI.Chapter01.Section07.Functoriality
using (funPost; funPost-β; funPost-isEquiv; funPre; funPre-uncurry; funPre-isEquiv)
open import SCT.VolumeI.Chapter01.Section07.ExponentialLaw using (module ExponentialLaw)
open import SCT.VolumeI.Chapter02.Section01.WalkingMorphism using ([1])
open import SCT.VolumeI.Chapter02.Section01.Morphisms
using (constantArrow; constantArrow-image; identityArrow)
open import SCT.VolumeI.Chapter02.Section04.Groupoids using (IsGroupoid)
open import SCT.VolumeI.Chapter02.Section04.BasicClosure using (constant-evaluation)
module _ {Γ : Context} where
constant-exchange-arguments : (N I K : CAT Γ)
→ (productMap (pr₁ {C = N} {D = I}) (id K) ∘
(Associativity.backward N I K ∘ productMap (id N) (swap {C = K} {D = I})))
=₁ (pr₁ ∘ Associativity.backward N K I)
constant-exchange-arguments N I K = pair₌ (right-first ⁻¹ ∙ left-first)
(right-second ⁻¹ ∙ left-second)
where
s : MAP (N × (K × I)) (N × (I × K))
s = productMap (id N) (swap {C = K} {D = I})
b : MAP (N × (I × K)) ((N × I) × K)
b = Associativity.backward N I K
r : MAP (N × (K × I)) ((N × K) × I)
r = Associativity.backward N K I
left-first : (pr₁ ∘ (productMap (pr₁ {C = N} {D = I}) (id K) ∘ (b ∘ s))) =₁ pr₁
left-first = comp-unitˡ pr₁ ∙
(pair-β₁ (id N ∘ pr₁) (swap ∘ pr₂) ∙
((Associativity.backward-first N I K ▷ s) ∙
((comp-assoc s b (pr₁ ∘ pr₁)) ⁻¹ ∙
project-pair₁ (pr₁ ∘ pr₁) (id K ∘ pr₂) (b ∘ s))))
right-first : (pr₁ ∘ (pr₁ ∘ r)) =₁ pr₁
right-first = Associativity.backward-first N K I ∙ (comp-assoc r pr₁ pr₁) ⁻¹
left-second : (pr₂ ∘ (productMap (pr₁ {C = N} {D = I}) (id K) ∘ (b ∘ s)))
=₁ (pr₁ ∘ (pr₂ {C = N} {D = K × I}))
left-second = (pair-β₂ pr₂ pr₁ ▷ pr₂) ∙
((comp-assoc pr₂ swap pr₂) ⁻¹ ∙
((pr₂ ◁ pair-β₂ (id N ∘ pr₁) (swap ∘ pr₂)) ∙
(comp-assoc s pr₂ pr₂ ∙
((Associativity.backward-third N I K ▷ s) ∙
((comp-assoc s b pr₂) ⁻¹ ∙
((comp-unitˡ pr₂ ▷ (b ∘ s)) ∙
project-pair₂ (pr₁ ∘ pr₁) (id K ∘ pr₂) (b ∘ s)))))))
right-second : (pr₂ ∘ (pr₁ ∘ r)) =₁ (pr₁ ∘ (pr₂ {C = N} {D = K × I}))
right-second = Associativity.backward-second N K I ∙ (comp-assoc r pr₁ pr₂) ⁻¹
constant-exponential : (I K X : CAT Γ)
→ (funPre {D = X} (swap {C = K} {D = I}) ∘
(ExponentialLaw.forward I K X ∘ constantArrow I (Fun K X)))
=₁ (ExponentialLaw.forward K I X ∘ funPost {C = K} (constantArrow I X))
constant-exponential I K X = reflect (funEval {C = K × I} {D = X})
(funUniversal (K × I) X) left-functor right-functor (right ⁻¹ ∙ ((eK ◁ arguments) ∙ left))
where
N : CAT Γ
N = Fun K X
eK : MAP (N × K) X
eK = funEval {C = K} {D = X}
s : MAP (N × (K × I)) (N × (I × K))
s = productMap (id N) (swap {C = K} {D = I})
b : MAP (N × (I × K)) ((N × I) × K)
b = Associativity.backward N I K
r : MAP (N × (K × I)) ((N × K) × I)
r = Associativity.backward N K I
d : MAP ((N × I) × K) (N × K)
d = productMap (pr₁ {C = N} {D = I}) (id K)
left-functor : MAP N (Fun (K × I) X)
left-functor = funPre {D = X} (swap {C = K} {D = I}) ∘
(ExponentialLaw.forward I K X ∘ constantArrow I N)
right-functor : MAP N (Fun (K × I) X)
right-functor = ExponentialLaw.forward K I X ∘ funPost {C = K} (constantArrow I X)
arguments : (d ∘ (b ∘ s)) =₁ (pr₁ ∘ r)
arguments = constant-exchange-arguments N I K
left : funUncurry {C = K × I} {D = X} left-functor =₁ (eK ∘ (d ∘ (b ∘ s)))
left = comp-assoc (b ∘ s) d eK ∙
(comp-assoc s b (eK ∘ d) ∙
(((evaluate-cong eK (constantArrow-image I N) ▷ b) ▷ s) ∙
((ExponentialLaw.forward-represents I K X (constantArrow I N) ▷ s) ∙
funPre-uncurry (swap {C = K} {D = I})
(ExponentialLaw.forward I K X ∘ constantArrow I N))))
right : funUncurry {C = K × I} {D = X} right-functor =₁ (eK ∘ (pr₁ ∘ r))
right = comp-assoc r pr₁ eK ∙
((constant-evaluation I X eK ▷ r) ∙
((evaluate-cong (funEval {C = I} {D = X})
(funPost-β {C = K} (constantArrow I X)) ▷ r) ∙
ExponentialLaw.forward-represents K I X (funPost {C = K} (constantArrow I X))))
functor-isGroupoid : (K : CAT Γ) {X : CAT Γ} → IsGroupoid X → IsGroupoid (Fun K X)
functor-isGroupoid K {X} given =
equiv-cancel-left (identityArrow {C = Fun K X}) (ExponentialLaw.forward [1] K X)
(ExponentialLaw.forward-isEquiv [1] K X)
(equiv-cancel-left (ExponentialLaw.forward [1] K X ∘ identityArrow {C = Fun K X})
(funPre {D = X} (swap {C = K} {D = [1]}))
(funPre-isEquiv {E = X} (swap {C = K} {D = [1]}) (swap-isEquiv K [1]))
(equiv-transport ((constant-exponential [1] K X) ⁻¹)
(equiv-compose (funPost {C = K} (identityArrow {C = X}))
(ExponentialLaw.forward K [1] X)
(funPost-isEquiv {A = K} (identityArrow {C = X}) given)
(ExponentialLaw.forward-isEquiv K [1] X))))
```