From 4ff8f155abc43d7a9423a2bf01c7be350e0f1369 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 11 Apr 2018 12:46:22 +0200
Subject: [PATCH] [QED] Get equivalence from 3rd formulation

---
 src/Cat/Category.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 8f39dac..a39dd27 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -150,11 +150,11 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
         lem : Σ Object (A ≅_) ≃ Σ Object (A ≡_)
         lem = equivSig {ℓa} {ℓb} {Object} {A ≅_} {_} {A ≡_} (f A)
 
-        aux : isContr (Σ[ B ∈ Object ] A ≡ B)
-        aux = {!Σ Object (A ≡_)!}
+        aux : isContr (Σ Object (A ≡_))
+        aux = (A , refl) , (λ y → contrSingl (snd y))
 
         step : isContr (Σ Object (A ≅_))
-        step = {!subst {P = isContr} {!!} aux!}
+        step = equivPreservesNType {n = ⟨-2⟩} (Equivalence.symmetry lem) aux
 
     propUnivalent : isProp Univalent
     propUnivalent a b i = propPi (λ iso → propIsContr) a b i