diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index da71f2c..07e2263 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -33,152 +33,13 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
 
     open IsPreCategory isPreCategory hiding (identity)
 
-    module _ (F : Functor ℂ 𝔻) where
-      center : Σ[ G ∈ Object ] (F ≅ G)
-      center = F , idToIso F F refl
-
-      open Σ center renaming (snd to isoF)
-
-      module _ (cG : Σ[ G ∈ Object ] (F ≅ G)) where
-        open Σ cG renaming (fst to G ; snd to isoG)
-        module G = Functor G
-        open Σ isoG   renaming (fst to θNT ; snd to invθNT)
-        open Σ invθNT renaming (fst to ηNT ; snd to areInv)
-        open Σ θNT    renaming (fst to θ   ; snd to θN)
-        open Σ ηNT    renaming (fst to η   ; snd to ηN)
-        open Σ areInv renaming (fst to ve-re ; snd to re-ve)
-
-        -- f ~ Transformation G G
-        -- f : (X : ℂ.Object) → 𝔻 [ G.omap X , G.omap X ]
-        -- f X = T[ θ ∘ η ] X
-        -- g = T[ η ∘ θ ] {!!}
-
-        ntF : NaturalTransformation F F
-        ntF = identity F
-
-        ntG : NaturalTransformation G G
-        ntG = identity G
-
-        idFunctor = Functors.identity
-
-        -- Dunno if this is the way to go, but if I can construct a an inverse of
-        -- G that is also inverse of F (possibly by being propositionally equal to
-        -- another functor F~)
-        postulate
-          G~ : Functor 𝔻 ℂ
-        F~ : Functor 𝔻 ℂ
-        F~ = G~
-        postulate
-          prop0 : F[ G~ ∘ G  ] ≡ idFunctor
-          prop1 : F[ F  ∘ G~ ] ≡ idFunctor
-
-        lem : F[ F  ∘ F~ ] ≡ idFunctor
-        lem = begin
-          F[ F  ∘ F~ ] ≡⟨⟩
-          F[ F  ∘ G~ ] ≡⟨ prop1 ⟩
-          idFunctor ∎
-
-        p0 : F ≡ G
-        p0 = begin
-          F                              ≡⟨ sym Functors.rightIdentity ⟩
-          F[ F           ∘ idFunctor ]   ≡⟨ cong (λ φ → F[ F ∘ φ ]) (sym prop0) ⟩
-          F[ F           ∘ F[ G~ ∘ G ] ] ≡⟨ Functors.isAssociative {F = G} {G = G~} {H = F} ⟩
-          F[ F[ F ∘ G~ ] ∘ G ]           ≡⟨⟩
-          F[ F[ F ∘ F~ ] ∘ G ]           ≡⟨ cong (λ φ → F[ φ ∘ G ]) lem ⟩
-          F[ idFunctor   ∘ G ]           ≡⟨ Functors.leftIdentity ⟩
-          G ∎
-
-        p1 : (λ i → Σ (Arrow F (p0 i)) (Isomorphism {A = F} {B = p0 i})) [ isoF ≡ isoG ]
-        p1 = {!!}
-
-        isContractible : (F , isoF) ≡ (G , isoG)
-        isContractible i = p0 i , p1 i
-
-      univalent[Contr] : isContr (Σ[ G ∈ Object ] (F ≅ G))
-      univalent[Contr] = center , isContractible
-
-    module _ {A B : Functor ℂ 𝔻} where
-      module A = Functor A
-      module B = Functor B
-      module _ (p : A ≡ B) where
-        omapP : A.omap ≡ B.omap
-        omapP i = Functor.omap (p i)
-
-        coerceAB : ∀ {X} → 𝔻 [ A.omap X , A.omap X ] ≡ 𝔻 [ A.omap X , B.omap X ]
-        coerceAB {X} = cong (λ φ → 𝔻 [ A.omap X , φ X ]) omapP
-
-        -- The transformation will be the identity on 𝔻. Such an arrow has the
-        -- type `A.omap A → A.omap A`. Which we can coerce to have the type
-        -- `A.omap → B.omap` since `A` and `B` are equal.
-        coeidentity : Transformation A B
-        coeidentity X = coe coerceAB 𝔻.identity
-
-        module _ {a b : ℂ.Object} (f : ℂ [ a , b ]) where
-          nat' : 𝔻 [ coeidentity b ∘ A.fmap f ] ≡ 𝔻 [ B.fmap f ∘ coeidentity a ]
-          nat' = begin
-            (𝔻 [ coeidentity b ∘ A.fmap f ]) ≡⟨ {!!} ⟩
-            (𝔻 [ B.fmap f ∘ coeidentity a ]) ∎
-
-        transs : (i : I) → Transformation A (p i)
-        transs = {!!}
-
-        natt : (i : I) → Natural A (p i) {!!}
-        natt = {!!}
-
-        t : Natural A B coeidentity
-        t = coe c (identityNatural A)
-          where
-          c : Natural A A (identityTrans A) ≡ Natural A B coeidentity
-          c = begin
-            Natural A A (identityTrans A) ≡⟨ (λ x → {!natt ?!}) ⟩
-            Natural A B coeidentity ∎
-          -- cong (λ φ → {!Natural A A (identityTrans A)!}) {!!}
-
-        k : Natural A A (identityTrans A) → Natural A B coeidentity
-        k n {a} {b} f = res
-          where
-          res : (𝔻 [ coeidentity b ∘ A.fmap f ]) ≡ (𝔻 [ B.fmap f ∘ coeidentity a ])
-          res = {!!}
-
-        nat : Natural A B coeidentity
-        nat = nat'
-
-        fromEq : NaturalTransformation A B
-        fromEq = coeidentity , nat
-
-    module _ {A B : Functor ℂ 𝔻} where
-      obverse : A ≡ B → A ≅ B
-      obverse p = res
-        where
-        ob  : Arrow A B
-        ob = fromEq p
-        re : Arrow B A
-        re = fromEq (sym p)
-        vr : _<<<_ {A = A} {B} {A} re ob ≡ identity A
-        vr = {!!}
-        rv : _<<<_ {A = B} {A} {B} ob re ≡ identity B
-        rv = {!!}
-        isInverse : IsInverseOf {A} {B} ob re
-        isInverse = vr , rv
-        iso : Isomorphism {A} {B} ob
-        iso = re , isInverse
-        res : A ≅ B
-        res = ob , iso
-
-      reverse : A ≅ B → A ≡ B
-      reverse iso = {!!}
-
-      ve-re : (y : A ≅ B) → obverse (reverse y) ≡ y
-      ve-re = {!!}
-
-      re-ve : (x : A ≡ B) → reverse (obverse x) ≡ x
-      re-ve = {!!}
-
-      done : isEquiv (A ≡ B) (A ≅ B) (idToIso A B)
-      done = {!gradLemma obverse reverse ve-re re-ve!}
-
-    univalent : Univalent
-    univalent = {!done!}
+    -- There used to be some work-in-progress on this theorem, please go back to
+    -- this point in time to see it:
+    --
+    -- commit 6b7d66b7fc936fe3674b2fd9fa790bd0e3fec12f
+    -- Author: Frederik Hanghøj Iversen <fhi.1990@gmail.com>
+    -- Date:   Fri Apr 13 15:26:46 2018 +0200
+    postulate univalent : Univalent
 
     isCategory : IsCategory raw
     IsCategory.isPreCategory isCategory = isPreCategory