{-# OPTIONS --without-K #-}
module segal.composition.l3 where
open import sum
open import equality
open import level
open import function.extensionality
open import function.isomorphism
open import hott.equivalence
open import hott.level
open import segal.composition.l1
open import segal.composition.l2
open import segal.preliminaries
module _ {i} (W : Wild₂ i) where
open WildOps₂ W
IsWild₃ : Set i
IsWild₃ = {a b c d : obj 𝓒}
→ (f : hom 𝓒 a b)
→ (g : hom 𝓒 b c)
→ (h : hom 𝓒 c d)
→ h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
module _ {i} (X : Segal₂ i) where
open SegalOps₂ X
Horn-3-1 = Σ X₀ λ x0 → Σ X₀ λ x1 → Σ X₀ λ x2 → Σ X₀ λ x3
→ Σ (X₁ x0 x1) λ x01 → Σ (X₁ x0 x2) λ x02
→ Σ (X₁ x0 x3) λ x03 → Σ (X₁ x1 x2) λ x12
→ Σ (X₁ x1 x3) λ x13 → Σ (X₁ x2 x3) λ x23
→ X₂' x01 x02 x12 × X₂' x01 x03 x13 × X₂' x12 x13 x23
Spine-3 = Σ X₀ λ x0 → Σ X₀ λ x1 → Σ X₀ λ x2 → Σ X₀ λ x3
→ X₁ x0 x1 × X₁ x1 x2 × X₁ x2 x3
Filler₃ = (x0 x1 x2 x3 : X₀)
(x01 : X₁ x0 x1) (x02 : X₁ x0 x2)
(x03 : X₁ x0 x3) (x12 : X₁ x1 x2)
(x13 : X₁ x1 x3) (x23 : X₁ x2 x3)
→ X₂' x01 x02 x12 → X₂' x01 x03 x13
→ X₂' x02 x03 x23 → X₂' x12 x13 x23
→ Set i
GenAssoc₃ = (h : Horn-3-1)
→ let (x0 , x1 , x2 , x3 , x01 , x02 , x03 ,
x12 , x13 , x23 , x012 , x013 , x123) = h
in X₂ x0 x2 x3 x02 x03 x23
SegalCondition₃ : Filler₃ → Set _
SegalCondition₃ X₃ = (h : Horn-3-1)
→ let (x0 , x1 , x2 , x3 , x01 , x02 , x03 , x12 ,
x13 , x23 , x012 , x013 , x123) = h
in contr (Σ (X₂ x0 x2 x3 x02 x03 x23) λ x023
→ X₃ x0 x1 x2 x3 x01 x02 x03 x12 x13 x23 x012 x013 x023 x123)
segal-cond-h1 : (X₃ : Filler₃) → h 1 (SegalCondition₃ X₃)
segal-cond-h1 X₃ = Π-level λ h → hn-h1 0 _
IsSegal₃ : Set (lsuc i)
IsSegal₃ = Σ Filler₃ SegalCondition₃
module _ {i} (W : Wild₂ i) where
private
X = invert≅ segal-wild₂ W
open SegalOps₂ X
open WildOps₂ W
private
spine⇒horn : Spine-3 X → Horn-3-1 X
spine⇒horn (x0 , x1 , x2 , x3 , x01 , x12 , x23)
= (x0 , x1 , x2 , x3 , x01 , x12 ∘ x01 , (x23 ∘ x12) ∘ x01 ,
x12 , x23 ∘ x12 , x23 , refl , refl , refl )
horn⇒spine : Horn-3-1 X → Spine-3 X
horn⇒spine (x0 , x1 , x2 , x3 , x01 , x02 , x03 ,
x12 , x13 , x23 , x012 , x013 , x123)
= (x0 , x1 , x2 , x3 , x01 , x12 , x23)
abstract
spine-horn' : Spine-3 X ≅ Horn-3-1 X
spine-horn' = begin
Spine-3 X
≅⟨ add-contr (λ { (x0 , x1 , x2 , x3 , x01 , x12 , x23) →
Σ-contr (hf₂ (x0 , x1 , x2 , x01 , x12)) (λ { (x02 , x012) →
Σ-contr (hf₂ (x1 , x2 , x3 , x12 , x23)) (λ { (x13 , x123) →
hf₂ (x0 , x1 , x3 , x01 , x13) }) }) } ) ⟩
( Σ (Spine-3 X) λ s
→ let (x0 , x1 , x2 , x3 , x01 , x12 , x23) = s
in Σ (Σ (X₁ x0 x2) λ x02 → X₂ x0 x1 x2 x01 x02 x12) λ { (x02 , x012) →
Σ (Σ (X₁ x1 x3) λ x13 → X₂ x1 x2 x3 x12 x13 x23) λ { (x13 , x123) →
(Σ (X₁ x0 x3) λ x03 → X₂ x0 x1 x3 x01 x03 x13) } } )
≅⟨ record
{ to = λ { ((x0 , x1 , x2 , x3 , x01 , x12 , x23) ,
(x02 , x012) , (x13 , x123) , (x03 , x013))
→ (x0 , x1 , x2 , x3 , x01 , x02 , x03 ,
x12 , x13 , x23 , x012 , x013 , x123) }
; from = λ { (x0 , x1 , x2 , x3 , x01 , x02 , x03 ,
x12 , x13 , x23 , x012 , x013 , x123)
→ ((x0 , x1 , x2 , x3 , x01 , x12 , x23) ,
(x02 , x012) , (x13 , x123) , (x03 , x013)) }
; iso₁ = λ _ → refl
; iso₂ = λ _ → refl } ⟩
Horn-3-1 X
∎ where open ≅-Reasoning
spine-horn-iso₂ : (h : Horn-3-1 X) → spine⇒horn (horn⇒spine h) ≡ h
spine-horn-iso₂ = _≅_.iso₂ spine-horn'
spine-horn₃ : Spine-3 X ≅ Horn-3-1 X
spine-horn₃ = record
{ to = spine⇒horn
; from = horn⇒spine
; iso₁ = λ _ → refl
; iso₂ = spine-horn-iso₂ }
module _ {i} (W : Wild₂ i) where
private X = invert≅ segal-wild₂ W
open SegalOps₂ X
open WildOps₂ W
private
module is-segal-gen-assoc-tmp where
g : GenAssoc₃ X → IsSegal₃ X
g assoc' =
(λ x0 x1 x2 x3 x01 x02 x03 x12 x13 x23 x012 x013 x023 x123
→ assoc' (x0 , x1 , x2 , x3 , x01 , x02 , x03 ,
x12 , x13 , x23 , x012 , x013 , x123) ≡ x023) ,
(λ _ → singl-contr _)
abstract
abs-iso : IsSegal₃ X ≅ GenAssoc₃ X
abs-iso = begin
IsSegal₃ X
≅⟨ record
{ to = λ {(X₂ , hf₂)
→ λ { (x0 , x1 , x2 , x3 , x01 , x02 , x03 ,
x12 , x13 , x23 , x012 , x013 , x123)
→ (λ x023 → X₂ x0 x1 x2 x3 x01 x02 x03 x12 x13 x23 x012 x013 x023 x123)
, hf₂ (x0 , x1 , x2 , x3 , x01 , x02 , x03 ,
x12 , x13 , x23 , x012 , x013 , x123) } }
; from = λ t → (λ x0 x1 x2 x3 x01 x02 x03 x12 x13 x23 x012 x013 x023 x123
→ proj₁ (t (x0 , x1 , x2 , x3 , x01 , x02 , x03 ,
x12 , x13 , x23 , x012 , x013 , x123)) x023)
, (λ h → proj₂ (t h))
; iso₁ = λ _ → refl
; iso₂ = λ _ → refl } ⟩
((h : Horn-3-1 X)
→ let (x0 , x1 , x2 , x3 , x01 , x02 , x03 ,
x12 , x13 , x23 , x012 , x013 , x123) = h
in ( Σ (X₂ x0 x2 x3 x02 x03 x23 → Set i) λ Fill
→ contr (Σ _ Fill)))
≅⟨ ( Π-ap-iso refl≅ (λ {
(x0 , x1 , x2 , x3 , x01 , x02 , x03 ,
x12 , x13 , x23 , x012 , x013 , x123)
→ contr-predicate })) ⟩
((h : Horn-3-1 X)
→ let (x0 , x1 , x2 , x3 , x01 , x02 , x03 ,
x12 , x13 , x23 , x012 , x013 , x123) = h
in X₂ x0 x2 x3 x02 x03 x23 )
∎
where open ≅-Reasoning
abs-iso-β : (a : GenAssoc₃ X) → g a ≡ invert≅ abs-iso a
abs-iso-β _ = refl
is-segal-gen-assoc₃ : IsSegal₃ X ≅ GenAssoc₃ X
is-segal-gen-assoc₃ = iso f' g α β
where
open is-segal-gen-assoc-tmp
open _≅_ abs-iso renaming
( to to f' ; from to g'
; iso₁ to α' ; iso₂ to β' )
α : (a : IsSegal₃ X) → g (f' a) ≡ a
α a = abs-iso-β (f' a) · α' a
β : (a : GenAssoc₃ X) → f' (g a) ≡ a
β a = ap f' (abs-iso-β a) · β' a
private
module gen-assoc-is-wild-tmp where
f : GenAssoc₃ X → IsWild₃ W
f assoc' {x0} {x1} {x2} {x3} x01 x12 x23 = assoc'
(x0 , x1 , x2 , x3 , x01 , x12 ∘ x01 , (x23 ∘ x12) ∘ x01 ,
x12 , x23 ∘ x12 , x23 , refl , refl , refl)
g : IsWild₃ W → GenAssoc₃ X
g assoc
(x0 , x1 , x2 , x3 , x01 , x02 , x03 ,
x12 , x13 , x23 , x012 , x013 , x123)
= sym (ap (λ f → x23 ∘ f) x012)
· assoc x01 x12 x23
· ap (λ f → f ∘ x01) x123
· x013
β : (a : IsWild₃ W) → _≡_ {A = IsWild₃ W} (f (g a)) a
β a = impl-funext λ x0 → impl-funext λ x1 → impl-funext λ x2 → impl-funext λ x3
→ funext λ x01 → funext λ x12 → funext λ x23 → lem
where
lem : ∀ {j}{A : Set j}{a b : A}{p : a ≡ b}
→ p · refl · refl ≡ p
lem {p = refl} = refl
abstract
assoc-iso : GenAssoc₃ X ≅ IsWild₃ W
assoc-iso = begin
GenAssoc₃ X
≅⟨ (Π-ap-iso (sym≅ (spine-horn₃ W)) λ s → refl≅) ⟩
((s : Spine-3 X)
→ let (x0 , x1 , x2 , x3 , x01 , x12 , x23) = s
in X₂ x0 x2 x3 (x12 ∘ x01) ((x23 ∘ x12) ∘ x01) x23)
≅⟨ refl≅ ⟩
((s : Spine-3 X)
→ let (x0 , x1 , x2 , x3 , x01 , x12 , x23) = s
in x23 ∘ (x12 ∘ x01) ≡ (x23 ∘ x12) ∘ x01)
≅⟨ record
{ to = λ t {x0} {x1} {x2} {x3} x01 x12 x23
→ t (x0 , x1 , x2 , x3 , x01 , x12 , x23)
; from = λ { t (x0 , x1 , x2 , x3 , x01 , x12 , x23)
→ t x01 x12 x23 }
; iso₁ = λ _ → refl
; iso₂ = λ _ → refl } ⟩
IsWild₃ W
∎
where open ≅-Reasoning
α : (a : GenAssoc₃ X) → g (f a) ≡ a
α a = iso⇒inj assoc-iso (β (f a))
gen-assoc-is-wild₃ : GenAssoc₃ X ≅ IsWild₃ W
gen-assoc-is-wild₃ = iso f g α β
where
open gen-assoc-is-wild-tmp
is-segal-is-wild₃ : IsSegal₃ X ≅ IsWild₃ W
is-segal-is-wild₃ = is-segal-gen-assoc₃ ·≅ gen-assoc-is-wild₃
Wild₃ : (i : Level) → Set (lsuc i)
Wild₃ i = Σ (Wild₂ i) IsWild₃
module WildOps₃ {i} (W : Wild₃ i) where
open Σ W renaming (proj₁ to W|2; proj₂ to assoc₁) public
open WildOps₂ W|2 public
Segal₃ : (i : Level) → Set _
Segal₃ i = Σ (Segal₂ i) IsSegal₃
module SegalOps₃ {i} (X : Segal₃ i) where
open Σ X renaming (proj₁ to X|2; proj₂ to s₃X) public
open SegalOps₂ X|2 public
open Σ s₃X renaming (proj₁ to X₃; proj₂ to hf₃) public
X₃' : {x0 x1 x2 x3 : X₀}
{x01 : X₁ x0 x1} {x02 : X₁ x0 x2}
{x03 : X₁ x0 x3} {x12 : X₁ x1 x2}
{x13 : X₁ x1 x3} {x23 : X₁ x2 x3}
→ X₂' x01 x02 x12 → X₂' x01 x03 x13
→ X₂' x02 x03 x23 → X₂' x12 x13 x23 → Set i
X₃' x012 x013 x023 x123 = X₃ _ _ _ _ _ _ _ _ _ _ x012 x013 x023 x123
segal-wild₃ : ∀ {i} → Segal₃ i ≅ Wild₃ i
segal-wild₃ = Σ-ap-iso' segal-wild₂ is-segal-is-wild₃
module _ {i} (W : Wild₃ i) where
private X = invert≅ segal-wild₃ W
open WildOps₃ W
open SegalOps₃ X
X₃-β : (x0 x1 x2 x3 : X₀)
(x01 : X₁ x0 x1) (x02 : X₁ x0 x2)
(x03 : X₁ x0 x3) (x12 : X₁ x1 x2)
(x13 : X₁ x1 x3) (x23 : X₁ x2 x3)
(x012 : X₂' x01 x02 x12)(x013 : X₂' x01 x03 x13)
(x023 : X₂' x02 x03 x23)(x123 : X₂' x12 x13 x23)
→ X₃' x012 x013 x023 x123
≡ ( sym (ap (λ f → x23 ∘ f) x012)
· assoc₁ x01 x12 x23
· ap (λ f → f ∘ x01) x123 · x013
≡ x023 )
X₃-β x0 x1 x2 x3 x01 x02 x03 x12 x13 x23 x012 x013 x023 x123 = refl