Rename proj. to fst and snd
This commit is contained in:
parent
d78965d73f
commit
8276deb4aa
|
|
@ -3,7 +3,7 @@
|
|||
|
||||
module Cat.Categories.Cat where
|
||||
|
||||
open import Cat.Prelude renaming (proj₁ to fst ; proj₂ to snd)
|
||||
open import Cat.Prelude renaming (fst to fst ; snd to snd)
|
||||
|
||||
open import Cat.Category
|
||||
open import Cat.Category.Functor
|
||||
|
|
@ -83,16 +83,16 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
|
|||
object : Category ℓ ℓ'
|
||||
Category.raw object = rawProduct
|
||||
|
||||
proj₁ : Functor object ℂ
|
||||
proj₁ = record
|
||||
fstF : Functor object ℂ
|
||||
fstF = record
|
||||
{ raw = record
|
||||
{ omap = fst ; fmap = fst }
|
||||
; isFunctor = record
|
||||
{ isIdentity = refl ; isDistributive = refl }
|
||||
}
|
||||
|
||||
proj₂ : Functor object 𝔻
|
||||
proj₂ = record
|
||||
sndF : Functor object 𝔻
|
||||
sndF = record
|
||||
{ raw = record
|
||||
{ omap = snd ; fmap = snd }
|
||||
; isFunctor = record
|
||||
|
|
@ -116,19 +116,19 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
|
|||
open module x₁ = Functor x₁
|
||||
open module x₂ = Functor x₂
|
||||
|
||||
isUniqL : F[ proj₁ ∘ x ] ≡ x₁
|
||||
isUniqL : F[ fstF ∘ x ] ≡ x₁
|
||||
isUniqL = Functor≡ refl
|
||||
|
||||
isUniqR : F[ proj₂ ∘ x ] ≡ x₂
|
||||
isUniqR : F[ sndF ∘ x ] ≡ x₂
|
||||
isUniqR = Functor≡ refl
|
||||
|
||||
isUniq : F[ proj₁ ∘ x ] ≡ x₁ × F[ proj₂ ∘ x ] ≡ x₂
|
||||
isUniq : F[ fstF ∘ x ] ≡ x₁ × F[ sndF ∘ x ] ≡ x₂
|
||||
isUniq = isUniqL , isUniqR
|
||||
|
||||
isProduct : ∃![ x ] (F[ proj₁ ∘ x ] ≡ x₁ × F[ proj₂ ∘ x ] ≡ x₂)
|
||||
isProduct : ∃![ x ] (F[ fstF ∘ x ] ≡ x₁ × F[ sndF ∘ x ] ≡ x₂)
|
||||
isProduct = x , isUniq , uq
|
||||
where
|
||||
module _ {y : Functor X object} (eq : F[ proj₁ ∘ y ] ≡ x₁ × F[ proj₂ ∘ y ] ≡ x₂) where
|
||||
module _ {y : Functor X object} (eq : F[ fstF ∘ y ] ≡ x₁ × F[ sndF ∘ y ] ≡ x₂) where
|
||||
omapEq : Functor.omap x ≡ Functor.omap y
|
||||
omapEq = {!!}
|
||||
-- fmapEq : (λ i → {!{A B : ?} → Arrow A B → 𝔻 [ ? A , ? B ]!}) [ Functor.fmap x ≡ Functor.fmap y ]
|
||||
|
|
@ -148,8 +148,8 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
|
|||
|
||||
rawProduct : RawProduct Catℓ ℂ 𝔻
|
||||
RawProduct.object rawProduct = P.object
|
||||
RawProduct.proj₁ rawProduct = P.proj₁
|
||||
RawProduct.proj₂ rawProduct = P.proj₂
|
||||
RawProduct.fst rawProduct = P.fstF
|
||||
RawProduct.snd rawProduct = P.sndF
|
||||
|
||||
isProduct : IsProduct Catℓ _ _ rawProduct
|
||||
IsProduct.ump isProduct = P.isProduct
|
||||
|
|
@ -182,8 +182,8 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
|
|||
object = Fun
|
||||
|
||||
module _ {dom cod : Functor ℂ 𝔻 × ℂ.Object} where
|
||||
open Σ dom renaming (proj₁ to F ; proj₂ to A)
|
||||
open Σ cod renaming (proj₁ to G ; proj₂ to B)
|
||||
open Σ dom renaming (fst to F ; snd to A)
|
||||
open Σ cod renaming (fst to G ; snd to B)
|
||||
private
|
||||
module F = Functor F
|
||||
module G = Functor G
|
||||
|
|
@ -200,7 +200,7 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
|
|||
open CatProduct renaming (object to _⊗_) using ()
|
||||
|
||||
module _ {c : Functor ℂ 𝔻 × ℂ.Object} where
|
||||
open Σ c renaming (proj₁ to F ; proj₂ to C)
|
||||
open Σ c renaming (fst to F ; snd to C)
|
||||
|
||||
ident : fmap {c} {c} (identityNT F , ℂ.identity {A = snd c}) ≡ 𝔻.identity
|
||||
ident = begin
|
||||
|
|
@ -214,9 +214,9 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
|
|||
module F = Functor F
|
||||
|
||||
module _ {F×A G×B H×C : Functor ℂ 𝔻 × ℂ.Object} where
|
||||
open Σ F×A renaming (proj₁ to F ; proj₂ to A)
|
||||
open Σ G×B renaming (proj₁ to G ; proj₂ to B)
|
||||
open Σ H×C renaming (proj₁ to H ; proj₂ to C)
|
||||
open Σ F×A renaming (fst to F ; snd to A)
|
||||
open Σ G×B renaming (fst to G ; snd to B)
|
||||
open Σ H×C renaming (fst to H ; snd to C)
|
||||
private
|
||||
module F = Functor F
|
||||
module G = Functor G
|
||||
|
|
@ -225,14 +225,14 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
|
|||
module _
|
||||
{θ×f : NaturalTransformation F G × ℂ [ A , B ]}
|
||||
{η×g : NaturalTransformation G H × ℂ [ B , C ]} where
|
||||
open Σ θ×f renaming (proj₁ to θNT ; proj₂ to f)
|
||||
open Σ θNT renaming (proj₁ to θ ; proj₂ to θNat)
|
||||
open Σ η×g renaming (proj₁ to ηNT ; proj₂ to g)
|
||||
open Σ ηNT renaming (proj₁ to η ; proj₂ to ηNat)
|
||||
open Σ θ×f renaming (fst to θNT ; snd to f)
|
||||
open Σ θNT renaming (fst to θ ; snd to θNat)
|
||||
open Σ η×g renaming (fst to ηNT ; snd to g)
|
||||
open Σ ηNT renaming (fst to η ; snd to ηNat)
|
||||
private
|
||||
ηθNT : NaturalTransformation F H
|
||||
ηθNT = NT[_∘_] {F} {G} {H} ηNT θNT
|
||||
open Σ ηθNT renaming (proj₁ to ηθ ; proj₂ to ηθNat)
|
||||
open Σ ηθNT renaming (fst to ηθ ; snd to ηθNat)
|
||||
|
||||
isDistributive :
|
||||
𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ F.fmap ( ℂ [ g ∘ f ] ) ]
|
||||
|
|
|
|||
|
|
@ -25,21 +25,21 @@ module _ {ℓa ℓb : Level} where
|
|||
private
|
||||
module T = Functor T
|
||||
Type : (Γ : ℂ.Object) → Set ℓa
|
||||
Type Γ = proj₁ (proj₁ (T.omap Γ))
|
||||
Type Γ = fst (fst (T.omap Γ))
|
||||
|
||||
module _ {Γ : ℂ.Object} {A : Type Γ} where
|
||||
|
||||
-- module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where
|
||||
-- k : Σ (proj₁ (omap T B) → proj₁ (omap T A))
|
||||
-- k : Σ (fst (omap T B) → fst (omap T A))
|
||||
-- (λ f →
|
||||
-- {x : proj₁ (omap T B)} →
|
||||
-- proj₂ (omap T B) x → proj₂ (omap T A) (f x))
|
||||
-- {x : fst (omap T B)} →
|
||||
-- snd (omap T B) x → snd (omap T A) (f x))
|
||||
-- k = T.fmap γ
|
||||
-- k₁ : proj₁ (omap T B) → proj₁ (omap T A)
|
||||
-- k₁ = proj₁ k
|
||||
-- k₂ : ({x : proj₁ (omap T B)} →
|
||||
-- proj₂ (omap T B) x → proj₂ (omap T A) (k₁ x))
|
||||
-- k₂ = proj₂ k
|
||||
-- k₁ : fst (omap T B) → fst (omap T A)
|
||||
-- k₁ = fst k
|
||||
-- k₂ : ({x : fst (omap T B)} →
|
||||
-- snd (omap T B) x → snd (omap T A) (k₁ x))
|
||||
-- k₂ = snd k
|
||||
|
||||
record ContextComprehension : Set (ℓa ⊔ ℓb) where
|
||||
field
|
||||
|
|
|
|||
|
|
@ -8,12 +8,12 @@ open import Cat.Category
|
|||
|
||||
module _ (ℓa ℓb : Level) where
|
||||
private
|
||||
Object = Σ[ hA ∈ hSet ℓa ] (proj₁ hA → hSet ℓb)
|
||||
Object = Σ[ hA ∈ hSet ℓa ] (fst hA → hSet ℓb)
|
||||
Arr : Object → Object → Set (ℓa ⊔ ℓb)
|
||||
Arr ((A , _) , B) ((A' , _) , B') = Σ[ f ∈ (A → A') ] ({x : A} → proj₁ (B x) → proj₁ (B' (f x)))
|
||||
Arr ((A , _) , B) ((A' , _) , B') = Σ[ f ∈ (A → A') ] ({x : A} → fst (B x) → fst (B' (f x)))
|
||||
identity : {A : Object} → Arr A A
|
||||
proj₁ identity = λ x → x
|
||||
proj₂ identity = λ b → b
|
||||
fst identity = λ x → x
|
||||
snd identity = λ b → b
|
||||
_∘_ : {a b c : Object} → Arr b c → Arr a b → Arr a c
|
||||
(g , g') ∘ (f , f') = g Function.∘ f , g' Function.∘ f'
|
||||
|
||||
|
|
@ -47,11 +47,11 @@ module _ (ℓa ℓb : Level) where
|
|||
{sA = setPi λ _ → hB}
|
||||
{sB = λ f →
|
||||
let
|
||||
helpr : isSet ((a : A) → proj₁ (famA a) → proj₁ (famB (f a)))
|
||||
helpr = setPi λ a → setPi λ _ → proj₂ (famB (f a))
|
||||
helpr : isSet ((a : A) → fst (famA a) → fst (famB (f a)))
|
||||
helpr = setPi λ a → setPi λ _ → snd (famB (f a))
|
||||
-- It's almost like above, but where the first argument is
|
||||
-- implicit.
|
||||
res : isSet ({a : A} → proj₁ (famA a) → proj₁ (famB (f a)))
|
||||
res : isSet ({a : A} → fst (famA a) → fst (famB (f a)))
|
||||
res = {!!}
|
||||
in res
|
||||
}
|
||||
|
|
|
|||
|
|
@ -29,16 +29,16 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
|
|||
center : Σ[ G ∈ Object ] (F ≅ G)
|
||||
center = F , id-to-iso F F refl
|
||||
|
||||
open Σ center renaming (proj₂ to isoF)
|
||||
open Σ center renaming (snd to isoF)
|
||||
|
||||
module _ (cG : Σ[ G ∈ Object ] (F ≅ G)) where
|
||||
open Σ cG renaming (proj₁ to G ; proj₂ to isoG)
|
||||
open Σ cG renaming (fst to G ; snd to isoG)
|
||||
module G = Functor G
|
||||
open Σ isoG renaming (proj₁ to θNT ; proj₂ to invθNT)
|
||||
open Σ invθNT renaming (proj₁ to ηNT ; proj₂ to areInv)
|
||||
open Σ θNT renaming (proj₁ to θ ; proj₂ to θN)
|
||||
open Σ ηNT renaming (proj₁ to η ; proj₂ to ηN)
|
||||
open Σ areInv renaming (proj₁ to ve-re ; proj₂ to re-ve)
|
||||
open Σ isoG renaming (fst to θNT ; snd to invθNT)
|
||||
open Σ invθNT renaming (fst to ηNT ; snd to areInv)
|
||||
open Σ θNT renaming (fst to θ ; snd to θN)
|
||||
open Σ ηNT renaming (fst to η ; snd to ηN)
|
||||
open Σ areInv renaming (fst to ve-re ; snd to re-ve)
|
||||
|
||||
-- f ~ Transformation G G
|
||||
-- f : (X : ℂ.Object) → 𝔻 [ G.omap X , G.omap X ]
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
{-# OPTIONS --cubical --allow-unsolved-metas #-}
|
||||
module Cat.Categories.Rel where
|
||||
|
||||
open import Cat.Prelude renaming (proj₁ to fst ; proj₂ to snd)
|
||||
open import Cat.Prelude renaming (fst to fst ; snd to snd)
|
||||
open import Function
|
||||
|
||||
open import Cat.Category
|
||||
|
|
|
|||
|
|
@ -2,8 +2,7 @@
|
|||
{-# OPTIONS --allow-unsolved-metas --cubical --caching #-}
|
||||
module Cat.Categories.Sets where
|
||||
|
||||
open import Cat.Prelude hiding (_≃_)
|
||||
import Data.Product
|
||||
open import Cat.Prelude as P hiding (_≃_)
|
||||
|
||||
open import Function using (_∘_ ; _∘′_)
|
||||
|
||||
|
|
@ -38,8 +37,8 @@ module _ (ℓ : Level) where
|
|||
open RawCategory SetsRaw hiding (_∘_)
|
||||
|
||||
isIdentity : IsIdentity Function.id
|
||||
proj₁ isIdentity = funExt λ _ → refl
|
||||
proj₂ isIdentity = funExt λ _ → refl
|
||||
fst isIdentity = funExt λ _ → refl
|
||||
snd isIdentity = funExt λ _ → refl
|
||||
|
||||
open Univalence (λ {A} {B} {f} → isIdentity {A} {B} {f})
|
||||
|
||||
|
|
@ -48,14 +47,14 @@ module _ (ℓ : Level) where
|
|||
|
||||
isIso = Eqv.Isomorphism
|
||||
module _ {hA hB : hSet ℓ} where
|
||||
open Σ hA renaming (proj₁ to A ; proj₂ to sA)
|
||||
open Σ hB renaming (proj₁ to B ; proj₂ to sB)
|
||||
open Σ hA renaming (fst to A ; snd to sA)
|
||||
open Σ hB renaming (fst to B ; snd to sB)
|
||||
lem1 : (f : A → B) → isSet A → isSet B → isProp (isIso f)
|
||||
lem1 f sA sB = res
|
||||
where
|
||||
module _ (x y : isIso f) where
|
||||
module x = Σ x renaming (proj₁ to inverse ; proj₂ to areInverses)
|
||||
module y = Σ y renaming (proj₁ to inverse ; proj₂ to areInverses)
|
||||
module x = Σ x renaming (fst to inverse ; snd to areInverses)
|
||||
module y = Σ y renaming (fst to inverse ; snd to areInverses)
|
||||
module xA = AreInverses x.areInverses
|
||||
module yA = AreInverses y.areInverses
|
||||
-- I had a lot of difficulty using the corresponding proof where
|
||||
|
|
@ -88,24 +87,24 @@ module _ (ℓ : Level) where
|
|||
res i = 1eq i , 2eq i
|
||||
module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
|
||||
lem2 : ((x : A) → isProp (P x)) → (p q : Σ A P)
|
||||
→ (p ≡ q) ≃ (proj₁ p ≡ proj₁ q)
|
||||
→ (p ≡ q) ≃ (fst p ≡ fst q)
|
||||
lem2 pA p q = fromIsomorphism iso
|
||||
where
|
||||
f : ∀ {p q} → p ≡ q → proj₁ p ≡ proj₁ q
|
||||
f e i = proj₁ (e i)
|
||||
g : ∀ {p q} → proj₁ p ≡ proj₁ q → p ≡ q
|
||||
f : ∀ {p q} → p ≡ q → fst p ≡ fst q
|
||||
f e i = fst (e i)
|
||||
g : ∀ {p q} → fst p ≡ fst q → p ≡ q
|
||||
g {p} {q} = lemSig pA p q
|
||||
ve-re : (e : p ≡ q) → (g ∘ f) e ≡ e
|
||||
ve-re = pathJ (\ q (e : p ≡ q) → (g ∘ f) e ≡ e)
|
||||
(\ i j → p .proj₁ , propSet (pA (p .proj₁)) (p .proj₂) (p .proj₂) (λ i → (g {p} {p} ∘ f) (λ i₁ → p) i .proj₂) (λ i → p .proj₂) i j ) q
|
||||
re-ve : (e : proj₁ p ≡ proj₁ q) → (f {p} {q} ∘ g {p} {q}) e ≡ e
|
||||
(\ i j → p .fst , propSet (pA (p .fst)) (p .snd) (p .snd) (λ i → (g {p} {p} ∘ f) (λ i₁ → p) i .snd) (λ i → p .snd) i j ) q
|
||||
re-ve : (e : fst p ≡ fst q) → (f {p} {q} ∘ g {p} {q}) e ≡ e
|
||||
re-ve e = refl
|
||||
inv : AreInverses (f {p} {q}) (g {p} {q})
|
||||
inv = record
|
||||
{ verso-recto = funExt ve-re
|
||||
; recto-verso = funExt re-ve
|
||||
}
|
||||
iso : (p ≡ q) Eqv.≅ (proj₁ p ≡ proj₁ q)
|
||||
iso : (p ≡ q) Eqv.≅ (fst p ≡ fst q)
|
||||
iso = f , g , inv
|
||||
|
||||
lem3 : ∀ {ℓc} {Q : A → Set (ℓc ⊔ ℓb)}
|
||||
|
|
@ -119,37 +118,37 @@ module _ (ℓ : Level) where
|
|||
where
|
||||
k : Eqv.Isomorphism _
|
||||
k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
|
||||
open Σ k renaming (proj₁ to g')
|
||||
open Σ k renaming (fst to g')
|
||||
ve-re : (x : Σ A P) → (g ∘ f) x ≡ x
|
||||
ve-re x i = proj₁ x , eq i
|
||||
ve-re x i = fst x , eq i
|
||||
where
|
||||
eq : proj₂ ((g ∘ f) x) ≡ proj₂ x
|
||||
eq : snd ((g ∘ f) x) ≡ snd x
|
||||
eq = begin
|
||||
proj₂ ((g ∘ f) x) ≡⟨⟩
|
||||
proj₂ (g (f (a , pA))) ≡⟨⟩
|
||||
snd ((g ∘ f) x) ≡⟨⟩
|
||||
snd (g (f (a , pA))) ≡⟨⟩
|
||||
g' (_≃_.eqv (eA a) pA) ≡⟨ lem ⟩
|
||||
pA ∎
|
||||
where
|
||||
open Σ x renaming (proj₁ to a ; proj₂ to pA)
|
||||
open Σ x renaming (fst to a ; snd to pA)
|
||||
k : Eqv.Isomorphism _
|
||||
k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
|
||||
open Σ k renaming (proj₁ to g' ; proj₂ to inv)
|
||||
open Σ k renaming (fst to g' ; snd to inv)
|
||||
module A = AreInverses inv
|
||||
-- anti-funExt
|
||||
lem : (g' ∘ (_≃_.eqv (eA a))) pA ≡ pA
|
||||
lem i = A.verso-recto i pA
|
||||
re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x
|
||||
re-ve x i = proj₁ x , eq i
|
||||
re-ve x i = fst x , eq i
|
||||
where
|
||||
open Σ x renaming (proj₁ to a ; proj₂ to qA)
|
||||
open Σ x renaming (fst to a ; snd to qA)
|
||||
eq = begin
|
||||
proj₂ ((f ∘ g) x) ≡⟨⟩
|
||||
snd ((f ∘ g) x) ≡⟨⟩
|
||||
_≃_.eqv (eA a) (g' qA) ≡⟨ (λ i → A.recto-verso i qA) ⟩
|
||||
qA ∎
|
||||
where
|
||||
k : Eqv.Isomorphism _
|
||||
k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
|
||||
open Σ k renaming (proj₁ to g' ; proj₂ to inv)
|
||||
open Σ k renaming (fst to g' ; snd to inv)
|
||||
module A = AreInverses inv
|
||||
inv : AreInverses f g
|
||||
inv = record
|
||||
|
|
@ -183,8 +182,8 @@ module _ (ℓ : Level) where
|
|||
in fromIsomorphism iso
|
||||
|
||||
module _ {hA hB : Object} where
|
||||
open Σ hA renaming (proj₁ to A ; proj₂ to sA)
|
||||
open Σ hB renaming (proj₁ to B ; proj₂ to sB)
|
||||
open Σ hA renaming (fst to A ; snd to sA)
|
||||
open Σ hB renaming (fst to B ; snd to sB)
|
||||
|
||||
-- lem3 and the equivalence from lem4
|
||||
step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B)
|
||||
|
|
@ -236,7 +235,7 @@ module _ (ℓ : Level) where
|
|||
univ≃ = trivial? ⊙ step0 ⊙ step1 ⊙ step2
|
||||
|
||||
module _ (hA : Object) where
|
||||
open Σ hA renaming (proj₁ to A)
|
||||
open Σ hA renaming (fst to A)
|
||||
|
||||
eq1 : (Σ[ hB ∈ Object ] hA ≅ hB) ≡ (Σ[ hB ∈ Object ] hA ≡ hB)
|
||||
eq1 = ua (lem3 (\ hB → univ≃))
|
||||
|
|
@ -245,7 +244,7 @@ module _ (ℓ : Level) where
|
|||
univalent[Contr] = subst {P = isContr} (sym eq1) tres
|
||||
where
|
||||
module _ (y : Σ[ hB ∈ Object ] hA ≡ hB) where
|
||||
open Σ y renaming (proj₁ to hB ; proj₂ to hA≡hB)
|
||||
open Σ y renaming (fst to hB ; snd to hA≡hB)
|
||||
qres : (hA , refl) ≡ (hB , hA≡hB)
|
||||
qres = contrSingl hA≡hB
|
||||
|
||||
|
|
@ -273,8 +272,8 @@ module _ {ℓ : Level} where
|
|||
open import Cubical.Sigma
|
||||
|
||||
module _ (hA hB : Object) where
|
||||
open Σ hA renaming (proj₁ to A ; proj₂ to sA)
|
||||
open Σ hB renaming (proj₁ to B ; proj₂ to sB)
|
||||
open Σ hA renaming (fst to A ; snd to sA)
|
||||
open Σ hB renaming (fst to B ; snd to sB)
|
||||
|
||||
private
|
||||
productObject : Object
|
||||
|
|
@ -285,30 +284,30 @@ module _ {ℓ : Level} where
|
|||
_&&&_ x = f x , g x
|
||||
|
||||
module _ (hX : Object) where
|
||||
open Σ hX renaming (proj₁ to X)
|
||||
open Σ hX renaming (fst to X)
|
||||
module _ (f : X → A ) (g : X → B) where
|
||||
ump : proj₁ Function.∘′ (f &&& g) ≡ f × proj₂ Function.∘′ (f &&& g) ≡ g
|
||||
proj₁ ump = refl
|
||||
proj₂ ump = refl
|
||||
ump : fst Function.∘′ (f &&& g) ≡ f × snd Function.∘′ (f &&& g) ≡ g
|
||||
fst ump = refl
|
||||
snd ump = refl
|
||||
|
||||
rawProduct : RawProduct 𝓢 hA hB
|
||||
RawProduct.object rawProduct = productObject
|
||||
RawProduct.proj₁ rawProduct = Data.Product.proj₁
|
||||
RawProduct.proj₂ rawProduct = Data.Product.proj₂
|
||||
RawProduct.fst rawProduct = fst
|
||||
RawProduct.snd rawProduct = snd
|
||||
|
||||
isProduct : IsProduct 𝓢 _ _ rawProduct
|
||||
IsProduct.ump isProduct {X = hX} f g
|
||||
= f &&& g , ump hX f g , λ eq → funExt (umpUniq eq)
|
||||
where
|
||||
open Σ hX renaming (proj₁ to X) using ()
|
||||
module _ {y : X → A × B} (eq : proj₁ Function.∘′ y ≡ f × proj₂ Function.∘′ y ≡ g) (x : X) where
|
||||
p1 : proj₁ ((f &&& g) x) ≡ proj₁ (y x)
|
||||
open Σ hX renaming (fst to X) using ()
|
||||
module _ {y : X → A × B} (eq : fst Function.∘′ y ≡ f × snd Function.∘′ y ≡ g) (x : X) where
|
||||
p1 : fst ((f &&& g) x) ≡ fst (y x)
|
||||
p1 = begin
|
||||
proj₁ ((f &&& g) x) ≡⟨⟩
|
||||
f x ≡⟨ (λ i → sym (proj₁ eq) i x) ⟩
|
||||
proj₁ (y x) ∎
|
||||
p2 : proj₂ ((f &&& g) x) ≡ proj₂ (y x)
|
||||
p2 = λ i → sym (proj₂ eq) i x
|
||||
fst ((f &&& g) x) ≡⟨⟩
|
||||
f x ≡⟨ (λ i → sym (fst eq) i x) ⟩
|
||||
fst (y x) ∎
|
||||
p2 : snd ((f &&& g) x) ≡ snd (y x)
|
||||
p2 = λ i → sym (snd eq) i x
|
||||
umpUniq : (f &&& g) x ≡ y x
|
||||
umpUniq i = p1 i , p2 i
|
||||
|
||||
|
|
|
|||
|
|
@ -29,12 +29,8 @@
|
|||
module Cat.Category where
|
||||
|
||||
open import Cat.Prelude
|
||||
renaming
|
||||
( proj₁ to fst
|
||||
; proj₂ to snd
|
||||
)
|
||||
|
||||
import Function
|
||||
import Function
|
||||
|
||||
------------------
|
||||
-- * Categories --
|
||||
|
|
@ -136,10 +132,10 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
|
|||
-- It may be that we need something weaker than this, in that there
|
||||
-- may be some other lemmas available to us.
|
||||
-- For instance, `need0` should be available to us when we prove `need1`.
|
||||
(need0 : (s : Σ Object (A ≅_)) → (open Σ s renaming (proj₁ to Y) using ()) → A ≡ Y)
|
||||
(need0 : (s : Σ Object (A ≅_)) → (open Σ s renaming (fst to Y) using ()) → A ≡ Y)
|
||||
(need2 : (iso : A ≅ A)
|
||||
→ (open Σ iso renaming (proj₁ to f ; proj₂ to iso-f))
|
||||
→ (open Σ iso-f renaming (proj₁ to f~ ; proj₂ to areInv))
|
||||
→ (open Σ iso renaming (fst to f ; snd to iso-f))
|
||||
→ (open Σ iso-f renaming (fst to f~ ; snd to areInv))
|
||||
→ (identity , identity) ≡ (f , f~)
|
||||
) where
|
||||
|
||||
|
|
@ -147,7 +143,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
|
|||
c = A , idIso A
|
||||
|
||||
module _ (y : Σ Object (A ≅_)) where
|
||||
open Σ y renaming (proj₁ to Y ; proj₂ to isoY)
|
||||
open Σ y renaming (fst to Y ; snd to isoY)
|
||||
q : A ≡ Y
|
||||
q = need0 y
|
||||
|
||||
|
|
@ -163,8 +159,8 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
|
|||
d : D A refl
|
||||
d A≅Y i = a0 i , a1 i , a2 i
|
||||
where
|
||||
open Σ A≅Y renaming (proj₁ to f ; proj₂ to iso-f)
|
||||
open Σ iso-f renaming (proj₁ to f~ ; proj₂ to areInv)
|
||||
open Σ A≅Y renaming (fst to f ; snd to iso-f)
|
||||
open Σ iso-f renaming (fst to f~ ; snd to areInv)
|
||||
aaa : (identity , identity) ≡ (f , f~)
|
||||
aaa = need2 A≅Y
|
||||
a0 : identity ≡ f
|
||||
|
|
@ -309,8 +305,8 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
|
|||
propIsTerminal T x y i {X} = res X i
|
||||
where
|
||||
module _ (X : Object) where
|
||||
open Σ (x {X}) renaming (proj₁ to fx ; proj₂ to cx)
|
||||
open Σ (y {X}) renaming (proj₁ to fy ; proj₂ to cy)
|
||||
open Σ (x {X}) renaming (fst to fx ; snd to cx)
|
||||
open Σ (y {X}) renaming (fst to fy ; snd to cy)
|
||||
fp : fx ≡ fy
|
||||
fp = cx fy
|
||||
prop : (x : Arrow X T) → isProp (∀ f → x ≡ f)
|
||||
|
|
@ -328,10 +324,10 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
|
|||
propTerminal : isProp Terminal
|
||||
propTerminal Xt Yt = res
|
||||
where
|
||||
open Σ Xt renaming (proj₁ to X ; proj₂ to Xit)
|
||||
open Σ Yt renaming (proj₁ to Y ; proj₂ to Yit)
|
||||
open Σ (Xit {Y}) renaming (proj₁ to Y→X) using ()
|
||||
open Σ (Yit {X}) renaming (proj₁ to X→Y) using ()
|
||||
open Σ Xt renaming (fst to X ; snd to Xit)
|
||||
open Σ Yt renaming (fst to Y ; snd to Yit)
|
||||
open Σ (Xit {Y}) renaming (fst to Y→X) using ()
|
||||
open Σ (Yit {X}) renaming (fst to X→Y) using ()
|
||||
open import Cat.Equivalence hiding (_≅_)
|
||||
-- Need to show `left` and `right`, what we know is that the arrows are
|
||||
-- unique. Well, I know that if I compose these two arrows they must give
|
||||
|
|
@ -361,8 +357,8 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
|
|||
propIsInitial I x y i {X} = res X i
|
||||
where
|
||||
module _ (X : Object) where
|
||||
open Σ (x {X}) renaming (proj₁ to fx ; proj₂ to cx)
|
||||
open Σ (y {X}) renaming (proj₁ to fy ; proj₂ to cy)
|
||||
open Σ (x {X}) renaming (fst to fx ; snd to cx)
|
||||
open Σ (y {X}) renaming (fst to fy ; snd to cy)
|
||||
fp : fx ≡ fy
|
||||
fp = cx fy
|
||||
prop : (x : Arrow I X) → isProp (∀ f → x ≡ f)
|
||||
|
|
@ -375,10 +371,10 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
|
|||
propInitial : isProp Initial
|
||||
propInitial Xi Yi = res
|
||||
where
|
||||
open Σ Xi renaming (proj₁ to X ; proj₂ to Xii)
|
||||
open Σ Yi renaming (proj₁ to Y ; proj₂ to Yii)
|
||||
open Σ (Xii {Y}) renaming (proj₁ to Y→X) using ()
|
||||
open Σ (Yii {X}) renaming (proj₁ to X→Y) using ()
|
||||
open Σ Xi renaming (fst to X ; snd to Xii)
|
||||
open Σ Yi renaming (fst to Y ; snd to Yii)
|
||||
open Σ (Xii {Y}) renaming (fst to Y→X) using ()
|
||||
open Σ (Yii {X}) renaming (fst to X→Y) using ()
|
||||
open import Cat.Equivalence hiding (_≅_)
|
||||
-- Need to show `left` and `right`, what we know is that the arrows are
|
||||
-- unique. Well, I know that if I compose these two arrows they must give
|
||||
|
|
@ -508,7 +504,7 @@ module Opposite {ℓa ℓb : Level} where
|
|||
open import Cat.Equivalence as Equivalence hiding (_≅_)
|
||||
k : Equivalence.Isomorphism (ℂ.id-to-iso A B)
|
||||
k = Equiv≃.toIso _ _ ℂ.univalent
|
||||
open Σ k renaming (proj₁ to f ; proj₂ to inv)
|
||||
open Σ k renaming (fst to f ; snd to inv)
|
||||
open AreInverses inv
|
||||
|
||||
_⊙_ = Function._∘_
|
||||
|
|
@ -531,12 +527,12 @@ module Opposite {ℓa ℓb : Level} where
|
|||
where
|
||||
l = id-to-iso A B p
|
||||
r = flopDem (ℂ.id-to-iso A B p)
|
||||
open Σ l renaming (proj₁ to l-obv ; proj₂ to l-areInv)
|
||||
open Σ l-areInv renaming (proj₁ to l-invs ; proj₂ to l-iso)
|
||||
open Σ l-iso renaming (proj₁ to l-l ; proj₂ to l-r)
|
||||
open Σ r renaming (proj₁ to r-obv ; proj₂ to r-areInv)
|
||||
open Σ r-areInv renaming (proj₁ to r-invs ; proj₂ to r-iso)
|
||||
open Σ r-iso renaming (proj₁ to r-l ; proj₂ to r-r)
|
||||
open Σ l renaming (fst to l-obv ; snd to l-areInv)
|
||||
open Σ l-areInv renaming (fst to l-invs ; snd to l-iso)
|
||||
open Σ l-iso renaming (fst to l-l ; snd to l-r)
|
||||
open Σ r renaming (fst to r-obv ; snd to r-areInv)
|
||||
open Σ r-areInv renaming (fst to r-invs ; snd to r-iso)
|
||||
open Σ r-iso renaming (fst to r-l ; snd to r-r)
|
||||
l-obv≡r-obv : l-obv ≡ r-obv
|
||||
l-obv≡r-obv = refl
|
||||
l-invs≡r-invs : l-invs ≡ r-invs
|
||||
|
|
|
|||
|
|
@ -30,7 +30,7 @@ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}}
|
|||
{{isExponential}} : IsExponential obj eval
|
||||
|
||||
transpose : (A : Object) → ℂ [ A × B , C ] → ℂ [ A , obj ]
|
||||
transpose A f = proj₁ (isExponential A f)
|
||||
transpose A f = fst (isExponential A f)
|
||||
|
||||
record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where
|
||||
open Category ℂ
|
||||
|
|
|
|||
|
|
@ -52,7 +52,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
private
|
||||
module MI = M.IsMonad m
|
||||
forthIsMonad : K.IsMonad (forthRaw raw)
|
||||
K.IsMonad.isIdentity forthIsMonad = proj₂ MI.isInverse
|
||||
K.IsMonad.isIdentity forthIsMonad = snd MI.isInverse
|
||||
K.IsMonad.isNatural forthIsMonad = MI.isNatural
|
||||
K.IsMonad.isDistributive forthIsMonad = MI.isDistributive
|
||||
|
||||
|
|
@ -83,11 +83,11 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
where
|
||||
inv-l = begin
|
||||
joinT X ∘ pureT (R.omap X) ≡⟨⟩
|
||||
join ∘ pure ≡⟨ proj₁ isInverse ⟩
|
||||
join ∘ pure ≡⟨ fst isInverse ⟩
|
||||
identity ∎
|
||||
inv-r = begin
|
||||
joinT X ∘ R.fmap (pureT X) ≡⟨⟩
|
||||
join ∘ fmap pure ≡⟨ proj₂ isInverse ⟩
|
||||
join ∘ fmap pure ≡⟨ snd isInverse ⟩
|
||||
identity ∎
|
||||
|
||||
back : K.Monad → M.Monad
|
||||
|
|
@ -160,7 +160,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
Rfmap (f >>> pureT B) >>> joinT B ≡⟨⟩
|
||||
Rfmap (f >>> pureT B) >>> joinT B ≡⟨ cong (λ φ → φ >>> joinT B) R.isDistributive ⟩
|
||||
Rfmap f >>> Rfmap (pureT B) >>> joinT B ≡⟨ ℂ.isAssociative ⟩
|
||||
joinT B ∘ Rfmap (pureT B) ∘ Rfmap f ≡⟨ cong (λ φ → φ ∘ Rfmap f) (proj₂ isInverse) ⟩
|
||||
joinT B ∘ Rfmap (pureT B) ∘ Rfmap f ≡⟨ cong (λ φ → φ ∘ Rfmap f) (snd isInverse) ⟩
|
||||
identity ∘ Rfmap f ≡⟨ ℂ.leftIdentity ⟩
|
||||
Rfmap f ∎
|
||||
)
|
||||
|
|
|
|||
|
|
@ -165,12 +165,12 @@ record IsMonad (raw : RawMonad) : Set ℓ where
|
|||
R.fmap f ∘ join ∎
|
||||
|
||||
pureNT : NaturalTransformation R⁰ R
|
||||
proj₁ pureNT = pureT
|
||||
proj₂ pureNT = pureN
|
||||
fst pureNT = pureT
|
||||
snd pureNT = pureN
|
||||
|
||||
joinNT : NaturalTransformation R² R
|
||||
proj₁ joinNT = joinT
|
||||
proj₂ joinNT = joinN
|
||||
fst joinNT = joinT
|
||||
snd joinNT = joinN
|
||||
|
||||
isNaturalForeign : IsNaturalForeign
|
||||
isNaturalForeign = begin
|
||||
|
|
|
|||
|
|
@ -29,14 +29,14 @@ record RawMonad : Set ℓ where
|
|||
-- Note that `pureT` and `joinT` differs from their definition in the
|
||||
-- kleisli formulation only by having an explicit parameter.
|
||||
pureT : Transformation Functors.identity R
|
||||
pureT = proj₁ pureNT
|
||||
pureT = fst pureNT
|
||||
pureN : Natural Functors.identity R pureT
|
||||
pureN = proj₂ pureNT
|
||||
pureN = snd pureNT
|
||||
|
||||
joinT : Transformation F[ R ∘ R ] R
|
||||
joinT = proj₁ joinNT
|
||||
joinT = fst joinNT
|
||||
joinN : Natural F[ R ∘ R ] R joinT
|
||||
joinN = proj₂ joinNT
|
||||
joinN = snd joinNT
|
||||
|
||||
Romap = Functor.omap R
|
||||
Rfmap = Functor.fmap R
|
||||
|
|
@ -71,7 +71,7 @@ record IsMonad (raw : RawMonad) : Set ℓ where
|
|||
joinT Y ∘ R.fmap f ∘ pureT X ≡⟨ sym ℂ.isAssociative ⟩
|
||||
joinT Y ∘ (R.fmap f ∘ pureT X) ≡⟨ cong (λ φ → joinT Y ∘ φ) (sym (pureN f)) ⟩
|
||||
joinT Y ∘ (pureT (R.omap Y) ∘ f) ≡⟨ ℂ.isAssociative ⟩
|
||||
joinT Y ∘ pureT (R.omap Y) ∘ f ≡⟨ cong (λ φ → φ ∘ f) (proj₁ isInverse) ⟩
|
||||
joinT Y ∘ pureT (R.omap Y) ∘ f ≡⟨ cong (λ φ → φ ∘ f) (fst isInverse) ⟩
|
||||
identity ∘ f ≡⟨ ℂ.leftIdentity ⟩
|
||||
f ∎
|
||||
|
||||
|
|
@ -129,8 +129,8 @@ private
|
|||
where
|
||||
xX = x {X}
|
||||
yX = y {X}
|
||||
e1 = Category.arrowsAreSets ℂ _ _ (proj₁ xX) (proj₁ yX)
|
||||
e2 = Category.arrowsAreSets ℂ _ _ (proj₂ xX) (proj₂ yX)
|
||||
e1 = Category.arrowsAreSets ℂ _ _ (fst xX) (fst yX)
|
||||
e2 = Category.arrowsAreSets ℂ _ _ (snd xX) (snd yX)
|
||||
|
||||
open IsMonad
|
||||
propIsMonad : (raw : _) → isProp (IsMonad raw)
|
||||
|
|
|
|||
|
|
@ -124,7 +124,7 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
-- | to talk about voevodsky's construction.
|
||||
module _ (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where
|
||||
private
|
||||
module E = AreInverses (Monoidal≅Kleisli ℂ .proj₂ .proj₂)
|
||||
module E = AreInverses (Monoidal≅Kleisli ℂ .snd .snd)
|
||||
|
||||
Monoidal→Kleisli : M.Monad → K.Monad
|
||||
Monoidal→Kleisli = E.obverse
|
||||
|
|
|
|||
|
|
@ -58,7 +58,7 @@ module _ (F G : Functor ℂ 𝔻) where
|
|||
propIsNatural θ x y i {A} {B} f = 𝔻.arrowsAreSets _ _ (x f) (y f) i
|
||||
|
||||
NaturalTransformation≡ : {α β : NaturalTransformation}
|
||||
→ (eq₁ : α .proj₁ ≡ β .proj₁)
|
||||
→ (eq₁ : α .fst ≡ β .fst)
|
||||
→ α ≡ β
|
||||
NaturalTransformation≡ eq = lemSig propIsNatural _ _ eq
|
||||
|
||||
|
|
@ -88,8 +88,8 @@ module _ {F G H : Functor ℂ 𝔻} where
|
|||
T[ θ ∘ η ] C = 𝔻 [ θ C ∘ η C ]
|
||||
|
||||
NT[_∘_] : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H
|
||||
proj₁ NT[ (θ , _) ∘ (η , _) ] = T[ θ ∘ η ]
|
||||
proj₂ NT[ (θ , θNat) ∘ (η , ηNat) ] {A} {B} f = begin
|
||||
fst NT[ (θ , _) ∘ (η , _) ] = T[ θ ∘ η ]
|
||||
snd NT[ (θ , θNat) ∘ (η , ηNat) ] {A} {B} f = begin
|
||||
𝔻 [ T[ θ ∘ η ] B ∘ F.fmap f ] ≡⟨⟩
|
||||
𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.fmap f ] ≡⟨ sym 𝔻.isAssociative ⟩
|
||||
𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.fmap f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
|
||||
|
|
|
|||
|
|
@ -2,8 +2,8 @@
|
|||
module Cat.Category.Product where
|
||||
|
||||
open import Cubical.NType.Properties
|
||||
open import Cat.Prelude hiding (_×_ ; proj₁ ; proj₂)
|
||||
import Data.Product as P
|
||||
open import Cat.Prelude as P hiding (_×_ ; fst ; snd)
|
||||
-- module P = Cat.Prelude
|
||||
|
||||
open import Cat.Category
|
||||
|
||||
|
|
@ -16,8 +16,8 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
no-eta-equality
|
||||
field
|
||||
object : Object
|
||||
proj₁ : ℂ [ object , A ]
|
||||
proj₂ : ℂ [ object , B ]
|
||||
fst : ℂ [ object , A ]
|
||||
snd : ℂ [ object , B ]
|
||||
|
||||
-- FIXME Not sure this is actually a proposition - so this name is
|
||||
-- misleading.
|
||||
|
|
@ -25,12 +25,12 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
open RawProduct raw public
|
||||
field
|
||||
ump : ∀ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ])
|
||||
→ ∃![ f×g ] (ℂ [ proj₁ ∘ f×g ] ≡ f P.× ℂ [ proj₂ ∘ f×g ] ≡ g)
|
||||
→ ∃![ f×g ] (ℂ [ fst ∘ f×g ] ≡ f P.× ℂ [ snd ∘ f×g ] ≡ g)
|
||||
|
||||
-- | Arrow product
|
||||
_P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
|
||||
→ ℂ [ X , object ]
|
||||
_P[_×_] π₁ π₂ = P.proj₁ (ump π₁ π₂)
|
||||
_P[_×_] π₁ π₂ = P.fst (ump π₁ π₂)
|
||||
|
||||
record Product : Set (ℓa ⊔ ℓb) where
|
||||
field
|
||||
|
|
@ -51,8 +51,8 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
-- The product mentioned in awodey in Def 6.1 is not the regular product of
|
||||
-- arrows. It's a "parallel" product
|
||||
module _ {A A' B B' : Object} where
|
||||
open Product
|
||||
open Product (product A B) hiding (_P[_×_]) renaming (proj₁ to fst ; proj₂ to snd)
|
||||
open Product using (_P[_×_])
|
||||
open Product (product A B) hiding (_P[_×_]) renaming (fst to fst ; snd to snd)
|
||||
_|×|_ : ℂ [ A , A' ] → ℂ [ B , B' ] → ℂ [ A × B , A' × B' ]
|
||||
f |×| g = product A' B'
|
||||
P[ ℂ [ f ∘ fst ]
|
||||
|
|
@ -70,7 +70,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object
|
|||
|
||||
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 : isProp (∀{y} → (ℂ [ y.fst ∘ y ] ≡ f) P.× (ℂ [ y.snd ∘ y ] ≡ g) → f×g ≡ y)
|
||||
help = propPiImpl (λ _ → propPi (λ _ → arrowsAreSets _ _))
|
||||
|
||||
res = ∃-unique (x.ump f g) (y.ump f g)
|
||||
|
|
@ -93,7 +93,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object
|
|||
module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
||||
(let module ℂ = Category ℂ) {A B : ℂ.Object} where
|
||||
|
||||
open import Data.Product
|
||||
open P
|
||||
|
||||
module _ where
|
||||
raw : RawCategory _ _
|
||||
|
|
@ -130,12 +130,12 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
|
||||
isAssocitaive : IsAssociative
|
||||
isAssocitaive {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 {proj₂ l} {proj₂ r} i
|
||||
= 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 : proj₁ l ≡ proj₁ r
|
||||
s0 : fst l ≡ fst r
|
||||
s0 = ℂ.isAssociative {f = f} {g} {h}
|
||||
|
||||
|
||||
|
|
@ -143,15 +143,15 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = leftIdentity , rightIdentity
|
||||
where
|
||||
leftIdentity : identity ∘ (f , f0 , f1) ≡ (f , f0 , f1)
|
||||
leftIdentity i = l i , lemPropF propEqs l {proj₂ L} {proj₂ R} i
|
||||
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 : proj₁ L ≡ proj₁ R
|
||||
l : fst L ≡ fst R
|
||||
l = ℂ.leftIdentity
|
||||
rightIdentity : (f , f0 , f1) ∘ identity ≡ (f , f0 , f1)
|
||||
rightIdentity i = l i , lemPropF propEqs l {proj₂ L} {proj₂ R} i
|
||||
rightIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i
|
||||
where
|
||||
L = (f , f0 , f1) ∘ identity
|
||||
R : Arrow AA BB
|
||||
|
|
@ -165,29 +165,50 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
|
||||
open Univalence isIdentity
|
||||
|
||||
module _ (A : Object) where
|
||||
c : Σ Object (A ≅_)
|
||||
c = A , {!!}
|
||||
univalent[Contr] : isContr (Σ Object (A ≅_))
|
||||
univalent[Contr] = {!!} , {!!}
|
||||
-- module _ (X : Object) where
|
||||
-- center : Σ Object (X ≅_)
|
||||
-- center = X , idIso X
|
||||
|
||||
-- module _ (y : Σ Object (X ≅_)) where
|
||||
-- open Σ y renaming (fst to Y ; snd to X≅Y)
|
||||
|
||||
-- contractible : (X , idIso X) ≡ (Y , X≅Y)
|
||||
-- contractible = {!!}
|
||||
|
||||
-- univalent[Contr] : isContr (Σ Object (X ≅_))
|
||||
-- univalent[Contr] = center , contractible
|
||||
-- module _ (y : Σ Object (X ≡_)) where
|
||||
-- open Σ y renaming (fst to Y ; snd to p)
|
||||
-- a0 : X ≡ Y
|
||||
-- a0 = {!!}
|
||||
-- a1 : PathP (λ i → X ≡ a0 i) refl p
|
||||
-- a1 = {!!}
|
||||
-- where
|
||||
-- P : (Z : Object) → X ≡ Z → Set _
|
||||
-- P Z p = PathP (λ i → X ≡ Z)
|
||||
|
||||
-- alt' : (X , refl) ≡ y
|
||||
-- alt' i = a0 i , a1 i
|
||||
-- alt : isContr (Σ Object (X ≡_))
|
||||
-- alt = (X , refl) , alt'
|
||||
|
||||
univalent' : Univalent[Contr]
|
||||
univalent' = univalence-lemma p q
|
||||
where
|
||||
module _ {𝕏 : Object} where
|
||||
open Σ 𝕏 renaming (proj₁ to X ; proj₂ to x0x1)
|
||||
open Σ x0x1 renaming (proj₁ to x0 ; proj₂ to x1)
|
||||
open Σ 𝕏 renaming (fst to X ; snd to x0x1)
|
||||
open Σ x0x1 renaming (fst to x0 ; snd to x1)
|
||||
-- x0 : X → A in ℂ
|
||||
-- x1 : X → B in ℂ
|
||||
module _ (𝕐-isoY : Σ Object (𝕏 ≅_)) where
|
||||
open Σ 𝕐-isoY renaming (proj₁ to 𝕐 ; proj₂ to isoY)
|
||||
open Σ 𝕐 renaming (proj₁ to Y ; proj₂ to y0y1)
|
||||
open Σ y0y1 renaming (proj₁ to y0 ; proj₂ to y1)
|
||||
open Σ isoY renaming (proj₁ to 𝓯 ; proj₂ to iso-𝓯)
|
||||
open Σ iso-𝓯 renaming (proj₁ to 𝓯~ ; proj₂ to inv-𝓯)
|
||||
open Σ 𝓯 renaming (proj₁ to f ; proj₂ to inv-f)
|
||||
open Σ 𝓯~ renaming (proj₁ to f~ ; proj₂ to inv-f~)
|
||||
open Σ inv-𝓯 renaming (proj₁ to left ; proj₂ to right)
|
||||
open Σ 𝕐-isoY renaming (fst to 𝕐 ; snd to isoY)
|
||||
open Σ 𝕐 renaming (fst to Y ; snd to y0y1)
|
||||
open Σ y0y1 renaming (fst to y0 ; snd to y1)
|
||||
open Σ isoY renaming (fst to 𝓯 ; snd to iso-𝓯)
|
||||
open Σ iso-𝓯 renaming (fst to 𝓯~ ; snd to inv-𝓯)
|
||||
open Σ 𝓯 renaming (fst to f ; snd to inv-f)
|
||||
open Σ 𝓯~ renaming (fst to f~ ; snd to inv-f~)
|
||||
open Σ inv-𝓯 renaming (fst to left ; snd to right)
|
||||
-- y0 : Y → A in ℂ
|
||||
-- y1 : Y → B in ℂ
|
||||
-- f : X → Y in ℂ
|
||||
|
|
@ -199,24 +220,24 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
= f
|
||||
, f~
|
||||
, ( begin
|
||||
ℂ [ f~ ∘ f ] ≡⟨ (λ i → proj₁ (left i)) ⟩
|
||||
ℂ [ f~ ∘ f ] ≡⟨ (λ i → fst (left i)) ⟩
|
||||
ℂ.identity ∎
|
||||
)
|
||||
, ( begin
|
||||
ℂ [ f ∘ f~ ] ≡⟨ (λ i → proj₁ (right i)) ⟩
|
||||
ℂ [ f ∘ f~ ] ≡⟨ (λ i → fst (right i)) ⟩
|
||||
ℂ.identity ∎
|
||||
)
|
||||
p0 : X ≡ Y
|
||||
p0 = ℂ.iso-to-id isoℂ
|
||||
-- I note `left2` and right2` here as a reminder.
|
||||
left2 : PathP
|
||||
(λ i → ℂ [ x0 ∘ proj₁ (left i) ] ≡ x0 × ℂ [ x1 ∘ proj₁ (left i) ] ≡ x1)
|
||||
(proj₂ (𝓯~ ∘ 𝓯)) (proj₂ identity)
|
||||
left2 i = proj₂ (left i)
|
||||
(λ i → ℂ [ x0 ∘ fst (left i) ] ≡ x0 × ℂ [ x1 ∘ fst (left i) ] ≡ x1)
|
||||
(snd (𝓯~ ∘ 𝓯)) (snd identity)
|
||||
left2 i = snd (left i)
|
||||
right2 : PathP
|
||||
(λ i → ℂ [ y0 ∘ proj₁ (right i) ] ≡ y0 × ℂ [ y1 ∘ proj₁ (right i) ] ≡ y1)
|
||||
(proj₂ (𝓯 ∘ 𝓯~)) (proj₂ identity)
|
||||
right2 i = proj₂ (right i)
|
||||
(λ i → ℂ [ y0 ∘ fst (right i) ] ≡ y0 × ℂ [ y1 ∘ fst (right i) ] ≡ y1)
|
||||
(snd (𝓯 ∘ 𝓯~)) (snd identity)
|
||||
right2 i = snd (right i)
|
||||
-- My idea:
|
||||
--
|
||||
-- x0, x1 and y0 and y1 are product arrows as in the diagram
|
||||
|
|
@ -245,23 +266,23 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
p : (X , x0x1) ≡ (Y , y0y1)
|
||||
p i = p0 i , {!!}
|
||||
module _ (iso : 𝕏 ≅ 𝕏) where
|
||||
open Σ iso renaming (proj₁ to 𝓯 ; proj₂ to inv-𝓯)
|
||||
open Σ inv-𝓯 renaming (proj₁ to 𝓯~) using ()
|
||||
open Σ 𝓯 renaming (proj₁ to f ; proj₂ to inv-f)
|
||||
open Σ 𝓯~ renaming (proj₁ to f~ ; proj₂ to inv-f~)
|
||||
open Σ iso renaming (fst to 𝓯 ; snd to inv-𝓯)
|
||||
open Σ inv-𝓯 renaming (fst to 𝓯~) using ()
|
||||
open Σ 𝓯 renaming (fst to f ; snd to inv-f)
|
||||
open Σ 𝓯~ renaming (fst to f~ ; snd to inv-f~)
|
||||
q0' : ℂ.identity ≡ f
|
||||
q0' i = {!!}
|
||||
prop : ∀ x → isProp (ℂ [ x0 ∘ x ] ≡ x0 × ℂ [ x1 ∘ x ] ≡ x1)
|
||||
prop x = propSig
|
||||
( ℂ.arrowsAreSets (ℂ [ x0 ∘ x ]) x0)
|
||||
(λ _ → ℂ.arrowsAreSets (ℂ [ x1 ∘ x ]) x1)
|
||||
q0'' : PathP (λ i → ℂ [ x0 ∘ q0' i ] ≡ x0 × ℂ [ x1 ∘ q0' i ] ≡ x1) (proj₂ identity) inv-f
|
||||
q0'' : PathP (λ i → ℂ [ x0 ∘ q0' i ] ≡ x0 × ℂ [ x1 ∘ q0' i ] ≡ x1) (snd identity) inv-f
|
||||
q0'' = lemPropF prop q0'
|
||||
q0 : identity ≡ 𝓯
|
||||
q0 i = q0' i , q0'' i
|
||||
q1' : ℂ.identity ≡ f~
|
||||
q1' = {!!}
|
||||
q1'' : PathP (λ i → (ℂ [ x0 ∘ q1' i ]) ≡ x0 × (ℂ [ x1 ∘ q1' i ]) ≡ x1) (proj₂ identity) inv-f~
|
||||
q1'' : PathP (λ i → (ℂ [ x0 ∘ q1' i ]) ≡ x0 × (ℂ [ x1 ∘ q1' i ]) ≡ x1) (snd identity) inv-f~
|
||||
q1'' = lemPropF prop q1'
|
||||
q1 : identity ≡ 𝓯~
|
||||
q1 i = q1' i , {!!}
|
||||
|
|
@ -275,11 +296,11 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
open import Cubical.Univalence
|
||||
module _ (c : (X , x) ≅ (Y , y)) where
|
||||
-- module _ (c : _ ≅ _) where
|
||||
open Σ c renaming (proj₁ to f_c ; proj₂ to inv_c)
|
||||
open Σ inv_c renaming (proj₁ to g_c ; proj₂ to ainv_c)
|
||||
open Σ ainv_c renaming (proj₁ to left ; proj₂ to right)
|
||||
open Σ c renaming (fst to f_c ; snd to inv_c)
|
||||
open Σ inv_c renaming (fst to g_c ; snd to ainv_c)
|
||||
open Σ ainv_c renaming (fst to left ; snd to right)
|
||||
c0 : X ℂ.≅ Y
|
||||
c0 = proj₁ f_c , proj₁ g_c , (λ i → proj₁ (left i)) , (λ i → proj₁ (right i))
|
||||
c0 = fst f_c , fst g_c , (λ i → fst (left i)) , (λ i → fst (right i))
|
||||
f0 : X ≡ Y
|
||||
f0 = ℂ.iso-to-id c0
|
||||
module _ {A : ℂ.Object} (α : ℂ.Arrow X A) where
|
||||
|
|
@ -296,7 +317,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
prp : isSet (ℂ.Object × ℂ.Arrow Y A × ℂ.Arrow Y B)
|
||||
prp = setSig {sA = {!!}} {(λ _ → setSig {sA = ℂ.arrowsAreSets} {λ _ → ℂ.arrowsAreSets})}
|
||||
ve-re : (p : (X , x) ≡ (Y , y)) → f (id-to-iso _ _ p) ≡ p
|
||||
-- ve-re p i j = {!ℂ.arrowsAreSets!} , ℂ.arrowsAreSets _ _ (let k = proj₁ (proj₂ (p i)) in {!!}) {!!} {!!} {!!} , {!!}
|
||||
-- ve-re p i j = {!ℂ.arrowsAreSets!} , ℂ.arrowsAreSets _ _ (let k = fst (snd (p i)) in {!!}) {!!} {!!} {!!} , {!!}
|
||||
ve-re p = let k = prp {!!} {!!} {!!} {!p!} in {!!}
|
||||
re-ve : (iso : (X , x) ≅ (Y , y)) → id-to-iso _ _ (f iso) ≡ iso
|
||||
re-ve = {!!}
|
||||
|
|
@ -332,17 +353,17 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
rawP : RawProduct ℂ A B
|
||||
rawP = record
|
||||
{ object = X
|
||||
; proj₁ = x0
|
||||
; proj₂ = x1
|
||||
; fst = x0
|
||||
; snd = x1
|
||||
}
|
||||
-- open RawProduct rawP renaming (proj₁ to x0 ; proj₂ to x1)
|
||||
-- open RawProduct rawP renaming (fst to x0 ; snd to x1)
|
||||
module _ {Y : ℂ.Object} (p0 : ℂ [ Y , A ]) (p1 : ℂ [ Y , B ]) where
|
||||
uy : isContr (Arrow (Y , p0 , p1) (X , x0 , x1))
|
||||
uy = uniq {Y , p0 , p1}
|
||||
open Σ uy renaming (proj₁ to Y→X ; proj₂ to contractible)
|
||||
open Σ Y→X renaming (proj₁ to p0×p1 ; proj₂ to cond)
|
||||
open Σ uy renaming (fst to Y→X ; snd to contractible)
|
||||
open Σ Y→X renaming (fst to p0×p1 ; snd to cond)
|
||||
ump : ∃![ f×g ] (ℂ [ x0 ∘ f×g ] ≡ p0 P.× ℂ [ x1 ∘ f×g ] ≡ p1)
|
||||
ump = p0×p1 , cond , λ {y} x → let k = contractible (y , x) in λ i → proj₁ (k i)
|
||||
ump = p0×p1 , cond , λ {y} x → let k = contractible (y , x) in λ i → fst (k i)
|
||||
isP : IsProduct ℂ A B rawP
|
||||
isP = record { ump = ump }
|
||||
p : Product ℂ A B
|
||||
|
|
@ -356,31 +377,31 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
module p = Product p
|
||||
module isp = IsProduct p.isProduct
|
||||
o : Object
|
||||
o = p.object , p.proj₁ , p.proj₂
|
||||
o = p.object , p.fst , p.snd
|
||||
module _ {Xx : Object} where
|
||||
open Σ Xx renaming (proj₁ to X ; proj₂ to x)
|
||||
open Σ Xx renaming (fst to X ; snd to x)
|
||||
ℂXo : ℂ [ X , isp.object ]
|
||||
ℂXo = isp._P[_×_] (proj₁ x) (proj₂ x)
|
||||
ump = p.ump (proj₁ x) (proj₂ x)
|
||||
Xoo = proj₁ (proj₂ ump)
|
||||
ℂXo = isp._P[_×_] (fst x) (snd x)
|
||||
ump = p.ump (fst x) (snd x)
|
||||
Xoo = fst (snd ump)
|
||||
Xo : Arrow Xx o
|
||||
Xo = ℂXo , Xoo
|
||||
contractible : ∀ y → Xo ≡ y
|
||||
contractible (y , yy) = res
|
||||
where
|
||||
k : ℂXo ≡ y
|
||||
k = proj₂ (proj₂ ump) (yy)
|
||||
k = snd (snd ump) (yy)
|
||||
prp : ∀ a → isProp
|
||||
( (ℂ [ p.proj₁ ∘ a ] ≡ proj₁ x)
|
||||
× (ℂ [ p.proj₂ ∘ a ] ≡ proj₂ x)
|
||||
( (ℂ [ p.fst ∘ a ] ≡ fst x)
|
||||
× (ℂ [ p.snd ∘ a ] ≡ snd x)
|
||||
)
|
||||
prp ab ac ad i
|
||||
= ℂ.arrowsAreSets _ _ (proj₁ ac) (proj₁ ad) i
|
||||
, ℂ.arrowsAreSets _ _ (proj₂ ac) (proj₂ ad) i
|
||||
= ℂ.arrowsAreSets _ _ (fst ac) (fst ad) i
|
||||
, ℂ.arrowsAreSets _ _ (snd ac) (snd ad) i
|
||||
h :
|
||||
( λ i
|
||||
→ ℂ [ p.proj₁ ∘ k i ] ≡ proj₁ x
|
||||
× ℂ [ p.proj₂ ∘ k i ] ≡ proj₂ x
|
||||
→ ℂ [ p.fst ∘ k i ] ≡ fst x
|
||||
× ℂ [ p.snd ∘ k i ] ≡ snd x
|
||||
) [ Xoo ≡ yy ]
|
||||
h = lemPropF prp k
|
||||
res : (ℂXo , Xoo) ≡ (y , yy)
|
||||
|
|
@ -396,8 +417,8 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
-- 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₂
|
||||
RawProduct.fst (e i) = p.fst
|
||||
RawProduct.snd (e i) = p.snd
|
||||
inv : AreInverses f g
|
||||
inv = record
|
||||
{ verso-recto = funExt ve-re
|
||||
|
|
|
|||
|
|
@ -3,10 +3,11 @@ module Cat.Prelude where
|
|||
|
||||
open import Agda.Primitive public
|
||||
-- FIXME Use:
|
||||
-- open import Agda.Builtin.Sigma public
|
||||
open import Agda.Builtin.Sigma public
|
||||
-- Rather than
|
||||
open import Data.Product public
|
||||
renaming (∃! to ∃!≈)
|
||||
using (_×_ ; Σ-syntax ; swap)
|
||||
|
||||
-- TODO Import Data.Function under appropriate names.
|
||||
|
||||
|
|
@ -46,7 +47,7 @@ module _ (ℓ : Level) where
|
|||
-- * Utilities --
|
||||
-----------------
|
||||
|
||||
-- | Unique existensials.
|
||||
-- | Unique existentials.
|
||||
∃! : ∀ {a b} {A : Set a}
|
||||
→ (A → Set b) → Set (a ⊔ b)
|
||||
∃! = ∃!≈ _≡_
|
||||
|
|
@ -57,15 +58,15 @@ module _ (ℓ : Level) where
|
|||
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)
|
||||
open Σ (snd f) renaming (snd to u)
|
||||
|
||||
∃-unique : proj₁ f ≡ proj₁ g
|
||||
∃-unique = u (proj₁ (proj₂ g))
|
||||
∃-unique : fst f ≡ fst g
|
||||
∃-unique = u (fst (snd g))
|
||||
|
||||
module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B}
|
||||
(proj₁≡ : (λ _ → A) [ proj₁ a ≡ proj₁ b ])
|
||||
(proj₂≡ : (λ i → B (proj₁≡ i)) [ proj₂ a ≡ proj₂ b ]) where
|
||||
(fst≡ : (λ _ → A) [ fst a ≡ fst b ])
|
||||
(snd≡ : (λ i → B (fst≡ i)) [ snd a ≡ snd b ]) where
|
||||
|
||||
Σ≡ : a ≡ b
|
||||
proj₁ (Σ≡ i) = proj₁≡ i
|
||||
proj₂ (Σ≡ i) = proj₂≡ i
|
||||
fst (Σ≡ i) = fst≡ i
|
||||
snd (Σ≡ i) = snd≡ i
|
||||
|
|
|
|||
Loading…
Reference in a new issue