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

Merge remote-tracking branch 'Saizan/dev' into dev

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-03-22 11:54:22 +01:00
parent d12122ce60 66ab7138a6
commit 52ca0b6732
1 changed files with 11 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -138,14 +138,10 @@ module _ (ℓ : Level) where
iso : (p ≡ q) Eqv.≅ (proj₁ p ≡ proj₁ q) iso : (p ≡ q) Eqv.≅ (proj₁ p ≡ proj₁ q)
iso = f , g , inv iso = f , g , inv
lem3 : {Q : A → Set ℓb} lem3 : ∀ {ℓc} {Q : A → Set (ℓc ⊔ ℓb)}
→ ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q → ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q
lem3 {Q} eA = res lem3 {Q = Q} eA = res
where where
P→Q : ∀ {a} → P a ≡ Q a
P→Q = ua (eA _)
Q→P : ∀ {a} → Q a ≡ P a
Q→P = sym P→Q
f : Σ A P → Σ A Q f : Σ A P → Σ A Q
f (a , pA) = a , _≃_.eqv (eA a) pA f (a , pA) = a , _≃_.eqv (eA a) pA
g : Σ A Q → Σ A P g : Σ A Q → Σ A P
@ -226,7 +222,7 @@ module _ (ℓ : Level) where
-- lem3 and the equivalence from lem4 -- lem3 and the equivalence from lem4
step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B) step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B)
step0 = lem3 (λ f → sym≃ (lem4 sA sB f)) step0 = lem3 {ℓc = lzero} (λ f → sym≃ (lem4 sA sB f))
-- univalence -- univalence
step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B) step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B)
step1 = hh ⊙ h step1 = hh ⊙ h
@ -340,8 +336,14 @@ module _ (ℓ : Level) where
isContractible = Σ≡ pObj {!isoEq!} isContractible = Σ≡ pObj {!isoEq!}
-- isContractible = lemSig prop≅ center y pObj -- isContractible = lemSig prop≅ center y pObj
univalent[Contr] : isContr (Σ[ hB ∈ Object ] hA ≅ hB) -- univalent[Contr] : isContr (Σ[ hB ∈ Object ] hA ≅ hB)
univalent[Contr] = center , isContractible -- univalent[Contr] = center , isContractible
eq1 : ∀ hA → (Σ[ hB ∈ Object ] hA ≅ hB) ≡ (Σ[ hB ∈ Object ] hA ≡ hB)
eq1 hA = ua (lem3 (\ hB → sym≃ thr))
univalent[Contr] : ∀ hA → isContr (Σ[ hB ∈ Object ] hA ≅ hB)
univalent[Contr] hA = subst {P = isContr} (sym (eq1 hA)) {!!}
univalent : Univalent univalent : Univalent
univalent = from[Contr] univalent[Contr] univalent = from[Contr] univalent[Contr]