fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Use 3rd formulation of univalence

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-04-11 12:54:22 +02:00
parent 4ff8f155ab
commit 770bce52a2
1 changed files with 1 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/Cat/Categories/Sets.agda
View file

@ -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