From 7dc7a5aee37deb41f2c2ebea4b8e023f1a647bc8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 16 Feb 2018 12:03:02 +0100
Subject: [PATCH] Prove that naturalTransformations are sets

Also adds a new module `Cat.Wishlist` of things I hope to put get from
upstream `cubical`.
---
 src/Cat/Categories/Fun.agda | 60 +++++--------------------------------
 src/Cat/Wishlist.agda       |  6 ++++
 2 files changed, 14 insertions(+), 52 deletions(-)
 create mode 100644 src/Cat/Wishlist.agda

diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index 81e656f..522bb34 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -8,9 +8,13 @@ open import Data.Product
 import Cubical.GradLemma
 module UIP = Cubical.GradLemma
 open import Cubical.Sigma
+open import Cubical.NType
+open import Data.Nat using (_≤_ ; z≤n ; s≤s)
+module Nat = Data.Nat
 
 open import Cat.Category
 open import Cat.Category.Functor
+open import Cat.Wishlist
 
 open import Cat.Equality
 open Equality.Data.Product
@@ -103,16 +107,6 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       IsSet'   : {ℓ : Level} (A : Set ℓ) → Set ℓ
       IsSet' A = {x y : A} → (p q : (λ _ → A) [ x ≡ y ]) → p ≡ q
 
-      -- Example 3.1.6. in HoTT states that
-      -- If `B a` is a set for all `a : A` then `(a : A) → B a` is a set.
-      -- In the case below `B = Natural F G`.
-
-      -- naturalIsSet : (θ : Transformation F G) → IsSet' (Natural F G θ)
-      -- naturalIsSet = {!!}
-
-      -- isS : IsSet' ((θ : Transformation F G) → Natural F G θ)
-      -- isS = {!!}
-
       naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ)
       naturalIsProp θ θNat θNat' = lem
         where
@@ -120,48 +114,10 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
           lem = λ i f → 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i
 
       naturalTransformationIsSets : isSet (NaturalTransformation F G)
-      naturalTransformationIsSets = {!sigPresSet!}
-      -- f a b p q i = res
-      --   where
-      --     k : (θ : Transformation F G) → (xx yy : Natural F G θ) → xx ≡ yy
-      --     k θ x y = let kk = naturalIsProp θ x y in {!!}
-      --     res : a ≡ b
-      --     res j = {!!} , {!!}
-      -- -- naturalTransformationIsSets σa σb p q
-      --   -- where
-      --     -- -- In Andrea's proof `lemSig` he proves something very similiar to
-      --     -- -- what I'm doing here, just for `Cubical.FromPathPrelude.Σ` rather
-      --     -- -- than `Σ`. In that proof, he just needs *one* proof that the first
-      --     -- -- components are equal - hence the arbitrary usage of `p` here.
-      --     -- secretSauce : proj₁ σa ≡ proj₁ σb
-      --     -- secretSauce i = proj₁ (p i)
-      --     -- lemSig : σa ≡ σb
-      --     -- lemSig i = (secretSauce i) , (UIP.lemPropF naturalIsProp secretSauce) {proj₂ σa} {proj₂ σb} i
-      --     -- res : p ≡ q
-      --     -- res = {!!}
-      -- naturalTransformationIsSets (θ , θNat) (η , ηNat) p q i j
-      --   = θ-η
-      --   -- `i or `j - `p'` or `q'`?
-      --   , {!!} -- UIP.lemPropF {B = Natural F G} (λ x → {!!}) {(θ , θNat)} {(η , ηNat)} {!!} i
-      --   -- naturalIsSet i (λ i → {!!} i) {!!} {!!} i j
-      --   -- naturalIsSet {!p''!} {!p''!} {!!} i j
-      --   -- λ f k → 𝔻.arrowIsSet (λ l → proj₂ (p l) f k) (λ l → proj₂ (p l) f k) {!!} {!!}
-      --   where
-      --     θ≡η θ≡η' : θ ≡ η
-      --     θ≡η  i = proj₁ (p i)
-      --     θ≡η' i = proj₁ (q i)
-      --     θ-η : Transformation F G
-      --     θ-η = transformationIsSet _ _ θ≡η θ≡η' i j
-      --     θNat≡ηNat  : (λ i → Natural F G (θ≡η  i)) [ θNat ≡ ηNat ]
-      --     θNat≡ηNat  i = proj₂ (p i)
-      --     θNat≡ηNat' : (λ i → Natural F G (θ≡η' i)) [ θNat ≡ ηNat ]
-      --     θNat≡ηNat' i = proj₂ (q i)
-      --     k  : Natural F G (θ≡η  i)
-      --     k  = θNat≡ηNat  i
-      --     k' : Natural F G (θ≡η' i)
-      --     k' = θNat≡ηNat' i
-      --     t : Natural F G θ-η
-      --     t = naturalIsProp {!θ!} {!!} {!!} {!!}
+      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
diff --git a/src/Cat/Wishlist.agda b/src/Cat/Wishlist.agda
new file mode 100644
index 0000000..2e56a27
--- /dev/null
+++ b/src/Cat/Wishlist.agda
@@ -0,0 +1,6 @@
+module Cat.Wishlist where
+
+open import Cubical.NType
+open import Data.Nat using (_≤_ ; z≤n ; s≤s)
+
+postulate ntypeCommulative : ∀ {ℓ n m} {A : Set ℓ} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A