```Discussion of Homotopy Type Theory and Univalent Foundations
help / color / mirror / Atom feed```
```From: "Licata, Dan" <dlicata@wesleyan.edu>
Subject: Re: [HoTT] A unifying cartesian cubical type theory
Date: Sun, 17 Feb 2019 14:14:48 +0000	[thread overview]
Message-ID: <96E42DDC-22B2-4B55-9A59-1A118D4C088F@wesleyan.edu> (raw)

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

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.
```

```next prev parent reply	other threads:[~2019-02-17 14:14 UTC|newest]

Thread overview: 18+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-02-14 19:04 Anders Mortberg
2019-02-14 20:06 ` Andrew Pitts
2019-02-15 15:38   ` Anders Mörtberg
2019-02-15  8:16 ` Bas Spitters
2019-02-15 16:32   ` Anders Mörtberg
2019-02-16  0:01     ` Michael Shulman
2019-02-16  0:14       ` Steve Awodey
2019-02-16 12:30         ` streicher
2019-02-16 19:51           ` Thomas Streicher
2019-02-16 22:27             ` Steve Awodey
2019-02-17  9:43               ` Thomas Streicher
2019-02-17 14:14                 ` Licata, Dan [this message]
2019-02-16 21:58           ` Richard Williamson
2019-02-17  9:15             ` Thomas Streicher
2019-02-17 13:49               ` Richard Williamson
2019-02-18 14:05 ` [HoTT] " Andrew Swan
2019-02-18 15:31   ` Anders Mörtberg
2019-06-16 16:04     ` Anders Mörtberg
```

```Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,

Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

switches of git-send-email(1):

git send-email \
```This is a public inbox, see mirroring instructions