diff --git a/Cubical/Categories/Instances/Cat.agda b/Cubical/Categories/Instances/Cat.agda
index 3fa88518b..845e113a3 100644
--- a/Cubical/Categories/Instances/Cat.agda
+++ b/Cubical/Categories/Instances/Cat.agda
@@ -35,46 +35,3 @@ module _ (ℓ ℓ' : Level) where
   ⋆IdR Cat _ = F-rUnit
   ⋆Assoc Cat _ _ _ = F-assoc
   isSetHom Cat {y = _ , isSetObY} = isSetFunctor isSetObY
-
-
-  -- isUnivalentCat : isUnivalent Cat
-  -- isUnivalent.univ isUnivalentCat (C , isSmallC) (C' , isSmallC') =
-  --   {!!}
-
-  --  where
-  --  w : Iso (CategoryPath C C') (CatIso Cat (C , isSmallC) (C' , isSmallC'))
-  --  Iso.fun w = pathToIso ∘ Σ≡Prop (λ _ → isPropIsSet) ∘ CategoryPath.mk≡
-  --  Iso.inv w (m , isiso inv sec ret) = ww
-  --    where
-  --     obIsom : Iso (C .ob) (C' .ob)
-  --     Iso.fun obIsom = F-ob m
-  --     Iso.inv obIsom = F-ob inv
-  --     Iso.rightInv obIsom = cong F-ob sec ≡$_
-  --     Iso.leftInv obIsom = cong F-ob ret ≡$_
-
-  --     homIsom : (x y : C .ob) →
-  --                 Iso (C .Hom[_,_] x y)
-  --                 (C' .Hom[_,_] (fst (isoToEquiv obIsom) x)
-  --                 (fst (isoToEquiv obIsom) y))
-  --     Iso.fun (homIsom x y) = F-hom m
-  --     Iso.inv (homIsom x y) f =
-  --       subst2 (C [_,_]) (cong F-ob ret ≡$ x) ((cong F-ob ret ≡$ y))
-  --         (F-hom inv f)
-
-  --     Iso.rightInv (homIsom x y) b =
-  --       -- cong (F-hom m)
-  --       --   (fromPathP {A = (λ i → Hom[ C , F-ob (ret i) x ] (F-ob (ret i) y))}
-  --       --    {!!}) ∙
-  --         {!!} ∙
-  --         λ i → (fromPathP (cong F-hom sec)) i b
-  --       -- {!!} ∙ λ i → {!sec i .F-hom b!}
-  --     Iso.leftInv (homIsom x y) a = {!!}
-
-  --     open CategoryPath
-  --     ww : CategoryPath C C'
-  --     ob≡ ww = ua (isoToEquiv obIsom)
-  --     Hom≡ ww = RelPathP _ λ x y → isoToEquiv $ homIsom x y
-  --     id≡ ww = {!!}
-  --     ⋆≡ ww = {!!}
-  --  Iso.rightInv w = {!!}
-  --  Iso.leftInv w = {!!}