This commit is contained in:
Frederik Hanghøj Iversen 2018-04-26 10:20:57 +02:00
parent 9a8b09e15f
commit 45eafe683f
3 changed files with 13 additions and 53 deletions

View file

@ -453,8 +453,8 @@ module _ {a b : Level} ( : RawCategory a b) where
-- This can probably also just be obtained from the above my taking the -- This can probably also just be obtained from the above my taking the
-- symmetric isomorphism. -- symmetric isomorphism.
domain-twist0 : f g <<< ι domain-twist-sym : f g <<< ι
domain-twist0 = begin domain-twist-sym = begin
f ≡⟨ sym rightIdentity f ≡⟨ sym rightIdentity
f <<< identity ≡⟨ cong (f <<<_) (sym (fst inv)) f <<< identity ≡⟨ cong (f <<<_) (sym (fst inv))
f <<< (ι~ <<< ι) ≡⟨ isAssociative f <<< (ι~ <<< ι) ≡⟨ isAssociative

View file

@ -125,41 +125,19 @@ module Try0 {a b : Level} { : Category a b}
(xy : .Arrow X Y) isProp ( [ ya xy ] xa × [ yb xy ] xb) (xy : .Arrow X Y) isProp ( [ ya xy ] xa × [ yb xy ] xb)
propEqs xs = propSig (.arrowsAreSets _ _) (\ _ .arrowsAreSets _ _) propEqs xs = propSig (.arrowsAreSets _ _) (\ _ .arrowsAreSets _ _)
arrowEq : {X Y : Object} {f g : Arrow X Y} fst f fst g f g
arrowEq {X} {Y} {f} {g} p = λ i p i , lemPropF propEqs p {snd f} {snd g} i
private private
isAssociative : IsAssociative isAssociative : IsAssociative
isAssociative {A'@(A , a0 , a1)} {B , _} {C , c0 , c1} {D'@(D , d0 , d1)} {ff@(f , f0 , f1)} {gg@(g , g0 , g1)} {hh@(h , h0 , h1)} i isAssociative {f = f , f0 , f1} {g , g0 , g1} {h , h0 , h1} = arrowEq .isAssociative
= s0 i , lemPropF propEqs s0 {P.snd l} {P.snd r} i
where
l = hh <<< (gg <<< ff)
r = hh <<< gg <<< ff
-- s0 : h .<<< (g .<<< f) ≡ h .<<< g .<<< f
s0 : fst l fst r
s0 = .isAssociative {f = f} {g} {h}
isIdentity : IsIdentity identity isIdentity : IsIdentity identity
isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = leftIdentity , rightIdentity isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = arrowEq .leftIdentity , arrowEq .rightIdentity
where
leftIdentity : identity <<< (f , f0 , f1) (f , f0 , f1)
leftIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i
where
L = identity <<< (f , f0 , f1)
R : Arrow AA BB
R = f , f0 , f1
l : fst L fst R
l = .leftIdentity
rightIdentity : (f , f0 , f1) <<< identity (f , f0 , f1)
rightIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i
where
L = (f , f0 , f1) <<< identity
R : Arrow AA BB
R = (f , f0 , f1)
l : [ f .identity ] f
l = .rightIdentity
arrowsAreSets : ArrowsAreSets arrowsAreSets : ArrowsAreSets
arrowsAreSets {X , x0 , x1} {Y , y0 , y1} arrowsAreSets {X , x0 , x1} {Y , y0 , y1}
= sigPresNType {n = ⟨0⟩} .arrowsAreSets λ a propSet (propEqs _) = sigPresSet .arrowsAreSets λ a propSet (propEqs _)
isPreCat : IsPreCategory raw isPreCat : IsPreCategory raw
IsPreCategory.isAssociative isPreCat = isAssociative IsPreCategory.isAssociative isPreCat = isAssociative
@ -184,24 +162,6 @@ module Try0 {a b : Level} { : Category a b}
, funExt (λ{ p refl}) , funExt (λ{ p refl})
, funExt (λ{ (p , q , r) refl}) , funExt (λ{ (p , q , r) refl})
-- Should follow from c being univalent
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)
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)
lemA : {A B : Object} {f g : Arrow A B} fst f fst g f g
lemA {A} {B} {f = f} {g} p i = p i , h i
where
h : PathP (λ i
( [ fst (snd B) p i ]) fst (snd A) ×
( [ snd (snd B) p i ]) snd (snd A)
) (snd f) (snd g)
h = lemPropF (λ a propSig
(.arrowsAreSets ( [ fst (snd B) a ]) (fst (snd A)))
λ _ .arrowsAreSets ( [ snd (snd B) a ]) (snd (snd A)))
p
step1 step1
: (Σ[ p (X Y) ] (PathP (λ i .Arrow (p i) 𝓐) xa ya) × (PathP (λ i .Arrow (p i) 𝓑) xb yb)) : (Σ[ p (X Y) ] (PathP (λ i .Arrow (p i) 𝓐) xa ya) × (PathP (λ i .Arrow (p i) 𝓑) xb yb))
Σ (X .≊ Y) (λ iso Σ (X .≊ Y) (λ iso
@ -231,10 +191,10 @@ module Try0 {a b : Level} { : Category a b}
((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-twist-sym iso p) , sym (.domain-twist-sym iso q))
, ( f~ , sym (.domain-twist iso p) , sym (.domain-twist iso q)) , ( f~ , sym (.domain-twist iso p) , sym (.domain-twist iso q))
, lemA (fst inv-f) , arrowEq (fst inv-f)
, lemA (snd inv-f) , arrowEq (snd inv-f)
} }
) )
, (λ{ (f , f~ , inv-f , inv-f~) , (λ{ (f , f~ , inv-f , inv-f~)

View file

@ -50,7 +50,7 @@ module _ {a b c} {A : Set a} {B : Set b} (sB : isSet B) {Q : B
Σ-fst-map : Σ A (\ a Q (f a)) Σ B Q Σ-fst-map : Σ A (\ a Q (f a)) Σ B Q
Σ-fst-map (x , q) = f x , q Σ-fst-map (x , q) = f x , q
isoSigFst : Isomorphism f Σ A (\ a Q (f a)) (Σ B Q) isoSigFst : Isomorphism f Σ A (Q f) Σ B Q
isoSigFst (g , g-f , f-g) = Σ-fst-map isoSigFst (g , g-f , f-g) = Σ-fst-map
, (\ { (b , q) g b , transp (\ i Q (f-g (~ i) b)) q }) , (\ { (b , q) g b , transp (\ i Q (f-g (~ i) b)) q })
, funExt (\ { (a , q) Cat.Prelude.Σ≡ (\ i g-f i a) , funExt (\ { (a , q) Cat.Prelude.Σ≡ (\ i g-f i a)