[WIP] Propositionality of products

This commit is contained in:
Frederik Hanghøj Iversen 2018-04-03 12:40:20 +02:00
parent 1c6d9ad2b5
commit 467c5d9c0c
2 changed files with 44 additions and 42 deletions

View file

@ -69,8 +69,14 @@ module _ {a b : Level} { : Category a b} {A B : Category.Object
module y = IsProduct y module y = IsProduct y
module _ {X : Object} (f : [ X , A ]) (g : [ X , B ]) where module _ {X : Object} (f : [ X , A ]) (g : [ X , B ]) where
module _ (f×g : Arrow X y.object) where
help : isProp ({y} ( [ y.proj₁ y ] f) P.× ( [ y.proj₂ y ] g) f×g y)
help = propPiImpl (λ _ propPi (λ _ arrowsAreSets _ _))
res = ∃-unique (x.ump f g) (y.ump f g)
prodAux : x.ump f g y.ump f g prodAux : x.ump f g y.ump f g
prodAux = {!!} prodAux = lemSig ((λ f×g propSig (propSig (arrowsAreSets _ _) λ _ arrowsAreSets _ _) (λ _ help f×g))) _ _ res
propIsProduct' : x y propIsProduct' : x y
propIsProduct' i = record { ump = λ f g prodAux f g i } propIsProduct' i = record { ump = λ f g prodAux f g i }
@ -84,42 +90,6 @@ module _ {a b : Level} { : Category a b} {A B : Category.Object
q : (λ i IsProduct A B (p i)) [ Product.isProduct x Product.isProduct y ] q : (λ i IsProduct A B (p i)) [ Product.isProduct x Product.isProduct y ]
q = lemPropF propIsProduct p q = lemPropF propIsProduct p
module _ {a b : Level} { : Category a b} {A B : Category.Object } where
open Category
private
module _ (x y : HasProducts ) where
private
module x = HasProducts x
module y = HasProducts y
module _ (A B : Object) where
module pX = Product (x.product A B)
module pY = Product (y.product A B)
objEq : pX.object pY.object
objEq = {!!}
proj₁Eq : (λ i [ objEq i , A ]) [ pX.proj₁ pY.proj₁ ]
proj₁Eq = {!!}
proj₂Eq : (λ i [ objEq i , B ]) [ pX.proj₂ pY.proj₂ ]
proj₂Eq = {!!}
rawEq : pX.raw pY.raw
RawProduct.object (rawEq i) = objEq i
RawProduct.proj₁ (rawEq i) = {!!}
RawProduct.proj₂ (rawEq i) = {!!}
isEq : (λ i IsProduct A B (rawEq i)) [ pX.isProduct pY.isProduct ]
isEq = {!!}
appEq : x.product A B y.product A B
appEq = Product≡ rawEq
productEq : x.product y.product
productEq i = λ A B appEq A B i
propHasProducts' : x y
propHasProducts' i = record { product = productEq i }
propHasProducts : isProp (HasProducts )
propHasProducts = propHasProducts'
module Try0 {a b : Level} { : Category a b} module Try0 {a b : Level} { : Category a b}
(let module = Category ) {A B : .Object} where (let module = Category ) {A B : .Object} where
@ -212,12 +182,17 @@ module Try0 {a b : Level} { : Category a b}
-- b : b0 ≡ b1 -- b : b0 ≡ b1
-- b = {!!} -- b = {!!}
open Univalence isIdentity
univalent : Univalent
univalent {A , a0 , a1} {B , b0 , b1} = {!!}
isCat : IsCategory raw isCat : IsCategory raw
isCat = record isCat = record
{ isAssociative = isAssocitaive { isAssociative = isAssocitaive
; isIdentity = isIdentity ; isIdentity = isIdentity
; arrowsAreSets = arrowsAreSets ; arrowsAreSets = arrowsAreSets
; univalent = {!!} ; univalent = univalent
} }
cat : Category _ _ cat : Category _ _
@ -296,13 +271,34 @@ module Try0 {a b : Level} { : Category a b}
t {Xx} = Xo , contractible t {Xx} = Xo , contractible
ve-re : x g (f x) x ve-re : x g (f x) x
ve-re x = Propositionality.propTerminal _ _ ve-re x = Propositionality.propTerminal _ _
re-ve : x f (g x) x re-ve : p f (g p) p
re-ve x = {!!} re-ve p = Product≡ e
where
module p = Product p
-- RawProduct does not have eta-equality.
e : Product.raw (f (g p)) Product.raw p
RawProduct.object (e i) = p.object
RawProduct.proj₁ (e i) = p.proj₁
RawProduct.proj₂ (e i) = p.proj₂
inv : AreInverses f g inv : AreInverses f g
inv = record inv = record
{ verso-recto = funExt ve-re { verso-recto = funExt ve-re
; recto-verso = funExt re-ve ; recto-verso = funExt re-ve
} }
thm : isProp (Product A B) propProduct : isProp (Product A B)
thm = equivPreservesNType {n = ⟨-1⟩} lemma Propositionality.propTerminal propProduct = equivPreservesNType {n = ⟨-1⟩} lemma Propositionality.propTerminal
module _ {a b : Level} { : Category a b} {A B : Category.Object } where
open Category
private
module _ (x y : HasProducts ) where
private
module x = HasProducts x
module y = HasProducts y
productEq : x.product y.product
productEq = funExt λ A funExt λ B Try0.propProduct _ _
propHasProducts : isProp (HasProducts )
propHasProducts x y i = record { product = productEq x y i }

View file

@ -56,6 +56,12 @@ module _ ( : Level) where
syntax ∃!-syntax (λ x B) = ∃![ x ] B syntax ∃!-syntax (λ x B) = ∃![ x ] B
module _ {a b} {A : Set a} {P : A Set b} (f g : ∃! P) where
open Σ (proj₂ f) renaming (proj₂ to u)
∃-unique : proj₁ f proj₁ g
∃-unique = u (proj₁ (proj₂ g))
module _ {a b : Level} {A : Set a} {B : A Set b} {a b : Σ A B} module _ {a b : Level} {A : Set a} {B : A Set b} {a b : Σ A B}
(proj₁≡ : (λ _ A) [ proj₁ a proj₁ b ]) (proj₁≡ : (λ _ A) [ proj₁ a proj₁ b ])
(proj₂≡ : (λ i B (proj₁≡ i)) [ proj₂ a proj₂ b ]) where (proj₂≡ : (λ i B (proj₁≡ i)) [ proj₂ a proj₂ b ]) where