From 770bce52a26dd82aba3fb8367db42d2bb33c1ca5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 11 Apr 2018 12:54:22 +0200 Subject: [PATCH] Use 3rd formulation of univalence --- src/Cat/Categories/Sets.agda | 19 +------------------ 1 file changed, 1 insertion(+), 18 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index a0982fd..be62a35 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -162,25 +162,8 @@ module _ (ℓ : Level) where univ≃ : (hA ≅ hB) ≃ (hA ≡ hB) univ≃ = trivial? ⊙ step0 ⊙ step1 ⊙ step2 - module _ (hA : Object) where - open Σ hA renaming (fst to A) - - eq1 : (Σ[ hB ∈ Object ] hA ≅ hB) ≡ (Σ[ hB ∈ Object ] hA ≡ hB) - eq1 = ua (equivSig (\ hB → univ≃)) - - univalent[Contr] : isContr (Σ[ hB ∈ Object ] hA ≅ hB) - univalent[Contr] = subst {P = isContr} (sym eq1) tres - where - module _ (y : Σ[ hB ∈ Object ] hA ≡ hB) where - open Σ y renaming (fst to hB ; snd to hA≡hB) - qres : (hA , refl) ≡ (hB , hA≡hB) - qres = contrSingl hA≡hB - - tres : isContr (Σ[ hB ∈ Object ] hA ≡ hB) - tres = (hA , refl) , qres - univalent : Univalent - univalent = from[Contr] univalent[Contr] + univalent = from[Andrea] (λ _ _ → univ≃) SetsIsCategory : IsCategory SetsRaw IsCategory.isPreCategory SetsIsCategory = isPreCat