Merge remote-tracking branch 'Saizan/dev' into dev

This commit is contained in:
Frederik Hanghøj Iversen 2018-03-29 13:36:09 +02:00
commit af25db7e31
2 changed files with 120 additions and 100 deletions

View file

@ -253,6 +253,10 @@ record IsCategory {a b : Level} ( : RawCategory a b) : Set (lsuc
res : (fx , cx) (fy , cy) res : (fx , cx) (fy , cy)
res i = fp i , cp i res i = fp i , cp i
-- this needs the univalence of the category
propTerminal : isProp Terminal
propTerminal = {!!}
-- Merely the dual of the above statement. -- Merely the dual of the above statement.
propIsInitial : I isProp (IsInitial I) propIsInitial : I isProp (IsInitial I)
propIsInitial I x y i {X} = res X i propIsInitial I x y i {X} = res X i
@ -269,6 +273,9 @@ record IsCategory {a b : Level} ( : RawCategory a b) : Set (lsuc
res : (fx , cx) (fy , cy) res : (fx , cx) (fy , cy)
res i = fp i , cp i res i = fp i , cp i
propInitial : isProp Initial
propInitial = {!!}
-- | Propositionality of being a category -- | Propositionality of being a category
module _ {a b : Level} ( : RawCategory a b) where module _ {a b : Level} ( : RawCategory a b) where
open RawCategory open RawCategory

View file

@ -1,6 +1,7 @@
{-# OPTIONS --allow-unsolved-metas --cubical #-} {-# OPTIONS --allow-unsolved-metas --cubical #-}
module Cat.Category.Product where module Cat.Category.Product where
open import Cubical.NType.Properties
open import Cat.Prelude hiding (_×_ ; proj₁ ; proj₂) open import Cat.Prelude hiding (_×_ ; proj₁ ; proj₂)
import Data.Product as P import Data.Product as P
@ -128,108 +129,120 @@ module Try0 {a b : Level} { : Category a b}
raw : RawCategory _ _ raw : RawCategory _ _
raw = record raw = record
{ Object = Σ[ X .Object ] .Arrow X A × .Arrow X B { Object = Σ[ X .Object ] .Arrow X A × .Arrow X B
; Arrow = λ{ (A , _) (B , _) .Arrow A B} ; Arrow = λ{ (X , xa , xb) (Y , ya , yb) Σ[ xy .Arrow X Y ] ( [ ya xy ] xa) × ( [ yb xy ] xb) }
; 𝟙 = λ{ {A , _} .𝟙 {A}} ; 𝟙 = λ{ {A , _} .𝟙 {A} , {!!}}
; _∘_ = ._∘_ ; _∘_ = \ { (f , p) (g , q) ._∘_ f g , {!!} }
}
open RawCategory raw
open Univalence .isIdentity
open import Cat.Equivalence hiding (_≅_)
k : {A B : .Object} isEquiv (A B) (A .≅ B) (.id-to-iso A B)
k = .univalent
module _ {X' Y' : Σ[ X .Object ] ( [ X , A ] × [ X , B ])} where
open Σ X' renaming (proj₁ to X) using ()
open Σ (proj₂ X') renaming (proj₁ to Xxa ; proj₂ to Xxb)
open Σ Y' renaming (proj₁ to Y) using ()
open Σ (proj₂ Y') renaming (proj₁ to Yxa ; proj₂ to Yxb)
module _ (p : X Y) where
D : y X y Set _
D y q = b (λ i [ q i , A ]) [ Xxa b ]
-- Not sure this is actually provable - but if it were it might involve
-- something like the ump of the product -- in which case perhaps the
-- objects of the category I'm constructing should not merely be the
-- data-part of the product but also the laws.
-- d : D X refl
d : b (λ i [ X , A ]) [ Xxa b ]
d b = {!!}
kk : D Y p
kk = pathJ D d Y p
a : (λ i [ p i , A ]) [ Xxa Yxa ]
a = kk Yxa
b : (λ i [ p i , B ]) [ Xxb Yxb ]
b = {!!}
f : X' Y'
f i = p i , a i , b i
module _ (p : X' Y') where
g : X Y
g i = proj₁ (p i)
step0 : (X' Y') (X Y)
step0 = Equiv≃.fromIsomorphism _ _ (g , f , record { verso-recto = {!refl!} ; recto-verso = refl})
step1 : (X Y) X .≅ Y
step1 = .univalent≃
-- Just a reminder
step1-5 : (X' Y') (X .≅ Y)
step1-5 = refl
step2 : (X' Y') (X .≅ Y)
step2 = Equivalence.compose step0 step1
univalent : isEquiv (X' Y') (X .≅ Y) (id-to-iso X' Y')
univalent = proj₂ step2
isCategory : IsCategory raw
isCategory = record
{ isAssociative = .isAssociative
; isIdentity = .isIdentity
; arrowsAreSets = .arrowsAreSets
; univalent = univalent
}
category : Category _ _
category = record
{ raw = raw
; isCategory = isCategory
}
open Category category hiding (IsTerminal ; Object)
-- Essential turns `p : Product A B` into a triple
productObject : Object
productObject = Product.object p , Product.proj₁ p , Product.proj₂ p
productObjectIsTerminal : IsTerminal productObject
productObjectIsTerminal = {!!}
proppp : isProp (IsTerminal productObject)
proppp = Propositionality.propIsTerminal productObject
module Try1 {a b : Level} (A B : Set) where
open import Data.Product
raw : RawCategory _ _
raw = record
{ Object = Σ[ X Set ] (X A) × (X B)
; Arrow = λ{ (X0 , f0 , g0) (X1 , f1 , g1) X0 X1}
; 𝟙 = λ x x
; _∘_ = λ x x₁ x₂ x (x₁ x₂)
} }
open RawCategory raw open RawCategory raw
isCategory : IsCategory raw cat : IsCategory raw
isCategory = record cat = {!!}
{ isAssociative = refl
; isIdentity = refl , refl
; arrowsAreSets = {!!}
; univalent = {!!}
}
t : IsTerminal ((A × B) , proj₁ , proj₂) module cat = IsCategory cat
t = {!!}
lemma : Terminal Product A B
lemma = {!!}
thm : isProp (Product A B)
thm = equivPreservesNType {n = ⟨-1⟩} lemma cat.Propositionality.propTerminal
-- open Univalence .isIdentity
-- open import Cat.Equivalence hiding (_≅_)
-- k : {A B : .Object} → isEquiv (A ≡ B) (A .≅ B) (.id-to-iso A B)
-- k = .univalent
-- module _ {X' Y' : Σ[ X ∈ .Object ] ( [ X , A ] × [ X , B ])} where
-- open Σ X' renaming (proj₁ to X) using ()
-- open Σ (proj₂ X') renaming (proj₁ to Xxa ; proj₂ to Xxb)
-- open Σ Y' renaming (proj₁ to Y) using ()
-- open Σ (proj₂ Y') renaming (proj₁ to Yxa ; proj₂ to Yxb)
-- module _ (p : X ≡ Y) where
-- D : ∀ y → X ≡ y → Set _
-- D y q = ∀ b → (λ i → [ q i , A ]) [ Xxa ≡ b ]
-- -- Not sure this is actually provable - but if it were it might involve
-- -- something like the ump of the product -- in which case perhaps the
-- -- objects of the category I'm constructing should not merely be the
-- -- data-part of the product but also the laws.
-- -- d : D X refl
-- d : ∀ b → (λ i → [ X , A ]) [ Xxa ≡ b ]
-- d b = {!!}
-- kk : D Y p
-- kk = pathJ D d Y p
-- a : (λ i → [ p i , A ]) [ Xxa ≡ Yxa ]
-- a = kk Yxa
-- b : (λ i → [ p i , B ]) [ Xxb ≡ Yxb ]
-- b = {!!}
-- f : X' ≡ Y'
-- f i = p i , a i , b i
-- module _ (p : X' ≡ Y') where
-- g : X ≡ Y
-- g i = proj₁ (p i)
-- step0 : (X' ≡ Y') ≃ (X ≡ Y)
-- step0 = Equiv≃.fromIsomorphism _ _ (g , f , record { verso-recto = {!refl!} ; recto-verso = refl})
-- step1 : (X ≡ Y) ≃ X .≅ Y
-- step1 = .univalent≃
-- -- Just a reminder
-- step1-5 : (X' ≅ Y') ≡ (X .≅ Y)
-- step1-5 = refl
-- step2 : (X' ≡ Y') ≃ (X .≅ Y)
-- step2 = Equivalence.compose step0 step1
-- univalent : isEquiv (X' ≡ Y') (X .≅ Y) (id-to-iso X' Y')
-- univalent = proj₂ step2
-- isCategory : IsCategory raw
-- isCategory = record
-- { isAssociative = .isAssociative
-- ; isIdentity = .isIdentity
-- ; arrowsAreSets = .arrowsAreSets
-- ; univalent = univalent
-- }
-- category : Category _ _
-- category = record
-- { raw = raw
-- ; isCategory = isCategory
-- }
-- open Category category hiding (IsTerminal ; Object)
-- -- Essential turns `p : Product A B` into a triple
-- productObject : Object
-- productObject = Product.object p , Product.proj₁ p , Product.proj₂ p
-- productObjectIsTerminal : IsTerminal productObject
-- productObjectIsTerminal = {!!}
-- proppp : isProp (IsTerminal productObject)
-- proppp = Propositionality.propIsTerminal productObject
-- module Try1 {a b : Level} (A B : Set) where
-- open import Data.Product
-- raw : RawCategory _ _
-- raw = record
-- { Object = Σ[ X ∈ Set ] (X → A) × (X → B)
-- ; Arrow = λ{ (X0 , f0 , g0) (X1 , f1 , g1) → X0 → X1}
-- ; 𝟙 = λ x → x
-- ; _∘_ = λ x x₁ x₂ → x (x₁ x₂)
-- }
-- open RawCategory raw
-- isCategory : IsCategory raw
-- isCategory = record
-- { isAssociative = refl
-- ; isIdentity = refl , refl
-- ; arrowsAreSets = {!!}
-- ; univalent = {!!}
-- }
-- t : IsTerminal ((A × B) , proj₁ , proj₂)
-- t = {!!}