module category-theory.functor-identity where
open import foundations.universe open import foundations.identity-type open import foundations.proposition open import foundations.function-extensionality open import foundations.retraction open import foundations.sigma-type open import foundations.function open import foundations.functions-are-functors open import foundations.homotopy open import foundations.greater-h-levels open import foundations.set open import category-theory.category open import category-theory.functor
private variable
o₁ h₁ o₂ h₂ : Level
module _ (e : FunExtAll)
(𝒞 : Category o₁ h₁) (𝒟 : Category o₂ h₂) where
private
module 𝒞 = Category 𝒞
module 𝒟 = Category 𝒟
isPropIsFunctor : ∀ (F : FunctorData 𝒞.𝒞 𝒟.𝒞) → isProp (isFunctor 𝒞 𝒟 F)
isPropIsFunctor F a b = q
where
module F = FunctorData F
module a = isFunctor a
module b = isFunctor b
p1 : a.preserve-id ＝ b.preserve-id
p1 = byFunExtType e a.preserve-id b.preserve-id
λ _ → 𝒟.is-set-hom _ _ _ _
p2 :
Id
(∀ {A B C} (f : 𝒞.Hom A B) (g : 𝒞.Hom B C) → F.₁ (g 𝒞.∘ f) ＝ F.₁ g 𝒟.∘ F.₁ f)
a.preserve-∘
b.preserve-∘
p2 = byFunExtImplicit e _ _
λ A → byFunExtImplicit e _ _
λ B → byFunExtImplicit e _ _
λ C → byFunExtType e _ _
λ f → byFunExtType e _ _
λ g → 𝒟.is-set-hom _ _ _ _
q : a ＝ b
q with p1 | p2
... | refl | refl = refl
fromFunctorId : ∀ (F G : Functor 𝒞 𝒟) → F ＝ G → Functor.F F ＝ Functor.F G
fromFunctorId _ _ = ap Functor.F
toFunctorId : ∀ (F G : Functor 𝒞 𝒟) → Functor.F F ＝ Functor.F G → F ＝ G
toFunctorId F G refl =
ap
(λ w → record { F = F.F ; is-functor = w })
(isPropIsFunctor G.F F.is-functor G.is-functor)
where
module F = Functor F
module G = Functor G
toFunctorIdはfromFunctorIdの逆写像となる。
hasRetractionFromFunctorId : ∀ F G
→ HasRetraction (fromFunctorId F G)
hasRetractionFromFunctorId F G .fst = toFunctorId F G
hasRetractionFromFunctorId F G .snd refl = ap (λ w → ap (λ x → record { F = G.F ; is-functor = x }) w) r
where
module F = Functor F
module G = Functor G
k : isSet (isFunctor 𝒞 𝒟 G.F)
k = isProp⇒isSet (isPropIsFunctor G.F)
r : isPropIsFunctor G.F F.is-functor G.is-functor ＝ refl
r = k F.is-functor G.is-functor (isPropIsFunctor G.F F.is-functor G.is-functor) refl