Re: [HoTT] A unifying cartesian cubical type theory

["Licata, Dan" <dlicata@wesleyan.edu>]

This is very cool!  It's great to know that we can do without the
diagonal cofibrations if we weaken the notion of fibration.

Here's a reformulation of this Kan operation that I find intriguing: 
in the internal language, I think Evan and Anders' definition is equivalent to saying that

    A : I → Set has Kan composition iff
      Π r:I, the map (λ f → f r) : (Π (x : I) → A x) → (A r)
             is an equivalence
    where equivalence is defined to be hfiber contractible,
    and contractible is defined to be
    "any partial element extends to a total one" (i.e. "trivial fibration")

In contrast, the stricter notion, where com^r->r is strictly the identity is 

    A : I → Set has Kan composition means 
      Π r:I, b : A(r), the strict fiber
             (i.e. SFiber (f : A → B) b = Σ a:A. f(a) =strictly b)
             of the map (λ f → f r) : (Π (x : I) → A x) → (A r)
             is contractible

Here's why:

(1) The definition in Evan and Anders' note, in pseudo-internal-language
    notation (ignoring the boundary constraint proofs) is: 

  hasWCom : (I → Set) → Set 
  hasWCom A = (r r' : I) → 
              (α : Set) {{cα : Cofib α}}
              (t : (x : I) → α → A x)
              (b : A r [ α ↦ t rα) ] )
              → A r' [ α ↦ t r' ]

  hasWPath :(I → Set) → (wcomA : hasWCom A) → Set
  hasWPath A wcomA = (r : I) → 
                     (α : Set) {{cα : Cofib α}}
                     (t : (x : I) → α → A x)
                     (b : A r [ α ↦ t r) ] )
                   → (Path (A r) (wcomA r r' α t b) (fst b)) [ α ↦ \ _ → t r' ]
  (i.e. the path is constantly t r' on α)

(2) If you move the r' binding inward and fuse the two functions into one, you get 

  hasWCom : (I → Set) → Set 
  hasWCom A = (r : I) → 
              (α : Set) {{cα : Cofib α}}
              (t : (x : I) → α → A x)
              (b : A r [ α ↦ t r) ] )
              → (Σ f:((r' : I) → A r'). Path (A r) (f r) b)
                [ α ↦ (\ r' → t r' , \ _ → t r) ]
  (i.e. on α, f is t - , and the path is constant.)

  If we ignore the partial element stuff for a bit, that's

  hasWCom : (I → Set) → Set 
  hasWCom A = (r : I) → 
              (b : A r )
              → (Σ f : ((r' : I) → A r'). Path (A r) (f r) b)

  which is 

  apply : (r : I) → ((x : I) → A x) → A r

  hasWCom : (I → Set l) → Set
  hasWCom A = (r : I) → 
              (b : A r )
              → HFiber (apply r) b

(3) Restoring and rearranging the partial element constraint to t
    instead of b gives

  hasWCom : (I → Set) → Set
  hasWCom A = (r : I) → 
              (α : Set) {{cα : Cofib α}}
              (b : A r )
              (t : α → (x : I) → (A x [x = r ↦ b]) )
              → (HFiber (apply r) b) [ α ↦ (\ r' → t r' pα , \ _ → t r) ]

   which is, strangely enough, exactly the weird definition of
   equivalence that a group came up with at Dagstuhl while trying to
   optmize cubicaltt.  

(4) Assuming using that weird definition of equivalence is not
    essential, we could rephrase using the hfiber-contractible
    definition, where contractible is defined to mean that any partial
    element extends to a total one: 

    -- trivial fibration: any partial element can be extended
    ContractibleFill : (A : Set) → Set 
    ContractibleFill A = (α : Set) {{cα : Cofib α}} → (t : α → A) → A [α ↦ t ]

    isEquivFill : (A : Set) (B : Set) (f : A → B) → Set 
    isEquivFill A B f = (b : B) → ContractibleFill (HFiber f b)

    isKan : (I → Set) → Set 
    isKan A = (r : I) → isEquivFill ((x : I) → A x) (A r) (apply A r)

    This unwinds to almost the operation you have, except
    that this definition has a partial element of the whole
    HFiber (apply A r) b on α, i.e. t r has a path to b,
    rather than being required to be strictly equal to it.  


For the strict one, we have

  hasCom : (I → Set l) → Set 
  hasCom A = (r r' : I) (α : Set) {{_ : Cofib α}} 
           → (t : (z : I) → α → A z) 
           → (b : A r [ α ↦ t r ]) 
           → A r' [ α ↦ t r' , (r = r') ↦ ⇒ (fst b) ]

  i.e.       (r : I) (α : Set) {{_ : Cofib α}} 
           → (t : (z : I) → α → A z) 
           → (b : A r [ α ↦ t r ]) 
           → Σ (f : (r' : I) → A r')[α ↦ t]. f r = b) 

  i.e.       (r : I) (b : A r)
           → (α : Set) {{_ : Cofib α}} 
           → (t : α → Σ f:((z : I) → A z). f r = b) 
           → Σ (f : (r' : I) → A r')[α ↦ t]. f r = b

  i.e.       (r : I) (b : A r)
           → (α : Set) {{_ : Cofib α}} 
           → (t : α → SFiber f b) 
           → SFiber f b [ α ↦ t ]  (using uniqueness for =) 

  i.e.       (r : I) (b : A r)
           → Contractible(SFiber f b)

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.