Almost prove that arrows are sets in the cateogry of families

This commit is contained in:
Frederik Hanghøj Iversen 2018-02-23 13:59:35 +01:00
parent a321a9c8b2
commit 5796b791b8

View file

@ -40,12 +40,29 @@ module _ (a b : Level) where
isIdentity : IsIdentity λ { {A} 𝟙 {A} } isIdentity : IsIdentity λ { {A} 𝟙 {A} }
isIdentity = (Σ≡ refl refl) , Σ≡ refl refl isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
open import Cubical.NType.Properties
open import Cubical.Sigma
instance instance
isCategory : IsCategory RawFam isCategory : IsCategory RawFam
isCategory = record isCategory = record
{ isAssociative = λ {A} {B} {C} {D} {f} {g} {h} isAssociative {A} {B} {C} {D} {f} {g} {h} { isAssociative = λ {A} {B} {C} {D} {f} {g} {h} isAssociative {A} {B} {C} {D} {f} {g} {h}
; isIdentity = λ {A} {B} {f} isIdentity {A} {B} {f = f} ; isIdentity = λ {A} {B} {f} isIdentity {A} {B} {f = f}
; arrowsAreSets = {!!} ; arrowsAreSets = λ {
{((A , hA) , famA)}
{((B , hB) , famB)}
setSig
{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))
-- It's almost like above, but where the first argument is
-- implicit.
res : isSet ({a : A} proj₁ (famA a) proj₁ (famB (f a)))
res = {!!}
in res
}
}
; univalent = {!!} ; univalent = {!!}
} }