Some stuff about CwF's

This commit is contained in:
Frederik Hanghøj Iversen 2018-01-22 14:44:50 +01:00
parent fd03049c92
commit dd3415a69d

View file

@ -7,14 +7,62 @@ open import Data.Product
open import Data.Sum
open import Data.Unit
open import Data.Empty
open import Data.Product
open import Cat.Category
open import Cat.Functor
-- See chapter 1 for a discussion on how presheaf categories are CwF's.
-- See section 6.8 in Huber's thesis for details on how to implement the
-- categorical version of CTT
module CwF { ' : Level} ( : Category ') where
open Category
open Functor
open import Function
open import Cubical
module _ {a b : Level} where
private
Obj = Σ[ A Set a ] (A Set b)
Arr : Obj Obj Set (a b)
Arr (A , B) (A' , B') = Σ[ f (A A') ] ({x : A} B x B' (f x))
one : {o : Obj} Arr o o
proj₁ one = λ x x
proj₂ one = λ b b
_:⊕:_ : {a b c : Obj} Arr b c Arr a b Arr a c
(g , g') :⊕: (f , f') = g f , g' f'
module _ {A B C D : Obj} {f : Arr A B} {g : Arr B C} {h : Arr C D} where
:assoc: : (_:⊕:_ {A} {C} {D} h (_:⊕:_ {A} {B} {C} g f)) (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} h g) f)
:assoc: = {!!}
module _ {A B : Obj} {f : Arr A B} where
:ident: : (_:⊕:_ {A} {A} {B} f one) f × (_:⊕:_ {A} {B} {B} one f) f
:ident: = {!!}
instance
:isCategory: : IsCategory Obj Arr one (λ {a b c} _:⊕:_ {a} {b} {c})
:isCategory: = record
{ assoc = λ {A} {B} {C} {D} {f} {g} {h} :assoc: {A} {B} {C} {D} {f} {g} {h}
; ident = {!!}
}
Fam : Category (lsuc (a b)) (a b)
Fam = record
{ Object = Obj
; Arrow = Arr
; 𝟙 = one
; _⊕_ = λ {a b c} _:⊕:_ {a} {b} {c}
}
Contexts = .Object
Substitutions = .Arrow
record CwF : Set {!a ⊔ b!} where
field
Terms : Functor (Opposite ) Fam
module _ { ' : Level} (Ns : Set ) where
-- Ns is the "namespace"
o = (lsuc lzero )
@ -49,5 +97,5 @@ module _ { ' : Level} (Ns : Set ) where
; Arrow = Mor
; 𝟙 = {!!}
; _⊕_ = {!!}
; isCategory = ?
; isCategory = {!!}
}