Simplifications and renaming
This commit is contained in:
parent
735b25de23
commit
04144db606
|
|
@ -121,9 +121,6 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
|
||||||
Univalent : Set (ℓa ⊔ ℓb)
|
Univalent : Set (ℓa ⊔ ℓb)
|
||||||
Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (idToIso A B)
|
Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (idToIso A B)
|
||||||
|
|
||||||
import Cat.Equivalence as E
|
|
||||||
open E public using () renaming (Isomorphism to TypeIsomorphism)
|
|
||||||
|
|
||||||
univalenceFromIsomorphism : {A B : Object}
|
univalenceFromIsomorphism : {A B : Object}
|
||||||
→ TypeIsomorphism (idToIso A B) → isEquiv (A ≡ B) (A ≅ B) (idToIso A B)
|
→ TypeIsomorphism (idToIso A B) → isEquiv (A ≡ B) (A ≅ B) (idToIso A B)
|
||||||
univalenceFromIsomorphism = fromIso _ _
|
univalenceFromIsomorphism = fromIso _ _
|
||||||
|
|
@ -305,6 +302,9 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
|
||||||
iso-to-id : (A ≅ B) → (A ≡ B)
|
iso-to-id : (A ≅ B) → (A ≡ B)
|
||||||
iso-to-id = fst (toIso _ _ univalent)
|
iso-to-id = fst (toIso _ _ univalent)
|
||||||
|
|
||||||
|
asTypeIso : TypeIsomorphism (idToIso A B)
|
||||||
|
asTypeIso = toIso _ _ univalent
|
||||||
|
|
||||||
-- | All projections are propositions.
|
-- | All projections are propositions.
|
||||||
module Propositionality where
|
module Propositionality where
|
||||||
-- | Terminal objects are propositional - a.k.a uniqueness of terminal
|
-- | Terminal objects are propositional - a.k.a uniqueness of terminal
|
||||||
|
|
@ -333,10 +333,8 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
|
||||||
right = Yprop _ _
|
right = Yprop _ _
|
||||||
iso : X ≅ Y
|
iso : X ≅ Y
|
||||||
iso = X→Y , Y→X , left , right
|
iso = X→Y , Y→X , left , right
|
||||||
fromIso' : X ≅ Y → X ≡ Y
|
|
||||||
fromIso' = fst (toIso (X ≡ Y) (X ≅ Y) univalent)
|
|
||||||
p0 : X ≡ Y
|
p0 : X ≡ Y
|
||||||
p0 = fromIso' iso
|
p0 = iso-to-id iso
|
||||||
p1 : (λ i → IsTerminal (p0 i)) [ Xit ≡ Yit ]
|
p1 : (λ i → IsTerminal (p0 i)) [ Xit ≡ Yit ]
|
||||||
p1 = lemPropF propIsTerminal p0
|
p1 = lemPropF propIsTerminal p0
|
||||||
res : Xt ≡ Yt
|
res : Xt ≡ Yt
|
||||||
|
|
@ -365,14 +363,8 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
|
||||||
right = Xprop _ _
|
right = Xprop _ _
|
||||||
iso : X ≅ Y
|
iso : X ≅ Y
|
||||||
iso = Y→X , X→Y , right , left
|
iso = Y→X , X→Y , right , left
|
||||||
fromIso' : X ≅ Y → X ≡ Y
|
|
||||||
fromIso' = fst (toIso (X ≡ Y) (X ≅ Y) univalent)
|
|
||||||
p0 : X ≡ Y
|
|
||||||
p0 = fromIso' iso
|
|
||||||
p1 : (λ i → IsInitial (p0 i)) [ Xii ≡ Yii ]
|
|
||||||
p1 = lemPropF propIsInitial p0
|
|
||||||
res : Xi ≡ Yi
|
res : Xi ≡ Yi
|
||||||
res i = p0 i , p1 i
|
res = lemSig propIsInitial _ _ (iso-to-id iso)
|
||||||
|
|
||||||
module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
|
module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
|
||||||
open RawCategory ℂ
|
open RawCategory ℂ
|
||||||
|
|
@ -495,72 +487,62 @@ module Opposite {ℓa ℓb : Level} where
|
||||||
module _ {A B : ℂ.Object} where
|
module _ {A B : ℂ.Object} where
|
||||||
k : Equivalence.Isomorphism (ℂ.idToIso A B)
|
k : Equivalence.Isomorphism (ℂ.idToIso A B)
|
||||||
k = toIso _ _ ℂ.univalent
|
k = toIso _ _ ℂ.univalent
|
||||||
open Σ k renaming (fst to f ; snd to inv)
|
open Σ k renaming (fst to η ; snd to inv-η)
|
||||||
open AreInverses inv
|
open AreInverses inv-η
|
||||||
|
|
||||||
_⊙_ = Function._∘_
|
_⊙_ = Function._∘_
|
||||||
infixr 9 _⊙_
|
infixr 9 _⊙_
|
||||||
|
|
||||||
-- f : A ℂ.≅ B → A ≡ B
|
genericly : {ℓa ℓb ℓc : Level} {a : Set ℓa} {b : Set ℓb} {c : Set ℓc}
|
||||||
flipDem : A ≅ B → A ℂ.≅ B
|
→ a × b × c → b × a × c
|
||||||
flipDem (f , g , inv) = g , f , inv
|
genericly (a , b , c) = (b , a , c)
|
||||||
|
|
||||||
flopDem : A ℂ.≅ B → A ≅ B
|
shuffle : A ≅ B → A ℂ.≅ B
|
||||||
flopDem (f , g , inv) = g , f , inv
|
shuffle (f , g , inv) = g , f , inv
|
||||||
|
|
||||||
|
shuffle~ : A ℂ.≅ B → A ≅ B
|
||||||
|
shuffle~ (f , g , inv) = g , f , inv
|
||||||
|
|
||||||
-- 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) → idToIso A B p ≡ flopDem (ℂ.idToIso A B p)
|
lem : (p : A ≡ B) → idToIso A B p ≡ shuffle~ (ℂ.idToIso A B p)
|
||||||
lem p i = l≡r i
|
lem p = Σ≡ refl (Σ≡ refl (Σ≡ (ℂ.arrowsAreSets _ _ l-l r-l) (ℂ.arrowsAreSets _ _ l-r r-r)))
|
||||||
where
|
where
|
||||||
l = idToIso A B p
|
l = idToIso A B p
|
||||||
r = flopDem (ℂ.idToIso A B p)
|
r = shuffle~ (ℂ.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)
|
||||||
open Σ r renaming (fst to r-obv ; snd to r-areInv)
|
open Σ r renaming (fst to r-obv ; snd to r-areInv)
|
||||||
open Σ r-areInv renaming (fst to r-invs ; snd to r-iso)
|
open Σ r-areInv renaming (fst to r-invs ; snd to r-iso)
|
||||||
open Σ r-iso renaming (fst to r-l ; snd to r-r)
|
open Σ r-iso renaming (fst to r-l ; snd to r-r)
|
||||||
l-obv≡r-obv : l-obv ≡ r-obv
|
|
||||||
l-obv≡r-obv = refl
|
|
||||||
l-invs≡r-invs : l-invs ≡ r-invs
|
|
||||||
l-invs≡r-invs = refl
|
|
||||||
l-l≡r-l : l-l ≡ r-l
|
|
||||||
l-l≡r-l = ℂ.arrowsAreSets _ _ l-l r-l
|
|
||||||
l-r≡r-r : l-r ≡ r-r
|
|
||||||
l-r≡r-r = ℂ.arrowsAreSets _ _ l-r r-r
|
|
||||||
l≡r : l ≡ r
|
|
||||||
l≡r i = l-obv≡r-obv i , l-invs≡r-invs i , l-l≡r-l i , l-r≡r-r i
|
|
||||||
|
|
||||||
ff : A ≅ B → A ≡ B
|
ζ : A ≅ B → A ≡ B
|
||||||
ff = f ⊙ flipDem
|
ζ = η ⊙ shuffle
|
||||||
|
|
||||||
-- inv : AreInverses (ℂ.idToIso A B) f
|
-- inv : AreInverses (ℂ.idToIso A B) f
|
||||||
invv : AreInverses (idToIso A B) ff
|
inv-ζ : AreInverses (idToIso A B) ζ
|
||||||
-- recto-verso : ℂ.idToIso A B ∘ f ≡ idFun (A ℂ.≅ B)
|
-- recto-verso : ℂ.idToIso A B ∘ f ≡ idFun (A ℂ.≅ B)
|
||||||
invv = record
|
inv-ζ = record
|
||||||
{ verso-recto = funExt (λ x → begin
|
{ verso-recto = funExt (λ x → begin
|
||||||
(ff ⊙ idToIso A B) x ≡⟨⟩
|
(ζ ⊙ idToIso A B) x ≡⟨⟩
|
||||||
(f ⊙ flipDem ⊙ idToIso A B) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → f ⊙ flipDem ⊙ φ) (funExt lem)) ⟩
|
(η ⊙ shuffle ⊙ idToIso A B) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ⊙ shuffle ⊙ φ) (funExt lem)) ⟩
|
||||||
(f ⊙ flipDem ⊙ flopDem ⊙ ℂ.idToIso A B) x ≡⟨⟩
|
(η ⊙ shuffle ⊙ shuffle~ ⊙ ℂ.idToIso A B) x ≡⟨⟩
|
||||||
(f ⊙ ℂ.idToIso A B) x ≡⟨ (λ i → verso-recto i x) ⟩
|
(η ⊙ ℂ.idToIso A B) x ≡⟨ (λ i → verso-recto i x) ⟩
|
||||||
x ∎)
|
x ∎)
|
||||||
; recto-verso = funExt (λ x → begin
|
; recto-verso = funExt (λ x → begin
|
||||||
(idToIso A B ⊙ f ⊙ flipDem) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ⊙ f ⊙ flipDem) (funExt lem)) ⟩
|
(idToIso A B ⊙ η ⊙ shuffle) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ⊙ η ⊙ shuffle) (funExt lem)) ⟩
|
||||||
(flopDem ⊙ ℂ.idToIso A B ⊙ f ⊙ flipDem) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → flopDem ⊙ φ ⊙ flipDem) recto-verso) ⟩
|
(shuffle~ ⊙ ℂ.idToIso A B ⊙ η ⊙ shuffle) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → shuffle~ ⊙ φ ⊙ shuffle) recto-verso) ⟩
|
||||||
(flopDem ⊙ flipDem) x ≡⟨⟩
|
(shuffle~ ⊙ shuffle) x ≡⟨⟩
|
||||||
x ∎)
|
x ∎)
|
||||||
}
|
}
|
||||||
|
|
||||||
h : Equivalence.Isomorphism (idToIso A B)
|
h : Equivalence.Isomorphism (idToIso A B)
|
||||||
h = ff , invv
|
h = ζ , inv-ζ
|
||||||
univalent : isEquiv (A ≡ B) (A ≅ B)
|
|
||||||
(Univalence.idToIso (swap ℂ.isIdentity) A B)
|
|
||||||
univalent = fromIso _ _ h
|
|
||||||
|
|
||||||
isCategory : IsCategory opRaw
|
isCategory : IsCategory opRaw
|
||||||
IsCategory.isPreCategory isCategory = isPreCategory
|
IsCategory.isPreCategory isCategory = isPreCategory
|
||||||
IsCategory.univalent isCategory = univalent
|
IsCategory.univalent isCategory = univalenceFromIsomorphism h
|
||||||
|
|
||||||
opposite : Category ℓa ℓb
|
opposite : Category ℓa ℓb
|
||||||
Category.raw opposite = opRaw
|
Category.raw opposite = opRaw
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue