Expose naturalIsProp

This commit is contained in:
Frederik Hanghøj Iversen 2018-02-23 11:12:27 +01:00
parent bc2129b8fc
commit 954a89f8d1

View file

@ -38,9 +38,6 @@ module _ {c c' d d' : Level} { : Category c c'} {𝔻 : Cat
(f : [ A , B ])
𝔻 [ θ B F.func→ f ] 𝔻 [ G.func→ f θ A ]
-- naturalIsProp : ∀ θ → isProp (Natural θ)
-- naturalIsProp θ x y = {!funExt!}
NaturalTransformation : Set (c c' d')
NaturalTransformation = Σ Transformation Natural
@ -100,59 +97,56 @@ module _ {c c' d d' : Level} { : Category c c'} {𝔻 : Cat
NatComp = _:⊕:_
private
module _ {F G : Functor 𝔻} where
module 𝔻 = Category 𝔻
module 𝔻 = Category 𝔻
transformationIsSet : isSet (Transformation F G)
transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l p l C) (λ l q l C) i j
IsSet' : { : Level} (A : Set ) Set
IsSet' A = {x y : A} (p q : (λ _ A) [ x y ]) p q
module _ {F G : Functor 𝔻} where
transformationIsSet : isSet (Transformation F G)
transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l p l C) (λ l q l C) i j
naturalIsProp : (θ : Transformation F G) isProp (Natural F G θ)
naturalIsProp θ θNat θNat' = lem
where
lem : (λ _ Natural F G θ) [ (λ f θNat f) (λ f θNat' f) ]
lem = λ i f 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i
naturalIsProp : (θ : Transformation F G) isProp (Natural F G θ)
naturalIsProp θ θNat θNat' = lem
where
lem : (λ _ Natural F G θ) [ (λ f θNat f) (λ f θNat' f) ]
lem = λ i f 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i
naturalTransformationIsSets : isSet (NaturalTransformation F G)
naturalTransformationIsSets = sigPresSet transformationIsSet
λ θ ntypeCommulative
(s≤s {n = Nat.suc Nat.zero} z≤n)
(naturalIsProp θ)
naturalTransformationIsSets : isSet (NaturalTransformation F G)
naturalTransformationIsSets = sigPresSet transformationIsSet
λ θ ntypeCommulative
(s≤s {n = Nat.suc Nat.zero} z≤n)
(naturalIsProp θ)
module _ {A B C D : Functor 𝔻} {θ' : NaturalTransformation A B}
{η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where
private
θ = proj₁ θ'
η = proj₁ η'
ζ = proj₁ ζ'
θNat = proj₂ θ'
ηNat = proj₂ η'
ζNat = proj₂ ζ'
L : NaturalTransformation A D
L = (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ'))
R : NaturalTransformation A D
R = (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
_g⊕f_ = _:⊕:_ {A} {B} {C}
_h⊕g_ = _:⊕:_ {B} {C} {D}
:assoc: : L R
:assoc: = lemSig (naturalIsProp {F = A} {D})
L R (funExt (λ x assoc))
where
open Category 𝔻
module _ {A B C D : Functor 𝔻} {θ' : NaturalTransformation A B}
{η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where
private
θ = proj₁ θ'
η = proj₁ η'
ζ = proj₁ ζ'
θNat = proj₂ θ'
ηNat = proj₂ η'
ζNat = proj₂ ζ'
L : NaturalTransformation A D
L = (_:⊕:_ {A} {C} {D} ζ' (_:⊕:_ {A} {B} {C} η' θ'))
R : NaturalTransformation A D
R = (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} ζ' η') θ')
_g⊕f_ = _:⊕:_ {A} {B} {C}
_h⊕g_ = _:⊕:_ {B} {C} {D}
:assoc: : L R
:assoc: = lemSig (naturalIsProp {F = A} {D})
L R (funExt (λ x assoc))
where
open Category 𝔻
private
module _ {A B : Functor 𝔻} {f : NaturalTransformation A B} where
private
allNatural = naturalIsProp {F = A} {B}
f' = proj₁ f
module 𝔻Data = Category 𝔻
eq-r : C (𝔻 [ f' C identityTrans A C ]) f' C
eq-r C = begin
𝔻 [ f' C identityTrans A C ] ≡⟨⟩
𝔻 [ f' C 𝔻Data.𝟙 ] ≡⟨ proj₁ (𝔻.ident {A} {B})
f' C
eq-l : C (𝔻 [ identityTrans B C f' C ]) f' C
eq-l C = proj₂ (𝔻.ident {A} {B})
allNatural = naturalIsProp {F = A} {B}
f' = proj₁ f
eq-r : C (𝔻 [ f' C identityTrans A C ]) f' C
eq-r C = begin
𝔻 [ f' C identityTrans A C ] ≡⟨⟩
𝔻 [ f' C 𝔻.𝟙 ] ≡⟨ proj₁ 𝔻.ident
f' C
eq-l : C (𝔻 [ identityTrans B C f' C ]) f' C
eq-l C = proj₂ 𝔻.ident
ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) f
ident-r = lemSig allNatural _ _ (funExt eq-r)
ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) f