Rename id-to-iso to idToIso
This commit is contained in:
parent
b5f89322ac
commit
e69ace21a0
|
@ -6,7 +6,7 @@ Prove postulates in `Cat.Wishlist`:
|
||||||
|
|
||||||
Prove that these two formulations of univalence are equivalent:
|
Prove that these two formulations of univalence are equivalent:
|
||||||
|
|
||||||
∀ A B → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
|
∀ A B → isEquiv (A ≡ B) (A ≅ B) (idToIso A B)
|
||||||
∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
|
∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
|
||||||
|
|
||||||
Prove univalence for the category of
|
Prove univalence for the category of
|
||||||
|
|
|
@ -67,7 +67,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
||||||
IsPreCategory.arrowsAreSets isPreCategory = arrowsAreSets
|
IsPreCategory.arrowsAreSets isPreCategory = arrowsAreSets
|
||||||
|
|
||||||
module _ {A B : ℂ.Object} where
|
module _ {A B : ℂ.Object} where
|
||||||
eqv : isEquiv (A ≡ B) (A ≅ B) (Univalence.id-to-iso isIdentity A B)
|
eqv : isEquiv (A ≡ B) (A ≅ B) (Univalence.idToIso isIdentity A B)
|
||||||
eqv = {!!}
|
eqv = {!!}
|
||||||
|
|
||||||
univalent : Univalent
|
univalent : Univalent
|
||||||
|
|
|
@ -35,7 +35,7 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
|
||||||
|
|
||||||
module _ (F : Functor ℂ 𝔻) where
|
module _ (F : Functor ℂ 𝔻) where
|
||||||
center : Σ[ G ∈ Object ] (F ≅ G)
|
center : Σ[ G ∈ Object ] (F ≅ G)
|
||||||
center = F , id-to-iso F F refl
|
center = F , idToIso F F refl
|
||||||
|
|
||||||
open Σ center renaming (snd to isoF)
|
open Σ center renaming (snd to isoF)
|
||||||
|
|
||||||
|
@ -175,7 +175,7 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
|
||||||
re-ve : (x : A ≡ B) → reverse (obverse x) ≡ x
|
re-ve : (x : A ≡ B) → reverse (obverse x) ≡ x
|
||||||
re-ve = {!!}
|
re-ve = {!!}
|
||||||
|
|
||||||
done : isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
|
done : isEquiv (A ≡ B) (A ≅ B) (idToIso A B)
|
||||||
done = {!gradLemma obverse reverse ve-re re-ve!}
|
done = {!gradLemma obverse reverse ve-re re-ve!}
|
||||||
|
|
||||||
univalent : Univalent
|
univalent : Univalent
|
||||||
|
|
|
@ -114,11 +114,11 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
|
||||||
-- | Extract an isomorphism from an equality
|
-- | Extract an isomorphism from an equality
|
||||||
--
|
--
|
||||||
-- [HoTT §9.1.4]
|
-- [HoTT §9.1.4]
|
||||||
id-to-iso : (A B : Object) → A ≡ B → A ≅ B
|
idToIso : (A B : Object) → A ≡ B → A ≅ B
|
||||||
id-to-iso A B eq = transp (\ i → A ≅ eq i) (idIso A)
|
idToIso A B eq = transp (\ i → A ≅ eq i) (idIso A)
|
||||||
|
|
||||||
Univalent : Set (ℓa ⊔ ℓb)
|
Univalent : Set (ℓa ⊔ ℓb)
|
||||||
Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
|
Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (idToIso A B)
|
||||||
|
|
||||||
-- A perhaps more readable version of univalence:
|
-- A perhaps more readable version of univalence:
|
||||||
Univalent≃ = {A B : Object} → (A ≡ B) ≃ (A ≅ B)
|
Univalent≃ = {A B : Object} → (A ≡ B) ≃ (A ≅ B)
|
||||||
|
@ -149,7 +149,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
|
||||||
|
|
||||||
-- Some error with primComp
|
-- Some error with primComp
|
||||||
isoAY : A ≅ Y
|
isoAY : A ≅ Y
|
||||||
isoAY = {!id-to-iso A Y q!}
|
isoAY = {!idToIso A Y q!}
|
||||||
|
|
||||||
lem : PathP (λ i → A ≅ q i) (idIso A) isoY
|
lem : PathP (λ i → A ≅ q i) (idIso A) isoY
|
||||||
lem = d* isoAY
|
lem = d* isoAY
|
||||||
|
@ -548,7 +548,7 @@ module Opposite {ℓa ℓb : Level} where
|
||||||
|
|
||||||
module _ {A B : ℂ.Object} where
|
module _ {A B : ℂ.Object} where
|
||||||
open import Cat.Equivalence as Equivalence hiding (_≅_)
|
open import Cat.Equivalence as Equivalence hiding (_≅_)
|
||||||
k : Equivalence.Isomorphism (ℂ.id-to-iso A B)
|
k : Equivalence.Isomorphism (ℂ.idToIso A B)
|
||||||
k = Equiv≃.toIso _ _ ℂ.univalent
|
k = Equiv≃.toIso _ _ ℂ.univalent
|
||||||
open Σ k renaming (fst to f ; snd to inv)
|
open Σ k renaming (fst to f ; snd to inv)
|
||||||
open AreInverses inv
|
open AreInverses inv
|
||||||
|
@ -568,11 +568,11 @@ module Opposite {ℓa ℓb : Level} where
|
||||||
|
|
||||||
-- Shouldn't be necessary to use `arrowsAreSets` here, but we have it,
|
-- Shouldn't be necessary to use `arrowsAreSets` here, but we have it,
|
||||||
-- so why not?
|
-- so why not?
|
||||||
lem : (p : A ≡ B) → id-to-iso A B p ≡ flopDem (ℂ.id-to-iso A B p)
|
lem : (p : A ≡ B) → idToIso A B p ≡ flopDem (ℂ.idToIso A B p)
|
||||||
lem p i = l≡r i
|
lem p i = l≡r i
|
||||||
where
|
where
|
||||||
l = id-to-iso A B p
|
l = idToIso A B p
|
||||||
r = flopDem (ℂ.id-to-iso A B p)
|
r = flopDem (ℂ.idToIso A B p)
|
||||||
open Σ l renaming (fst to l-obv ; snd to l-areInv)
|
open Σ l renaming (fst to l-obv ; snd to l-areInv)
|
||||||
open Σ l-areInv renaming (fst to l-invs ; snd to l-iso)
|
open Σ l-areInv renaming (fst to l-invs ; snd to l-iso)
|
||||||
open Σ l-iso renaming (fst to l-l ; snd to l-r)
|
open Σ l-iso renaming (fst to l-l ; snd to l-r)
|
||||||
|
@ -593,27 +593,27 @@ module Opposite {ℓa ℓb : Level} where
|
||||||
ff : A ≅ B → A ≡ B
|
ff : A ≅ B → A ≡ B
|
||||||
ff = f ⊙ flipDem
|
ff = f ⊙ flipDem
|
||||||
|
|
||||||
-- inv : AreInverses (ℂ.id-to-iso A B) f
|
-- inv : AreInverses (ℂ.idToIso A B) f
|
||||||
invv : AreInverses (id-to-iso A B) ff
|
invv : AreInverses (idToIso A B) ff
|
||||||
-- recto-verso : ℂ.id-to-iso A B ∘ f ≡ idFun (A ℂ.≅ B)
|
-- recto-verso : ℂ.idToIso A B ∘ f ≡ idFun (A ℂ.≅ B)
|
||||||
invv = record
|
invv = record
|
||||||
{ verso-recto = funExt (λ x → begin
|
{ verso-recto = funExt (λ x → begin
|
||||||
(ff ⊙ id-to-iso A B) x ≡⟨⟩
|
(ff ⊙ idToIso A B) x ≡⟨⟩
|
||||||
(f ⊙ flipDem ⊙ id-to-iso A B) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → f ⊙ flipDem ⊙ φ) (funExt lem)) ⟩
|
(f ⊙ flipDem ⊙ idToIso A B) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → f ⊙ flipDem ⊙ φ) (funExt lem)) ⟩
|
||||||
(f ⊙ flipDem ⊙ flopDem ⊙ ℂ.id-to-iso A B) x ≡⟨⟩
|
(f ⊙ flipDem ⊙ flopDem ⊙ ℂ.idToIso A B) x ≡⟨⟩
|
||||||
(f ⊙ ℂ.id-to-iso A B) x ≡⟨ (λ i → verso-recto i x) ⟩
|
(f ⊙ ℂ.idToIso A B) x ≡⟨ (λ i → verso-recto i x) ⟩
|
||||||
x ∎)
|
x ∎)
|
||||||
; recto-verso = funExt (λ x → begin
|
; recto-verso = funExt (λ x → begin
|
||||||
(id-to-iso A B ⊙ f ⊙ flipDem) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ⊙ f ⊙ flipDem) (funExt lem)) ⟩
|
(idToIso A B ⊙ f ⊙ flipDem) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ⊙ f ⊙ flipDem) (funExt lem)) ⟩
|
||||||
(flopDem ⊙ ℂ.id-to-iso A B ⊙ f ⊙ flipDem) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → flopDem ⊙ φ ⊙ flipDem) recto-verso) ⟩
|
(flopDem ⊙ ℂ.idToIso A B ⊙ f ⊙ flipDem) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → flopDem ⊙ φ ⊙ flipDem) recto-verso) ⟩
|
||||||
(flopDem ⊙ flipDem) x ≡⟨⟩
|
(flopDem ⊙ flipDem) x ≡⟨⟩
|
||||||
x ∎)
|
x ∎)
|
||||||
}
|
}
|
||||||
|
|
||||||
h : Equivalence.Isomorphism (id-to-iso A B)
|
h : Equivalence.Isomorphism (idToIso A B)
|
||||||
h = ff , invv
|
h = ff , invv
|
||||||
univalent : isEquiv (A ≡ B) (A ≅ B)
|
univalent : isEquiv (A ≡ B) (A ≅ B)
|
||||||
(Univalence.id-to-iso (swap ℂ.isIdentity) A B)
|
(Univalence.idToIso (swap ℂ.isIdentity) A B)
|
||||||
univalent = Equiv≃.fromIso _ _ h
|
univalent = Equiv≃.fromIso _ _ h
|
||||||
|
|
||||||
isCategory : IsCategory opRaw
|
isCategory : IsCategory opRaw
|
||||||
|
|
|
@ -322,14 +322,14 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
||||||
f i = f0 i , {!f1 i!}
|
f i = f0 i , {!f1 i!}
|
||||||
prp : isSet (ℂ.Object × ℂ.Arrow Y A × ℂ.Arrow Y B)
|
prp : isSet (ℂ.Object × ℂ.Arrow Y A × ℂ.Arrow Y B)
|
||||||
prp = setSig {sA = {!!}} {(λ _ → setSig {sA = ℂ.arrowsAreSets} {λ _ → ℂ.arrowsAreSets})}
|
prp = setSig {sA = {!!}} {(λ _ → setSig {sA = ℂ.arrowsAreSets} {λ _ → ℂ.arrowsAreSets})}
|
||||||
ve-re : (p : (X , x) ≡ (Y , y)) → f (id-to-iso _ _ p) ≡ p
|
ve-re : (p : (X , x) ≡ (Y , y)) → f (idToIso _ _ p) ≡ p
|
||||||
-- ve-re p i j = {!ℂ.arrowsAreSets!} , ℂ.arrowsAreSets _ _ (let k = fst (snd (p i)) in {!!}) {!!} {!!} {!!} , {!!}
|
-- ve-re p i j = {!ℂ.arrowsAreSets!} , ℂ.arrowsAreSets _ _ (let k = fst (snd (p i)) in {!!}) {!!} {!!} {!!} , {!!}
|
||||||
ve-re p = let k = prp {!!} {!!} {!!} {!p!} in {!!}
|
ve-re p = let k = prp {!!} {!!} {!!} {!p!} in {!!}
|
||||||
re-ve : (iso : (X , x) ≅ (Y , y)) → id-to-iso _ _ (f iso) ≡ iso
|
re-ve : (iso : (X , x) ≅ (Y , y)) → idToIso _ _ (f iso) ≡ iso
|
||||||
re-ve = {!!}
|
re-ve = {!!}
|
||||||
iso : E.Isomorphism (id-to-iso (X , x) (Y , y))
|
iso : E.Isomorphism (idToIso (X , x) (Y , y))
|
||||||
iso = f , record { verso-recto = funExt ve-re ; recto-verso = funExt re-ve }
|
iso = f , record { verso-recto = funExt ve-re ; recto-verso = funExt re-ve }
|
||||||
res : isEquiv ((X , x) ≡ (Y , y)) ((X , x) ≅ (Y , y)) (id-to-iso (X , x) (Y , y))
|
res : isEquiv ((X , x) ≡ (Y , y)) ((X , x) ≅ (Y , y)) (idToIso (X , x) (Y , y))
|
||||||
res = Equiv≃.fromIso _ _ iso
|
res = Equiv≃.fromIso _ _ iso
|
||||||
|
|
||||||
isCat : IsCategory raw
|
isCat : IsCategory raw
|
||||||
|
|
Loading…
Reference in a new issue