Reduce applications of symmetry
This commit is contained in:
parent
770bce52a2
commit
e6a2e3a0f0
|
@ -132,20 +132,16 @@ module _ (ℓ : Level) where
|
|||
open Σ hB renaming (fst to B ; snd to sB)
|
||||
|
||||
-- lem3 and the equivalence from lem4
|
||||
step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B)
|
||||
step0 = equivSig (λ f → sym≃ (lem4 sA sB f))
|
||||
|
||||
-- univalence
|
||||
step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B)
|
||||
step1 = sym≃ univalence
|
||||
step0 : Σ (A → B) (isEquiv A B) ≃ Σ (A → B) isIso
|
||||
step0 = equivSig (lem4 sA sB)
|
||||
|
||||
-- lem2 with propIsSet
|
||||
step2 : (A ≡ B) ≃ (hA ≡ hB)
|
||||
step2 = sym≃ (lem2 (λ A → isSetIsProp) hA hB)
|
||||
step2 : (hA ≡ hB) ≃ (A ≡ B)
|
||||
step2 = lem2 (λ A → isSetIsProp) hA hB
|
||||
|
||||
-- Go from an isomorphism on sets to an isomorphism on homotopic sets
|
||||
trivial? : (hA ≅ hB) ≃ (A ≈ B)
|
||||
trivial? = sym≃ (fromIsomorphism _ _ res)
|
||||
trivial? : (A ≈ B) ≃ (hA ≅ hB)
|
||||
trivial? = fromIsomorphism _ _ res
|
||||
where
|
||||
fwd : Σ (A → B) isIso → hA ≅ hB
|
||||
fwd (f , g , inv) = f , g , inv.toPair
|
||||
|
@ -155,12 +151,8 @@ module _ (ℓ : Level) where
|
|||
bwd (f , g , x , y) = f , g , record { verso-recto = x ; recto-verso = y }
|
||||
res : Σ (A → B) isIso ≈ (hA ≅ hB)
|
||||
res = fwd , bwd , record { verso-recto = refl ; recto-verso = refl }
|
||||
|
||||
conclusion : (hA ≅ hB) ≃ (hA ≡ hB)
|
||||
conclusion = trivial? ⊙ step0 ⊙ step1 ⊙ step2
|
||||
|
||||
univ≃ : (hA ≅ hB) ≃ (hA ≡ hB)
|
||||
univ≃ = trivial? ⊙ step0 ⊙ step1 ⊙ step2
|
||||
univ≃ : (hA ≡ hB) ≃ (hA ≅ hB)
|
||||
univ≃ = step2 ⊙ univalence ⊙ step0 ⊙ trivial?
|
||||
|
||||
univalent : Univalent
|
||||
univalent = from[Andrea] (λ _ _ → univ≃)
|
||||
|
|
|
@ -135,7 +135,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
|
|||
Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
|
||||
|
||||
Univalent[Andrea] : Set _
|
||||
Univalent[Andrea] = ∀ A B → (A ≅ B) ≃ (A ≡ B)
|
||||
Univalent[Andrea] = ∀ A B → (A ≡ B) ≃ (A ≅ B)
|
||||
|
||||
-- From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
|
||||
-- Date: Wed, Mar 21, 2018 at 3:12 PM
|
||||
|
@ -147,14 +147,14 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
|
|||
from[Andrea] = from[Contr] ∘ step
|
||||
where
|
||||
module _ (f : Univalent[Andrea]) (A : Object) where
|
||||
lem : Σ Object (A ≅_) ≃ Σ Object (A ≡_)
|
||||
lem = equivSig {ℓa} {ℓb} {Object} {A ≅_} {_} {A ≡_} (f A)
|
||||
lem : Σ Object (A ≡_) ≃ Σ Object (A ≅_)
|
||||
lem = equivSig (f A)
|
||||
|
||||
aux : isContr (Σ Object (A ≡_))
|
||||
aux = (A , refl) , (λ y → contrSingl (snd y))
|
||||
|
||||
step : isContr (Σ Object (A ≅_))
|
||||
step = equivPreservesNType {n = ⟨-2⟩} (Equivalence.symmetry lem) aux
|
||||
step = equivPreservesNType {n = ⟨-2⟩} lem aux
|
||||
|
||||
propUnivalent : isProp Univalent
|
||||
propUnivalent a b i = propPi (λ iso → propIsContr) a b i
|
||||
|
|
|
@ -171,10 +171,6 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
|
||||
open IsPreCategory isPreCat
|
||||
|
||||
univalent : Univalent
|
||||
univalent {(X , xa , xb)} {(Y , ya , yb)} = {!!}
|
||||
|
||||
-- module _ {(X , xa , xb) : Object} {(Y , ya , yb) : Object} where
|
||||
module _ (𝕏 𝕐 : Object) where
|
||||
open Σ 𝕏 renaming (fst to X ; snd to x)
|
||||
open Σ x renaming (fst to xa ; snd to xb)
|
||||
|
@ -298,13 +294,9 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
: ((X , xa , xb) ≡ (Y , ya , yb))
|
||||
≃ ((X , xa , xb) ≅ (Y , ya , yb))
|
||||
equiv1 = _ , fromIso _ _ (snd iso)
|
||||
equiv4reel
|
||||
: ((X , xa , xb) ≅ (Y , ya , yb))
|
||||
≃ ((X , xa , xb) ≡ (Y , ya , yb))
|
||||
equiv4reel = {!!}
|
||||
|
||||
univalent' : Univalent
|
||||
univalent' = from[Andrea] equiv4reel
|
||||
univalent : Univalent
|
||||
univalent = from[Andrea] equiv1
|
||||
|
||||
isCat : IsCategory raw
|
||||
IsCategory.isPreCategory isCat = isPreCat
|
||||
|
|
Loading…
Reference in a new issue