Distinguish isomorphism of categories and of types

This commit is contained in:
Frederik Hanghøj Iversen 2018-04-19 12:20:44 +02:00
parent 98b90f2370
commit 313c7593d1
9 changed files with 226 additions and 58 deletions

View file

@ -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.idToIso isIdentity A B) eqv : isEquiv (A B) (A B) (Univalence.idToIso isIdentity A B)
eqv = {!!} eqv = {!!}
univalent : Univalent univalent : Univalent

View file

@ -2,6 +2,7 @@
module Cat.Categories.Fun where module Cat.Categories.Fun where
open import Cat.Prelude open import Cat.Prelude
open import Cat.Equivalence
open import Cat.Category open import Cat.Category
open import Cat.Category.Functor open import Cat.Category.Functor
@ -33,13 +34,140 @@ module Fun {c c' d d' : Level} ( : Category c c') (𝔻 : C
open IsPreCategory isPreCategory hiding (identity) open IsPreCategory isPreCategory hiding (identity)
module _ {F G : Functor 𝔻} (p : F G) where
private
module F = Functor F
module G = Functor G
p-omap : F.omap G.omap
p-omap = cong Functor.omap p
pp : {C : .Object} 𝔻 [ Functor.omap F C , Functor.omap F C ] 𝔻 [ Functor.omap F C , Functor.omap G C ]
pp {C} = cong (λ f 𝔻 [ Functor.omap F C , f C ]) p-omap
module _ {C : .Object} where
p* : F.omap C G.omap C
p* = cong (_$ C) p-omap
iso : F.omap C 𝔻.≊ G.omap C
iso = 𝔻.idToIso _ _ p*
open Σ iso renaming (fst to f→g) public
open Σ (snd iso) renaming (fst to g→f ; snd to inv) public
lem : coe (pp {C}) 𝔻.identity f→g
lem = trans (𝔻.9-1-9-right {b = Functor.omap F C} 𝔻.identity p*) 𝔻.rightIdentity
idToNatTrans : NaturalTransformation F G
idToNatTrans = (λ C coe pp 𝔻.identity) , λ f begin
coe pp 𝔻.identity 𝔻.<<< F.fmap f ≡⟨ cong (𝔻._<<< F.fmap f) lem
-- Just need to show that f→g is a natural transformation
-- I know that it has an inverse; g→f
f→g 𝔻.<<< F.fmap f ≡⟨ {!lem!}
G.fmap f 𝔻.<<< f→g ≡⟨ cong (G.fmap f 𝔻.<<<_) (sym lem)
G.fmap f 𝔻.<<< coe pp 𝔻.identity
module _ {A B : Functor 𝔻} where
module A = Functor A
module B = Functor B
module _ (iso : A B) where
omapEq : A.omap B.omap
omapEq = funExt eq
where
module _ (C : .Object) where
f : 𝔻.Arrow (A.omap C) (B.omap C)
f = fst (fst iso) C
g : 𝔻.Arrow (B.omap C) (A.omap C)
g = fst (fst (snd iso)) C
inv : 𝔻.IsInverseOf f g
inv
= ( begin
g 𝔻.<<< f ≡⟨ cong (λ x fst x $ C) (fst (snd (snd iso)))
𝔻.identity
)
, ( begin
f 𝔻.<<< g ≡⟨ cong (λ x fst x $ C) (snd (snd (snd iso)))
𝔻.identity
)
isoC : A.omap C 𝔻.≊ B.omap C
isoC = f , g , inv
eq : A.omap C B.omap C
eq = 𝔻.isoToId isoC
U : (F : .Object 𝔻.Object) Set _
U F = {A B : .Object} [ A , B ] 𝔻 [ F A , F B ]
module _
(omap : .Object 𝔻.Object)
(p : A.omap omap)
where
D : Set _
D = ( fmap : U omap)
( let
raw-B : RawFunctor 𝔻
raw-B = record { omap = omap ; fmap = fmap }
)
(isF-B' : IsFunctor 𝔻 raw-B)
( let
B' : Functor 𝔻
B' = record { raw = raw-B ; isFunctor = isF-B' }
)
(iso' : A B') PathP (λ i U (p i)) A.fmap fmap
-- D : Set _
-- D = PathP (λ i → U (p i)) A.fmap fmap
-- eeq : (λ f → A.fmap f) ≡ fmap
-- eeq = funExtImp (λ A → funExtImp (λ B → funExt (λ f → isofmap {A} {B} f)))
-- where
-- module _ {X : .Object} {Y : .Object} (f : [ X , Y ]) where
-- isofmap : A.fmap f ≡ fmap f
-- isofmap = {!ap!}
d : D A.omap refl
d = res
where
module _
( fmap : U A.omap )
( let
raw-B : RawFunctor 𝔻
raw-B = record { omap = A.omap ; fmap = fmap }
)
( isF-B' : IsFunctor 𝔻 raw-B )
( let
B' : Functor 𝔻
B' = record { raw = raw-B ; isFunctor = isF-B' }
)
( iso' : A B' )
where
module _ {X Y : .Object} (f : [ X , Y ]) where
step : {!!} 𝔻.≊ {!!}
step = {!!}
resres : A.fmap {X} {Y} f fmap {X} {Y} f
resres = {!!}
res : PathP (λ i U A.omap) A.fmap fmap
res i {X} {Y} f = resres f i
fmapEq : PathP (λ i U (omapEq i)) A.fmap B.fmap
fmapEq = pathJ D d B.omap omapEq B.fmap B.isFunctor iso
rawEq : A.raw B.raw
rawEq i = record { omap = omapEq i ; fmap = fmapEq i }
private
f : (A B) (A B)
f p = idToNatTrans p , idToNatTrans (sym p) , NaturalTransformation≡ A A (funExt (λ C {!!})) , {!!}
g : (A B) (A B)
g = Functor≡ rawEq
inv : AreInverses f g
inv = {!funExt λ p → ?!} , {!!}
iso : (A B) (A B)
iso = f , g , inv
univ : (A B) (A B)
univ = fromIsomorphism _ _ iso
-- There used to be some work-in-progress on this theorem, please go back to -- There used to be some work-in-progress on this theorem, please go back to
-- this point in time to see it: -- this point in time to see it:
-- --
-- commit 6b7d66b7fc936fe3674b2fd9fa790bd0e3fec12f -- commit 6b7d66b7fc936fe3674b2fd9fa790bd0e3fec12f
-- Author: Frederik Hanghøj Iversen <fhi.1990@gmail.com> -- Author: Frederik Hanghøj Iversen <fhi.1990@gmail.com>
-- Date: Fri Apr 13 15:26:46 2018 +0200 -- Date: Fri Apr 13 15:26:46 2018 +0200
postulate univalent : Univalent univalent : Univalent
univalent = univalenceFrom≃ univ
isCategory : IsCategory raw isCategory : IsCategory raw
IsCategory.isPreCategory isCategory = isPreCategory IsCategory.isPreCategory isCategory = isPreCategory

View file

@ -8,7 +8,7 @@ open import Cat.Category
open import Cat.Category.Functor open import Cat.Category.Functor
open import Cat.Category.Product open import Cat.Category.Product
open import Cat.Wishlist open import Cat.Wishlist
open import Cat.Equivalence renaming (_≅_ to _≈_) open import Cat.Equivalence
_⊙_ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} (A B) (B C) A C _⊙_ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c} (A B) (B C) A C
eqA eqB = Equivalence.compose eqA eqB eqA eqB = Equivalence.compose eqA eqB
@ -93,7 +93,7 @@ module _ ( : Level) where
re-ve e = refl re-ve e = refl
inv : AreInverses (f {p} {q}) (g {p} {q}) inv : AreInverses (f {p} {q}) (g {p} {q})
inv = funExt ve-re , funExt re-ve inv = funExt ve-re , funExt re-ve
iso : (p q) (fst p fst q) iso : (p q) (fst p fst q)
iso = f , g , inv iso = f , g , inv
module _ {a b : Level} {A : Set a} {B : Set b} where module _ {a b : Level} {A : Set a} {B : Set b} where
@ -109,7 +109,7 @@ module _ ( : Level) where
re-ve = inverse-from-to-iso A B re-ve = inverse-from-to-iso A B
ve-re : (x : isIso f) (obv inv) x x ve-re : (x : isIso f) (obv inv) x x
ve-re = inverse-to-from-iso A B sA sB ve-re = inverse-to-from-iso A B sA sB
iso : isEquiv A B f isIso f iso : isEquiv A B f isIso f
iso = obv , inv , funExt re-ve , funExt ve-re iso = obv , inv , funExt re-ve , funExt ve-re
in fromIsomorphism _ _ iso in fromIsomorphism _ _ iso
@ -125,7 +125,7 @@ module _ ( : Level) where
step2 : (hA hB) (A B) step2 : (hA hB) (A B)
step2 = lem2 (λ A isSetIsProp) hA hB step2 = lem2 (λ A isSetIsProp) hA hB
univ≃ : (hA hB) (hA hB) univ≃ : (hA hB) (hA hB)
univ≃ = step2 univalence step0 univ≃ = step2 univalence step0
univalent : Univalent univalent : Univalent

View file

@ -32,7 +32,6 @@ open import Cat.Prelude
import Cat.Equivalence import Cat.Equivalence
open Cat.Equivalence public using () renaming (Isomorphism to TypeIsomorphism) open Cat.Equivalence public using () renaming (Isomorphism to TypeIsomorphism)
open Cat.Equivalence open Cat.Equivalence
renaming (_≅_ to _≈_)
hiding (preorder≅ ; Isomorphism) hiding (preorder≅ ; Isomorphism)
------------------ ------------------
@ -52,6 +51,8 @@ record RawCategory (a b : Level) : Set (lsuc (a ⊔ b)) where
identity : {A : Object} Arrow A A identity : {A : Object} Arrow A A
_<<<_ : {A B C : Object} Arrow B C Arrow A B Arrow A C _<<<_ : {A B C : Object} Arrow B C Arrow A B Arrow A C
-- infixr 8 _<<<_
-- infixl 8 _>>>_
infixl 10 _<<<_ _>>>_ infixl 10 _<<<_ _>>>_
-- | Operations on data -- | Operations on data
@ -86,8 +87,8 @@ record RawCategory (a b : Level) : Set (lsuc (a ⊔ b)) where
Isomorphism : {A B} (f : Arrow A B) Set b Isomorphism : {A B} (f : Arrow A B) Set b
Isomorphism {A} {B} f = Σ[ g Arrow B A ] IsInverseOf f g Isomorphism {A} {B} f = Σ[ g Arrow B A ] IsInverseOf f g
__ : (A B : Object) Set b __ : (A B : Object) Set b
__ A B = Σ[ f Arrow A B ] (Isomorphism f) __ A B = Σ[ f Arrow A B ] (Isomorphism f)
module _ {A B : Object} where module _ {A B : Object} where
Epimorphism : {X : Object } (f : Arrow A B) Set b Epimorphism : {X : Object } (f : Arrow A B) Set b
@ -111,29 +112,30 @@ record RawCategory (a b : Level) : Set (lsuc (a ⊔ b)) where
-- | Univalence is indexed by a raw category as well as an identity proof. -- | Univalence is indexed by a raw category as well as an identity proof.
module Univalence (isIdentity : IsIdentity identity) where module Univalence (isIdentity : IsIdentity identity) where
-- | The identity isomorphism -- | The identity isomorphism
idIso : (A : Object) A A idIso : (A : Object) A A
idIso A = identity , identity , isIdentity idIso A = identity , identity , isIdentity
-- | Extract an isomorphism from an equality -- | Extract an isomorphism from an equality
-- --
-- [HoTT §9.1.4] -- [HoTT §9.1.4]
idToIso : (A B : Object) A B A B idToIso : (A B : Object) A B A B
idToIso 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) (idToIso A B) Univalent = {A B : Object} isEquiv (A B) (A B) (idToIso A B)
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 _ _
-- 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)
Univalent≅ = {A B : Object} (A B) (A B)
private private
-- | Equivalent formulation of univalence. -- | Equivalent formulation of univalence.
Univalent[Contr] : Set _ Univalent[Contr] : Set _
Univalent[Contr] = A isContr (Σ[ X Object ] A X) Univalent[Contr] = A isContr (Σ[ X Object ] A X)
-- From: Thierry Coquand <Thierry.Coquand@cse.gu.se> -- From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
-- Date: Wed, Mar 21, 2018 at 3:12 PM -- Date: Wed, Mar 21, 2018 at 3:12 PM
@ -145,15 +147,18 @@ record RawCategory (a b : Level) : Set (lsuc (a ⊔ b)) where
univalenceFrom≃ = from[Contr] step univalenceFrom≃ = from[Contr] step
where where
module _ (f : Univalent≃) (A : Object) where module _ (f : Univalent≃) (A : Object) where
lem : Σ Object (A ≡_) Σ Object (A _) lem : Σ Object (A ≡_) Σ Object (A _)
lem = equivSig λ _ f lem = equivSig λ _ f
aux : isContr (Σ Object (A ≡_)) aux : isContr (Σ Object (A ≡_))
aux = (A , refl) , (λ y contrSingl (snd y)) aux = (A , refl) , (λ y contrSingl (snd y))
step : isContr (Σ Object (A _)) step : isContr (Σ Object (A _))
step = equivPreservesNType {n = ⟨-2⟩} lem aux step = equivPreservesNType {n = ⟨-2⟩} lem aux
univalenceFrom≅ : Univalent≅ Univalent
univalenceFrom≅ x = univalenceFrom≃ $ fromIsomorphism _ _ x
propUnivalent : isProp Univalent propUnivalent : isProp Univalent
propUnivalent a b i = propPi (λ iso propIsContr) a b i propUnivalent a b i = propPi (λ iso propIsContr) a b i
@ -263,8 +268,8 @@ module _ {a b : Level} ( : RawCategory a b) where
module _ where module _ where
private private
trans : Transitive _≅_ trans : Transitive _≊_
trans (f , f~ , f-inv) (g , g~ , g-inv) trans (f , f~ , f-inv) (g , g~ , g-inv)
= g <<< f = g <<< f
, f~ <<< g~ , f~ <<< g~
, ( begin , ( begin
@ -283,11 +288,11 @@ module _ {a b : Level} ( : RawCategory a b) where
g <<< g~ ≡⟨ snd g-inv g <<< g~ ≡⟨ snd g-inv
identity identity
) )
isPreorder : IsPreorder __ isPreorder : IsPreorder __
isPreorder = record { isEquivalence = equalityIsEquivalence ; reflexive = idToIso _ _ ; trans = trans } isPreorder = record { isEquivalence = equalityIsEquivalence ; reflexive = idToIso _ _ ; trans = trans }
preorder : Preorder _ _ _ preorder : Preorder _ _ _
preorder = record { Carrier = Object ; _≈_ = _≡_ ; __ = __ ; isPreorder = isPreorder } preorder = record { Carrier = Object ; _≈_ = _≡_ ; __ = __ ; isPreorder = isPreorder }
record PreCategory : Set (lsuc (a b)) where record PreCategory : Set (lsuc (a b)) where
field field
@ -319,7 +324,7 @@ module _ {a b : Level} ( : RawCategory a b) where
iso : TypeIsomorphism (idToIso A B) iso : TypeIsomorphism (idToIso A B)
iso = toIso _ _ univalent iso = toIso _ _ univalent
isoToId : (A B) (A B) isoToId : (A B) (A B)
isoToId = fst iso isoToId = fst iso
asTypeIso : TypeIsomorphism (idToIso A B) asTypeIso : TypeIsomorphism (idToIso A B)
@ -329,14 +334,47 @@ module _ {a b : Level} ( : RawCategory a b) where
inverse-from-to-iso' : AreInverses (idToIso A B) isoToId inverse-from-to-iso' : AreInverses (idToIso A B) isoToId
inverse-from-to-iso' = snd iso inverse-from-to-iso' = snd iso
-- lemma 9.1.9 in hott module _ {a b : Object} (f : Arrow a b) where
module _ {a' : Object} (p : a a') where
private
p~ : Arrow a' a
p~ = fst (snd (idToIso _ _ p))
D : a'' a a'' Set _
D a'' p' = coe (cong (λ x Arrow x b) p') f f <<< (fst (snd (idToIso _ _ p')))
9-1-9-left : coe (cong (λ x Arrow x b) p) f f <<< p~
9-1-9-left = pathJ D (begin
coe refl f ≡⟨ id-coe
f ≡⟨ sym rightIdentity
f <<< identity ≡⟨ cong (f <<<_) (sym subst-neutral)
f <<< _ ) a' p
module _ {b' : Object} (p : b b') where
private
p* : Arrow b b'
p* = fst (idToIso _ _ p)
D : b'' b b'' Set _
D b'' p' = coe (cong (λ x Arrow a x) p') f fst (idToIso _ _ p') <<< f
9-1-9-right : coe (cong (λ x Arrow a x) p) f p* <<< f
9-1-9-right = pathJ D (begin
coe refl f ≡⟨ id-coe
f ≡⟨ sym leftIdentity
identity <<< f ≡⟨ cong (_<<< f) (sym subst-neutral)
_ <<< f ) b' p
-- lemma 9.1.9 in hott
module _ {a a' b b' : Object} module _ {a a' b b' : Object}
(p : a a') (q : b b') (f : Arrow a b) (p : a a') (q : b b') (f : Arrow a b)
where where
private private
q* : Arrow b b' q* : Arrow b b'
q* = fst (idToIso b b' q) q* = fst (idToIso _ _ q)
p* : Arrow a a' q~ : Arrow b' b
q~ = fst (snd (idToIso _ _ q))
p* : Arrow a a'
p* = fst (idToIso _ _ p) p* = fst (idToIso _ _ p)
p~ : Arrow a' a p~ : Arrow a' a
p~ = fst (snd (idToIso _ _ p)) p~ = fst (snd (idToIso _ _ p))
@ -376,7 +414,8 @@ module _ {a b : Level} ( : RawCategory a b) where
where where
lem : p~ <<< p* identity lem : p~ <<< p* identity
lem = fst (snd (snd (idToIso _ _ p))) lem = fst (snd (snd (idToIso _ _ p)))
module _ {A B X : Object} (iso : A B) where
module _ {A B X : Object} (iso : A B) where
private private
p : A B p : A B
p = isoToId iso p = isoToId iso
@ -384,7 +423,7 @@ module _ {a b : Level} ( : RawCategory a b) where
p-dom = cong (λ x Arrow x X) p p-dom = cong (λ x Arrow x X) p
p-cod : Arrow X A Arrow X B p-cod : Arrow X A Arrow X B
p-cod = cong (λ x Arrow X x) p p-cod = cong (λ x Arrow X x) p
lem : {A B} {x : A B} idToIso A B (isoToId x) x lem : {A B} {x : A B} idToIso A B (isoToId x) x
lem {x = x} i = snd inverse-from-to-iso' i x lem {x = x} i = snd inverse-from-to-iso' i x
open Σ iso renaming (fst to ι) using () open Σ iso renaming (fst to ι) using ()
@ -459,7 +498,7 @@ module _ {a b : Level} ( : RawCategory a b) where
left = Xprop _ _ left = Xprop _ _
right : X→Y <<< Y→X identity right : X→Y <<< Y→X identity
right = Yprop _ _ right = Yprop _ _
iso : X Y iso : X Y
iso = X→Y , Y→X , left , right iso = X→Y , Y→X , left , right
p0 : X Y p0 : X Y
p0 = isoToId iso p0 = isoToId iso
@ -489,7 +528,7 @@ module _ {a b : Level} ( : RawCategory a b) where
left = Yprop _ _ left = Yprop _ _
right : X→Y <<< Y→X identity right : X→Y <<< Y→X identity
right = Xprop _ _ right = Xprop _ _
iso : X Y iso : X Y
iso = Y→X , X→Y , right , left iso = Y→X , X→Y , right , left
res : Xi Yi res : Xi Yi
res = lemSig propIsInitial _ _ (isoToId iso) res = lemSig propIsInitial _ _ (isoToId iso)
@ -500,11 +539,11 @@ module _ {a b : Level} ( : RawCategory a b) where
open import Data.Nat using (_≤_ ; z≤n ; s≤s) open import Data.Nat using (_≤_ ; z≤n ; s≤s)
setIso : x isSet (Isomorphism x) setIso : x isSet (Isomorphism x)
setIso x = ntypeCommulative ((s≤s {n = 1} z≤n)) (propIsomorphism x) setIso x = ntypeCommulative ((s≤s {n = 1} z≤n)) (propIsomorphism x)
step : isSet (A B) step : isSet (A B)
step = setSig {sA = arrowsAreSets} {sB = setIso} step = setSig {sA = arrowsAreSets} {sB = setIso}
res : isSet (A B) res : isSet (A B)
res = equivPreservesNType res = equivPreservesNType
{A = A B} {B = A B} {n = ⟨0⟩} {A = A B} {B = A B} {n = ⟨0⟩}
(Equivalence.symmetry (univalent≃ {A = A} {B})) (Equivalence.symmetry (univalent≃ {A = A} {B}))
step step
@ -636,10 +675,10 @@ module Opposite {a b : Level} where
a × b × c b × a × c a × b × c b × a × c
genericly (a , b , c) = (b , a , c) genericly (a , b , c) = (b , a , c)
shuffle : A B A .≅ B shuffle : A B A .≊ B
shuffle (f , g , inv) = g , f , inv shuffle (f , g , inv) = g , f , inv
shuffle~ : A . B A B shuffle~ : A . B A B
shuffle~ (f , g , inv) = g , f , inv 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,
@ -656,12 +695,12 @@ module Opposite {a b : Level} where
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)
ζ : A B A B ζ : A B A B
ζ = η shuffle ζ = η shuffle
-- inv : AreInverses (.idToIso A B) f -- inv : AreInverses (.idToIso A B) f
inv-ζ : AreInverses (idToIso A B) ζ inv-ζ : AreInverses (idToIso A B) ζ
-- recto-verso : .idToIso A B <<< f ≡ idFun (A . B) -- recto-verso : .idToIso A B <<< f ≡ idFun (A . B)
inv-ζ = record inv-ζ = record
{ fst = funExt (λ x begin { fst = funExt (λ x begin
(ζ idToIso A B) x ≡⟨⟩ (ζ idToIso A B) x ≡⟨⟩

View file

@ -204,11 +204,8 @@ module _ {a b : Level} ( : Category a b) where
open import Cat.Equivalence open import Cat.Equivalence
Monoidal≅Kleisli : M.Monad K.Monad Monoidal≊Kleisli : M.Monad K.Monad
Monoidal≅Kleisli = forth , back , funExt backeq , funExt fortheq Monoidal≊Kleisli = forth , back , funExt backeq , funExt fortheq
Monoidal≃Kleisli : M.Monad K.Monad
Monoidal≃Kleisli = forth , eqv
Monoidal≡Kleisli : M.Monad K.Monad Monoidal≡Kleisli : M.Monad K.Monad
Monoidal≡Kleisli = ua (forth , eqv) Monoidal≡Kleisli = isoToPath Monoidal≊Kleisli

View file

@ -123,7 +123,7 @@ module voe {a b : Level} ( : Category a b) where
-- | to talk about voevodsky's construction. -- | to talk about voevodsky's construction.
module _ (omap : Omap ) (pure : {X : Object} Arrow X (omap X)) where module _ (omap : Omap ) (pure : {X : Object} Arrow X (omap X)) where
private private
module E = AreInverses {f = (fst (MonoidalKleisli ))} {fst (snd (Monoidal≅Kleisli ))}(Monoidal≅Kleisli .snd .snd) module E = AreInverses {f = (fst (MonoidalKleisli ))} {fst (snd (Monoidal≊Kleisli ))}(Monoidal≊Kleisli .snd .snd)
Monoidal→Kleisli : M.Monad K.Monad Monoidal→Kleisli : M.Monad K.Monad
Monoidal→Kleisli = E.obverse Monoidal→Kleisli = E.obverse

View file

@ -2,7 +2,7 @@
module Cat.Category.Product where module Cat.Category.Product where
open import Cat.Prelude as P hiding (_×_ ; fst ; snd) open import Cat.Prelude as P hiding (_×_ ; fst ; snd)
open import Cat.Equivalence hiding (_≅_) open import Cat.Equivalence
open import Cat.Category open import Cat.Category
@ -176,10 +176,10 @@ module Try0 {a b : Level} { : Category a b}
open Σ x renaming (fst to xa ; snd to xb) open Σ x renaming (fst to xa ; snd to xb)
open Σ 𝕐 renaming (fst to Y ; snd to y) open Σ 𝕐 renaming (fst to Y ; snd to y)
open Σ y renaming (fst to ya ; snd to yb) open Σ y renaming (fst to ya ; snd to yb)
open import Cat.Equivalence using (composeIso) renaming (_≅_ to __) open import Cat.Equivalence using (composeIso) renaming (_≅_ to __)
step0 step0
: ((X , xa , xb) (Y , ya , yb)) : ((X , xa , xb) (Y , ya , yb))
(Σ[ p (X Y) ] (PathP (λ i .Arrow (p i) A) xa ya) × (PathP (λ i .Arrow (p i) B) xb yb)) (Σ[ p (X Y) ] (PathP (λ i .Arrow (p i) A) xa ya) × (PathP (λ i .Arrow (p i) B) xb yb))
step0 step0
= (λ p cong fst p , cong-d (fst snd) p , cong-d (snd snd) p) = (λ p cong fst p , cong-d (fst snd) p , cong-d (snd snd) p)
-- , (λ x → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i)) -- , (λ x → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
@ -190,7 +190,7 @@ module Try0 {a b : Level} { : Category a b}
-- Should follow from c being univalent -- Should follow from c being univalent
iso-id-inv : {p : X Y} p .isoToId (.idToIso X Y p) iso-id-inv : {p : X Y} p .isoToId (.idToIso X Y p)
iso-id-inv {p} = sym (λ i fst (.inverse-from-to-iso' {X} {Y}) i p) iso-id-inv {p} = sym (λ i fst (.inverse-from-to-iso' {X} {Y}) i p)
id-iso-inv : {iso : X . Y} iso .idToIso X Y (.isoToId iso) id-iso-inv : {iso : X . Y} iso .idToIso X Y (.isoToId iso)
id-iso-inv {iso} = sym (λ i snd (.inverse-from-to-iso' {X} {Y}) i iso) id-iso-inv {iso} = sym (λ i snd (.inverse-from-to-iso' {X} {Y}) i iso)
lemA : {A B : Object} {f g : Arrow A B} fst f fst g f g lemA : {A B : Object} {f g : Arrow A B} fst f fst g f g
@ -207,7 +207,7 @@ module Try0 {a b : Level} { : Category a b}
step1 step1
: (Σ[ p (X Y) ] (PathP (λ i .Arrow (p i) A) xa ya) × (PathP (λ i .Arrow (p i) B) xb yb)) : (Σ[ p (X Y) ] (PathP (λ i .Arrow (p i) A) xa ya) × (PathP (λ i .Arrow (p i) B) xb yb))
Σ (X .≅ Y) (λ iso Σ (X .≊ Y) (λ iso
let p = .isoToId iso let p = .isoToId iso
in in
( PathP (λ i .Arrow (p i) A) xa ya) ( PathP (λ i .Arrow (p i) A) xa ya)
@ -216,7 +216,7 @@ module Try0 {a b : Level} { : Category a b}
step1 step1
= symIso = symIso
(isoSigFst (isoSigFst
{A = (X . Y)} {A = (X . Y)}
{B = (X Y)} {B = (X Y)}
(.groupoidObject _ _) (.groupoidObject _ _)
{Q = \ p (PathP (λ i .Arrow (p i) A) xa ya) × (PathP (λ i .Arrow (p i) B) xb yb)} {Q = \ p (PathP (λ i .Arrow (p i) A) xa ya) × (PathP (λ i .Arrow (p i) B) xb yb)}
@ -225,13 +225,13 @@ module Try0 {a b : Level} { : Category a b}
) )
step2 step2
: Σ (X . Y) (λ iso : Σ (X . Y) (λ iso
let p = .isoToId iso let p = .isoToId iso
in in
( PathP (λ i .Arrow (p i) A) xa ya) ( PathP (λ i .Arrow (p i) A) xa ya)
× PathP (λ i .Arrow (p i) B) xb yb × PathP (λ i .Arrow (p i) B) xb yb
) )
((X , xa , xb) (Y , ya , yb)) ((X , xa , xb) (Y , ya , yb))
step2 step2
= ( λ{ (iso@(f , f~ , inv-f) , p , q) = ( λ{ (iso@(f , f~ , inv-f) , p , q)
( f , sym (.domain-twist0 iso p) , sym (.domain-twist0 iso q)) ( f , sym (.domain-twist0 iso p) , sym (.domain-twist0 iso q))
@ -242,7 +242,7 @@ module Try0 {a b : Level} { : Category a b}
) )
, (λ{ (f , f~ , inv-f , inv-f~) , (λ{ (f , f~ , inv-f , inv-f~)
let let
iso : X . Y iso : X . Y
iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~ iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~
p : X Y p : X Y
p = .isoToId iso p = .isoToId iso
@ -275,14 +275,14 @@ module Try0 {a b : Level} { : Category a b}
-- must compose to give idToIso -- must compose to give idToIso
iso iso
: ((X , xa , xb) (Y , ya , yb)) : ((X , xa , xb) (Y , ya , yb))
((X , xa , xb) (Y , ya , yb)) ((X , xa , xb) (Y , ya , yb))
iso = step0 step1 step2 iso = step0 step1 step2
where where
infixl 5 _⊙_ infixl 5 _⊙_
_⊙_ = composeIso _⊙_ = composeIso
equiv1 equiv1
: ((X , xa , xb) (Y , ya , yb)) : ((X , xa , xb) (Y , ya , yb))
((X , xa , xb) (Y , ya , yb)) ((X , xa , xb) (Y , ya , yb))
equiv1 = _ , fromIso _ _ (snd iso) equiv1 = _ , fromIso _ _ (snd iso)
univalent : Univalent univalent : Univalent

View file

@ -5,7 +5,7 @@ open import Cubical.Primitives
open import Cubical.FromStdLib renaming (-max to _⊔_) open import Cubical.FromStdLib renaming (-max to _⊔_)
open import Cubical.PathPrelude hiding (inverse) open import Cubical.PathPrelude hiding (inverse)
open import Cubical.PathPrelude using (isEquiv ; isContr ; fiber) public open import Cubical.PathPrelude using (isEquiv ; isContr ; fiber) public
open import Cubical.GradLemma open import Cubical.GradLemma hiding (isoToPath)
open import Cat.Prelude using (lemPropF ; setPi ; lemSig ; propSet ; Preorder ; equalityIsEquivalence ; propSig ; id-coe) open import Cat.Prelude using (lemPropF ; setPi ; lemSig ; propSet ; Preorder ; equalityIsEquivalence ; propSig ; id-coe)
@ -329,6 +329,9 @@ preorder≅ = record
module _ { : Level} {A B : Set } where module _ { : Level} {A B : Set } where
isoToPath : (A B) (A B)
isoToPath = ua fromIsomorphism _ _
univalence : (A B) (A B) univalence : (A B) (A B)
univalence = Equivalence.compose u' aux univalence = Equivalence.compose u' aux
where where

View file

@ -90,6 +90,7 @@ IsPreorder
IsPreorder _~_ = Relation.Binary.IsPreorder _≡_ _~_ IsPreorder _~_ = Relation.Binary.IsPreorder _≡_ _~_
module _ { : Level} {A : Set } {a : A} where module _ { : Level} {A : Set } {a : A} where
-- FIXME rename to `coe-neutral`
id-coe : coe refl a a id-coe : coe refl a a
id-coe = begin id-coe = begin
coe refl a ≡⟨⟩ coe refl a ≡⟨⟩