Skip to content

Commit

Permalink
Cartesian CuTT style fibrancy
Browse files Browse the repository at this point in the history
  • Loading branch information
loic-p committed Oct 26, 2020
1 parent 20eea8d commit bfc8e59
Showing 1 changed file with 69 additions and 112 deletions.
181 changes: 69 additions & 112 deletions theories/translation_fib.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,12 +27,6 @@ Admitted.

Definition cofib (p : ℙ) := forall q (α : q ≤ p), precofib q.

Definition lbox {p} : cofib p -> cofib (S p).
Admitted.

Definition rbox {p} : cofib p -> cofib (S p).
Admitted.

Definition is1 {p} : cofib p -> SProp.
Admitted.

Expand All @@ -45,43 +39,36 @@ Definition is1_match {p} {X : Type} (c : cofib p)
(b2 : (is1 c -> sFalse) -> X) : X.
Admitted.

Definition is1_promote_lbox {p q r} (α : q ≤ p) (β : r ≤ S q) (c : cofib p) :
is1 (β ⋅ lbox (α ⋅ c)) -> is1 ((promote α) ∘ β ⋅ lbox c).
Admitted.

Definition is1_promote_rbox {p q r} (α : q ≤ p) (β : r ≤ S q) (c : cofib p) :
is1 (β ⋅ rbox (α ⋅ c)) -> is1 ((promote α) ∘ β ⋅ rbox c).
Admitted.
Definition lid (p : ℙ) := p ≤ 1.

(* welcome to fibrancy HELL *)
Record FPsh@{i} : Type :=
mkFPsh {
fpsh0 : forall p : ℙ, Type@{i} ;
fpsh1 : forall p : ℙ, (forall q (α : q ≤ p), fpsh0 q) -> SProp ;
fpshl0 : forall (p : ℙ) (c : cofib p)
(s0 : forall (q : ℙ) (α : q ≤ S p) (αε : is1 (α ⋅ lbox c)), fpsh0 q)
(s1 : forall (q : ℙ) (α : q ≤ S p) (αε : is1 (α ⋅ lbox c)), fpsh1 q (fun r β => s0 r (α ∘ β) (is1_funct β _ αε))),
fpshl0 : forall (p : ℙ) (c : cofib p) (l l' : lid p)
(s0 : forall (q : ℙ) (α : q ≤ S p) (αε : is1 (squish ∘ α ⋅ c)), fpsh0 q)
(s1 : forall (q : ℙ) (α : q ≤ S p) (αε : is1 (squish ∘ α ⋅ c)), fpsh1 q (fun r β => s0 r (α ∘ β) (is1_funct β _ αε)))
(l0 : forall (q : ℙ) (α : q ≤ p), fpsh0 q)
(l1 : forall (q : ℙ) (α : q ≤ p),
fpsh1 q (fun r β => is1_match (α ∘ β ⋅ c)
(fun βε => s0 r ((merge ! l) ∘ α ∘ β) βε)
(fun _ => l0 r (α ∘ β)))),
fpsh0 p ;
fpshl1 : forall (p : ℙ) (c : cofib p)
(s0 : forall (q : ℙ) (α : q ≤ S p) (αε : is1 (α ⋅ lbox c)), fpsh0 q)
(s1 : forall (q : ℙ) (α : q ≤ S p) (αε : is1 (α ⋅ lbox c)), fpsh1 q (fun r β => s0 r (α ∘ β) (is1_funct β _ αε))),
fpsh1 p (fun q α => is1_match ((side_1 ∘ α) ⋅ lbox c)
(fun αε => s0 q (side_1 ∘ α) αε)
(fun _ => fpshl0 q (α ⋅ c)
(fun r β βε => s0 r (promote α ∘ β) (is1_promote_lbox α β c βε))
(fun r β βε => s1 r (promote α ∘ β) (is1_promote_lbox α β c βε)))) ;
fpshr0 : forall (p : ℙ) (c : cofib p)
(s0 : forall (q : ℙ) (α : q ≤ S p) (αε : is1 (α ⋅ rbox c)), fpsh0 q)
(s1 : forall (q : ℙ) (α : q ≤ S p) (αε : is1 (α ⋅ rbox c)), fpsh1 q (fun r β => s0 r (α ∘ β) (is1_funct β _ αε))),
fpsh0 p ;
fpshr1 : forall (p : ℙ) (c : cofib p)
(s0 : forall (q : ℙ) (α : q ≤ S p) (αε : is1 (α ⋅ rbox c)), fpsh0 q)
(s1 : forall (q : ℙ) (α : q ≤ S p) (αε : is1 (α ⋅ rbox c)), fpsh1 q (fun r β => s0 r (α ∘ β) (is1_funct β _ αε))),
fpsh1 p (fun q α => is1_match ((side_0 ∘ α) ⋅ rbox c)
(fun αε => s0 q (side_0 ∘ α) αε)
(fun _ => fpshr0 q (α ⋅ c)
(fun r β βε => s0 r (promote α ∘ β) (is1_promote_rbox α β c βε))
(fun r β βε => s1 r (promote α ∘ β) (is1_promote_rbox α β c βε)))) ;
fpshl1 : forall (p : ℙ) (c : cofib p) (l l' : lid p)
(s0 : forall (q : ℙ) (α : q ≤ S p) (αε : is1 (squish ∘ α ⋅ c)), fpsh0 q)
(s1 : forall (q : ℙ) (α : q ≤ S p) (αε : is1 (squish ∘ α ⋅ c)), fpsh1 q (fun r β => s0 r (α ∘ β) (is1_funct β _ αε)))
(l0 : forall (q : ℙ) (α : q ≤ p), fpsh0 q)
(l1 : forall (q : ℙ) (α : q ≤ p),
fpsh1 q (fun r β => is1_match (α ∘ β ⋅ c)
(fun βε => s0 r ((merge ! l) ∘ α ∘ β) βε)
(fun _ => l0 r (α ∘ β)))),
fpsh1 p (fun q α => is1_match (α ⋅ c)
(fun αε => s0 q ((merge ! l') ∘ α) αε)
(fun _ => fpshl0 q (α ⋅ c) (l ∘ α) (l' ∘ α)
(fun r β βε => s0 r (promote α ∘ β) βε)
(fun r β βε => s1 r (promote α ∘ β) βε)
(α ⋅ l0) (α ⋅ l1))) ;
}.

(* Elements of a presheaf *)
Expand Down Expand Up @@ -153,38 +140,35 @@ fun s => mkYtEl@{i j} q (yt_funct α f) (α ⋅ s.(ytel0)) (α ⋅ s.(ytel1)).
Record yft@{i j} (p : ℙ) := mkYFT {
yft0 : forall q (α : q ≤ p), Type@{i};
yft1 : forall q (α : q ≤ p), (forall r (β : r ≤ q), yft0 r (α ∘ β)) -> SProp;
yftl0 : forall (q : ℙ) (α : S q ≤ p) (c : cofib q)
(s0 : forall (r : ℙ) (β : r ≤ S q) (βε : is1 (β ⋅ lbox c)), yft0 r (α ∘ β))
(s1 : forall (r : ℙ) (β : r ≤ S q) (βε : is1 (β ⋅ lbox c)), yft1 r (α ∘ β) (fun r0 β0 => s0 r0 (β ∘ β0) (is1_funct β0 _ βε))),
yft0 q (α ∘ side_1) ;
yftl1 : forall (q : ℙ) (α : S q ≤ p) (c : cofib q)
(s0 : forall (r : ℙ) (β : r ≤ S q) (βε : is1 (β ⋅ lbox c)), yft0 r (α ∘ β))
(s1 : forall (r : ℙ) (β : r ≤ S q) (βε : is1 (β ⋅ lbox c)), yft1 r (α ∘ β) (fun r0 β0 => s0 r0 (β ∘ β0) (is1_funct β0 _ βε))),
yft1 q (α ∘ side_1) (fun r (β : r ≤ q) => is1_match ((side_1 ∘ β) ⋅ lbox c)
(fun βε => s0 r (side_1 ∘ β) βε)
(fun _ => yftl0 r (α ∘ promote β) (β ⋅ c)
(fun r0 β0 β0ε => s0 r0 (promote β ∘ β0) (is1_promote_lbox β β0 c β0ε))
(fun r0 β0 β0ε => s1 r0 (promote β ∘ β0) (is1_promote_lbox β β0 c β0ε)))) ;
yftr0 : forall (q : ℙ) (α : S q ≤ p) (c : cofib q)
(s0 : forall (r : ℙ) (β : r ≤ S q) (βε : is1 (β ⋅ rbox c)), yft0 r (α ∘ β))
(s1 : forall (r : ℙ) (β : r ≤ S q) (βε : is1 (β ⋅ rbox c)), yft1 r (α ∘ β) (fun r0 β0 => s0 r0 (β ∘ β0) (is1_funct β0 _ βε))),
yft0 q (α ∘ side_0) ;
yftr1 : forall (q : ℙ) (α : S q ≤ p) (c : cofib q)
(s0 : forall (r : ℙ) (β : r ≤ S q) (βε : is1 (β ⋅ rbox c)), yft0 r (α ∘ β))
(s1 : forall (r : ℙ) (β : r ≤ S q) (βε : is1 (β ⋅ rbox c)), yft1 r (α ∘ β) (fun r0 β0 => s0 r0 (β ∘ β0) (is1_funct β0 _ βε))),
yft1 q (α ∘ side_0) (fun r (β : r ≤ q) => is1_match ((side_0 ∘ β) ⋅ rbox c)
(fun βε => s0 r (side_0 ∘ β) βε)
(fun _ => yftr0 r (α ∘ promote β) (β ⋅ c)
(fun r0 β0 β0ε => s0 r0 (promote β ∘ β0) (is1_promote_rbox β β0 c β0ε))
(fun r0 β0 β0ε => s1 r0 (promote β ∘ β0) (is1_promote_rbox β β0 c β0ε)))) ;
yftl0 : forall (q : ℙ) (α : S q ≤ p) (c : cofib q) (l l' : lid q)
(s0 : forall (r : ℙ) (β : r ≤ S q) (βε : is1 (squish ∘ β ⋅ c)), yft0 r (α ∘ β))
(s1 : forall (r : ℙ) (β : r ≤ S q) (βε : is1 (squish ∘ β ⋅ c)), yft1 r (α ∘ β) (fun r0 β0 => s0 r0 (β ∘ β0) (is1_funct β0 _ βε)))
(l0 : forall (r : ℙ) (β : r ≤ q), yft0 r (α ∘ (merge ! l) ∘ β))
(l1 : forall (r : ℙ) (β : r ≤ q),
yft1 r (α ∘ (merge ! l) ∘ β) (fun r0 β0 => is1_match (β ∘ β0 ⋅ c)
(fun β0ε => s0 r0 ((merge ! l) ∘ β ∘ β0) β0ε)
(fun _ => l0 r0 (β ∘ β0)))),
yft0 q (α ∘ (merge ! l')) ;
yftl1 : forall (q : ℙ) (α : S q ≤ p) (c : cofib q) (l l' : lid q)
(s0 : forall (r : ℙ) (β : r ≤ S q) (βε : is1 (squish ∘ β ⋅ c)), yft0 r (α ∘ β))
(s1 : forall (r : ℙ) (β : r ≤ S q) (βε : is1 (squish ∘ β ⋅ c)), yft1 r (α ∘ β) (fun r0 β0 => s0 r0 (β ∘ β0) (is1_funct β0 _ βε)))
(l0 : forall (r : ℙ) (β : r ≤ q), yft0 r (α ∘ (merge ! l) ∘ β))
(l1 : forall (r : ℙ) (β : r ≤ q),
yft1 r (α ∘ (merge ! l) ∘ β) (fun r0 β0 => is1_match (β ∘ β0 ⋅ c)
(fun β0ε => s0 r0 ((merge ! l) ∘ β ∘ β0) β0ε)
(fun _ => l0 r0 (β ∘ β0)))),
yft1 q (α ∘ (merge ! l')) (fun r β => is1_match (β ⋅ c)
(fun βε => s0 r ((merge ! l') ∘ β) βε)
(fun _ => yftl0 r (α ∘ promote β) (β ⋅ c) (l ∘ β) (l' ∘ β)
(fun r0 β0 β0ε => s0 r0 (promote β ∘ β0) β0ε)
(fun r0 β0 β0ε => s1 r0 (promote β ∘ β0) β0ε)
(β ⋅ l0) (β ⋅ l1))) ;
}.

Arguments yft0 {_}.
Arguments yft1 {_}.
Arguments yftl0 {_}.
Arguments yftl1 {_}.
Arguments yftr0 {_}.
Arguments yftr1 {_}.

Definition yft_funct@{i j} {p q : ℙ} (α : q ≤ p) :
yft@{i j} p -> yft@{i j} q :=
Expand All @@ -194,8 +178,6 @@ fun f =>
yft1 := α ⋅ yft1 f;
yftl0 := α ⋅ yftl0 f;
yftl1 := α ⋅ yftl1 f;
yftr0 := α ⋅ yftr0 f;
yftr1 := α ⋅ yftr1 f;
|}.

Definition yftR@{i j k} {p : ℙ} (s : forall q : nat, q ≤ p -> yft@{i j} q) : SProp :=
Expand Down Expand Up @@ -241,20 +223,15 @@ fun s => mkYftEl@{i j k} q (yft_funct α f) (α ⋅ s.(yftel0)) (α ⋅ s.(yftel
Definition Uᶠ@{i j k l} : Psh@{l} :=
mkPsh@{l} yft@{i j} (fun p s => yftR@{i j k} s).

Definition Gluel {p : ℙ}
(c : cofib p)
(s0 : forall q (α : q ≤ S p), is1 (α ⋅ lbox c) -> yft q)
(s1 : forall q (α : q ≤ S p) (αε : is1 (α ⋅ lbox c)),
yftR (fun r β => s0 r (α ∘ β) (is1_funct β (α ⋅ lbox c) αε))) :
yft p.
Proof.
Admitted.

Definition Gluer {p : ℙ}
(c : cofib p)
(s0 : forall q (α : q ≤ S p), is1 (α ⋅ rbox c) -> yft q)
(s1 : forall q (α : q ≤ S p) (αε : is1 (α ⋅ rbox c)),
yftR (fun r β => s0 r (α ∘ β) (is1_funct β (α ⋅ rbox c) αε))) :
Definition Glue {p : ℙ}
(c : cofib p) (l l' : lid p)
(s0 : forall q (α : q ≤ S p), is1 (squish ∘ α ⋅ c) -> yft q)
(s1 : forall q (α : q ≤ S p) (αε : is1 (squish ∘ α ⋅ c)),
yftR (fun r β => s0 r (α ∘ β) (is1_funct β _ αε)))
(l0 : forall q (α : q ≤ p), yft q)
(l1 : forall q (α : q ≤ p), yftR (fun r β => is1_match (α ∘ β ⋅ c)
(fun βε => s0 r (merge ! l ∘ α ∘ β) βε)
(fun _ => l0 r (α ∘ β)))) :
yft p.
Proof.
Admitted.
Expand All @@ -264,21 +241,10 @@ Proof.
unshelve econstructor.
- exact (fun q α => yft q).
- refine (fun q α s => yftR s).
- refine (fun q α c s0 s1 => _).
refine (Gluel c s0 s1).
- refine (fun q α c s0 s1 => _).
refine (Gluer c s0 s1).
- refine (fun q α c s0 s1 r β => _).
simpl in s0 ; simpl in s1.
apply sfalso.
- refine (fun q α c s0 s1 r β => _).
simpl in s0 ; simpl in s1.
- refine (fun q α c l l' s0 s1 l0 l1 => _).
refine (Glue c l l' s0 s1 l0 l1).
- refine (fun q α c l l' s0 s1 l0 l1 => _).
apply sfalso.
(* unshelve econstructor.
+ refine (fun r β => _).
refine (is1_match (side_1 ∘ β ⋅ lbox c) (fun βε => _) (fun _ => _)).
* refine (yft0 (s0 r (side_1 ∘ β) βε) r !).
* apply falso. *)
Defined.

Definition U1 (p : ℙ) : psh1 Uᶠ p (fun q α => U0 q).
Expand Down Expand Up @@ -334,10 +300,8 @@ Proof.
unshelve econstructor.
- refine (fun r β => bool).
- refine (fun r β s => boolR s).
- refine (fun r β c s0 s1 => _). apply falso.
- refine (fun r β c s0 s1 => _). apply falso.
- refine (fun r β c s0 s1 => _). apply sfalso.
- refine (fun r β c s0 s1 => _). apply sfalso.
- refine (fun r β c l l' s0 s1 l0 l1 => _). apply falso.
- refine (fun r β c l l' s0 s1 l0 l1 => _). apply sfalso.
Defined.

Definition bool1 {p} : @El1 p Type0 Type1 bool0.
Expand Down Expand Up @@ -381,10 +345,9 @@ unshelve econstructor.
(B0 r (α ∘ β)).(yft1) r ! (fun r' β' => _)).
unshelve refine (cast0 B0 B1 (α ∘ β) β' _).
exact (f r' β' (β' · x0) (β' · x1)).
- refine (fun r β c s0 s1 x0 x1 => _). apply falso.
- refine (fun r β c s0 s1 x0 x1 => _). apply falso.
- refine (fun r β c s0 s1 x0 x1 => _). apply sfalso.
- refine (fun r β c s0 s1 x0 x1 => _). apply sfalso.
- refine (fun r β c l l' s0 s1 l0 l1 x0 x1 => _).
simpl in *. apply falso.
- refine (fun r β c l l' s0 s1 l0 l1 x0 x1 => _). apply sfalso.
Defined.

Definition Arr1 {p}
Expand Down Expand Up @@ -477,10 +440,8 @@ unshelve econstructor.
exact (SigmaT (α ∘ β ⋅ A0) (α ∘ β ⋅ A1) (α ∘ β ⋅ P0) (α ∘ β ⋅ P1)).
- refine (fun r β => _).
exact (SigmaR (α ∘ β ⋅ A0) (α ∘ β ⋅ A1) (α ∘ β ⋅ P0) (α ∘ β ⋅ P1)).
- refine (fun r β c s0 s1 => _). apply falso.
- refine (fun r β c s0 s1 => _). apply falso.
- refine (fun r β c s0 s1 => _). apply sfalso.
- refine (fun r β c s0 s1 => _). apply sfalso.
- refine (fun r β c l l' s0 s1 l0 l1 => _). apply falso.
- refine (fun r β c l l' s0 s1 l0 l1 => _). apply sfalso.
Defined.

Definition Sigma1 {p}
Expand Down Expand Up @@ -770,10 +731,8 @@ unshelve econstructor.
(fun r3 (β3 : r3 ≤ r) => B0 r3 (α ∘ β ∘ β3) (β3 · x0) (β3 · x1))
(fun r3 (β3 : r3 ≤ r) => B1 r3 (α ∘ β ∘ β3) (β3 · x0) (β3 · x1))
_ ! _ β2 (f0 r2 _ (β2 · x0) (β2 · x1))).
- refine (fun r β c s0 s1 => _). apply falso.
- refine (fun r β c s0 s1 => _). apply falso.
- refine (fun r β c s0 s1 => _). apply sfalso.
- refine (fun r β c s0 s1 => _). apply sfalso.
- refine (fun r β c l l' s0 s1 l0 l1 x0 x1 => _). apply falso.
- refine (fun r β c l l' s0 s1 l0 l1 x0 x1 => _). apply sfalso.
Defined.

Definition Prod1 {p}
Expand Down Expand Up @@ -890,10 +849,8 @@ unshelve econstructor.
exact (cube_eq ((α ∘ β) · A0) ((α ∘ β) · A1) ((α ∘ β) · x0) ((α ∘ β) · y0)).
- unshelve refine (fun r β s => _). simpl in s.
exact (cube_eqR ((α ∘ β) · A0) ((α ∘ β) · A1) ((α ∘ β) · x0) ((α ∘ β) · y0) s).
- refine (fun r β c s0 s1 => _). apply falso.
- refine (fun r β c s0 s1 => _). apply falso.
- refine (fun r β c s0 s1 => _). apply sfalso.
- refine (fun r β c s0 s1 => _). apply sfalso.
- refine (fun r β c l l' s0 s1 l0 l1 => _). apply falso.
- refine (fun r β c l l' s0 s1 l0 l1 => _). apply sfalso.
Defined.

Definition eq1 {p}
Expand Down

0 comments on commit bfc8e59

Please sign in to comment.