From 5796b791b8f110503caf82c1e4e9f08f175fe7fc 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 13:59:35 +0100
Subject: [PATCH] Almost prove that arrows are sets in the cateogry of families

---
 src/Cat/Categories/Fam.agda | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda
index 7727a6d..d100b77 100644
--- a/src/Cat/Categories/Fam.agda
+++ b/src/Cat/Categories/Fam.agda
@@ -40,12 +40,29 @@ module _ (ℓa ℓb : Level) where
     isIdentity : IsIdentity λ { {A} → 𝟙 {A} }
     isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
 
+    open import Cubical.NType.Properties
+    open import Cubical.Sigma
     instance
       isCategory : IsCategory RawFam
       isCategory = record
         { isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {A} {B} {C} {D} {f} {g} {h}
         ; isIdentity = λ {A} {B} {f} → isIdentity {A} {B} {f = f}
-        ; arrowsAreSets = {!!}
+        ; arrowsAreSets = λ {
+          {((A , hA) , famA)}
+          {((B , hB) , famB)}
+            → setSig
+              {sA = setPi λ _ → hB}
+              {sB = λ f →
+                let
+                  helpr : isSet ((a : A) → proj₁ (famA a) → proj₁ (famB (f a)))
+                  helpr = setPi λ a → setPi λ _ → proj₂ (famB (f a))
+                  -- It's almost like above, but where the first argument is
+                  -- implicit.
+                  res : isSet ({a : A} → proj₁ (famA a) → proj₁ (famB (f a)))
+                  res = {!!}
+                in res
+              }
+          }
         ; univalent = {!!}
         }