fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Category.Product complete step2

Browse source
This commit is contained in:
Andrea Vezzosi 2018-04-13 14:35:54 +02:00
parent 6023a49da6
commit 5afa835787
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Cat/Category/Product.agda
View file

@ -125,10 +125,11 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
private private
open RawCategory raw open RawCategory raw
propEqs : ∀ {X' : Object}{Y' : Object} (let X , xa , xb = X') (let Y , ya , yb = Y') propEqs : ∀ {X' : Object}{Y' : Object} (let X , xa , xb = X') (let Y , ya , yb = Y')
→ (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 _ _)
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 {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
= s0 i , lemPropF propEqs s0 {P.snd l} {P.snd r} i = s0 i , lemPropF propEqs s0 {P.snd l} {P.snd r} i
@ -259,8 +260,8 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
{ fst = funExt (λ x → lemSig { fst = funExt (λ x → lemSig
(λ x → propSig prop0 (λ _ → prop1)) (λ x → propSig prop0 (λ _ → prop1))
_ _ _ _
(Σ≡ {!!} (ℂ.propIsomorphism _ _ _))) (Σ≡ refl (ℂ.propIsomorphism _ _ _)))
; snd = funExt (λ{ (f , _) → lemSig propIsomorphism _ _ {!refl!}}) ; snd = funExt (λ{ (f , _) → lemSig propIsomorphism _ _ (Σ≡ refl (propEqs _ _ _))})
} }
where where
prop0 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) A) xa ya) prop0 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) A) xa ya)