From 954a89f8d13167be0712121e37e12ddc18a90bc9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 23 Feb 2018 11:12:27 +0100
Subject: [PATCH] Expose `naturalIsProp`

---
 src/Cat/Categories/Fun.agda | 94 +++++++++++++++++--------------------
 1 file changed, 44 insertions(+), 50 deletions(-)

diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index ba492d0..b5a33c8 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -38,9 +38,6 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       → (f : ℂ [ A , B ])
       → 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ]
 
-    -- naturalIsProp : ∀ θ → isProp (Natural θ)
-    -- naturalIsProp θ x y = {!funExt!}
-
     NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
     NaturalTransformation = Σ Transformation Natural
 
@@ -100,59 +97,56 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     NatComp = _:⊕:_
 
   private
-    module _ {F G : Functor ℂ 𝔻} where
-      module 𝔻 = Category 𝔻
+    module 𝔻 = Category 𝔻
 
-      transformationIsSet : isSet (Transformation F G)
-      transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C)   (λ l → q l C) i j
-      IsSet'   : {ℓ : Level} (A : Set ℓ) → Set ℓ
-      IsSet' A = {x y : A} → (p q : (λ _ → A) [ x ≡ y ]) → p ≡ q
+  module _ {F G : Functor ℂ 𝔻} where
+    transformationIsSet : isSet (Transformation F G)
+    transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C)   (λ l → q l C) i j
 
-      naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ)
-      naturalIsProp θ θNat θNat' = lem
-        where
-          lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ]
-          lem = λ i f → 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i
+    naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ)
+    naturalIsProp θ θNat θNat' = lem
+      where
+        lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ]
+        lem = λ i f → 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i
 
-      naturalTransformationIsSets : isSet (NaturalTransformation F G)
-      naturalTransformationIsSets = sigPresSet transformationIsSet
-        λ θ → ntypeCommulative
-          (s≤s {n = Nat.suc Nat.zero} z≤n)
-          (naturalIsProp θ)
+    naturalTransformationIsSets : isSet (NaturalTransformation F G)
+    naturalTransformationIsSets = sigPresSet transformationIsSet
+      λ θ → ntypeCommulative
+        (s≤s {n = Nat.suc Nat.zero} z≤n)
+        (naturalIsProp θ)
 
-    module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B}
-      {η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where
-      private
-        θ = proj₁ θ'
-        η = proj₁ η'
-        ζ = proj₁ ζ'
-        θNat = proj₂ θ'
-        ηNat = proj₂ η'
-        ζNat = proj₂ ζ'
-        L : NaturalTransformation A D
-        L = (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ'))
-        R : NaturalTransformation A D
-        R = (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
-      _g⊕f_ = _:⊕:_ {A} {B} {C}
-      _h⊕g_ = _:⊕:_ {B} {C} {D}
-      :assoc: : L ≡ R
-      :assoc: = lemSig (naturalIsProp {F = A} {D})
-        L R (funExt (λ x → assoc))
-        where
-          open Category 𝔻
+  module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B}
+    {η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where
+    private
+      θ = proj₁ θ'
+      η = proj₁ η'
+      ζ = proj₁ ζ'
+      θNat = proj₂ θ'
+      ηNat = proj₂ η'
+      ζNat = proj₂ ζ'
+      L : NaturalTransformation A D
+      L = (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ'))
+      R : NaturalTransformation A D
+      R = (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
+    _g⊕f_ = _:⊕:_ {A} {B} {C}
+    _h⊕g_ = _:⊕:_ {B} {C} {D}
+    :assoc: : L ≡ R
+    :assoc: = lemSig (naturalIsProp {F = A} {D})
+      L R (funExt (λ x → assoc))
+      where
+        open Category 𝔻
 
+  private
     module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
-      private
-        allNatural = naturalIsProp {F = A} {B}
-        f' = proj₁ f
-        module 𝔻Data = Category 𝔻
-        eq-r : ∀ C → (𝔻 [ f' C ∘ identityTrans A C ]) ≡ f' C
-        eq-r C = begin
-          𝔻 [ f' C ∘ identityTrans A C ] ≡⟨⟩
-          𝔻 [ f' C ∘ 𝔻Data.𝟙 ]  ≡⟨ proj₁ (𝔻.ident {A} {B}) ⟩
-          f' C ∎
-        eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C
-        eq-l C = proj₂ (𝔻.ident {A} {B})
+      allNatural = naturalIsProp {F = A} {B}
+      f' = proj₁ f
+      eq-r : ∀ C → (𝔻 [ f' C ∘ identityTrans A C ]) ≡ f' C
+      eq-r C = begin
+        𝔻 [ f' C ∘ identityTrans A C ] ≡⟨⟩
+        𝔻 [ f' C ∘ 𝔻.𝟙 ]  ≡⟨ proj₁ 𝔻.ident ⟩
+        f' C ∎
+      eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C
+      eq-l C = proj₂ 𝔻.ident
       ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
       ident-r = lemSig allNatural _ _ (funExt eq-r)
       ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f