Minor style fix.

HoTT · May 8, 2017 · 7278ce7 · 7278ce7
1 parent f7897a0
commit 7278ce7
Show file tree

Hide file tree

Showing 2 changed files with 55 additions and 18 deletions.
diff --git a/theorems/stash/modalities/JoinAdj.agda b/theorems/stash/modalities/JoinAdj.agda
@@ -9,11 +9,11 @@ module stash.modalities.JoinAdj {i j k}
   private
 
     module From (f : B → C) (γ : A → hfiber cst f)
-      = JoinRec (fst ∘ γ) f (λ { (a , b) → app= (snd (γ a)) b })
+      = JoinRec (fst ∘ γ) f (λ a b → app= (snd (γ a)) b)
 
     from-β : (f : B → C) (γ : A → hfiber cst f)
-             (a : A) (b : B) → ap (From.f f γ) (glue (a , b)) == app= (snd (γ a)) b
-    from-β f γ a b = From.glue-β f γ (a , b)
+             (a : A) (b : B) → ap (From.f f γ) (jglue a b) == app= (snd (γ a)) b
+    from-β f γ a b = From.glue-β f γ a b
 
     to : (A * B → C) → Σ (B → C) (λ f → A → hfiber cst f)
     to φ = φ ∘ right , (λ a → φ (left a) , λ= (λ b → ap φ (glue (a , b))))
@@ -30,16 +30,17 @@ module stash.modalities.JoinAdj {i j k}
               coh a = pair= idp (ap λ= (λ= (λ b → from-β f γ a b)) ∙ ! (λ=-η (snd (γ a))))
 
       from-to : (φ : A * B → C) → from (to φ) == φ
-      from-to φ = λ= (Join-elim (λ a → idp) (λ b → idp) (λ ab → ↓-==-in (coh ab)))
-
-        where coh : (ab : A × B) → ap φ (glue ab) == ap (from (to φ)) (glue ab) ∙ idp
-              coh (a , b) = ap φ (glue (a , b))
-                               =⟨ ! (app=-β (λ b → ap φ (glue (a , b))) b) ⟩
-                            app= (λ= (λ b → ap φ (glue (a , b)))) b
-                               =⟨ ! (from-β (fst (to φ)) (snd (to φ)) a b) ⟩
-                            ap (From.f (fst (to φ)) (snd (to φ))) (glue (a , b))
-                               =⟨ ! (∙-unit-r (ap (from (to φ)) (glue (a , b)))) ⟩ 
-                            ap (from (to φ)) (glue (a , b)) ∙ idp ∎
+      from-to φ = λ= (Join-elim (λ a → idp) (λ b → idp) (λ a b → ↓-==-in (coh a b)))
+
+        where coh : ∀ a b → ap φ (jglue a b) == ap (from (to φ)) (jglue a b) ∙ idp
+              coh a b = ap φ (jglue a b)
+                           =⟨ ! (app=-β (λ b → ap φ (jglue a b)) b) ⟩
+                        app= (λ= (λ b → ap φ (jglue a b))) b
+                           =⟨ ! (from-β (fst (to φ)) (snd (to φ)) a b) ⟩
+                        ap (From.f (fst (to φ)) (snd (to φ))) (jglue a b)
+                           =⟨ ! (∙-unit-r (ap (from (to φ)) (jglue a b))) ⟩ 
+                        ap (from (to φ)) (jglue a b) ∙ idp
+                           =∎
 
   join-adj : (A * B → C) ≃ Σ (B → C) (λ f → A → hfiber cst f)
   join-adj = equiv to from to-from from-to

diff --git a/theorems/stash/modalities/Orthogonality.agda b/theorems/stash/modalities/Orthogonality.agda
@@ -58,7 +58,13 @@ module stash.modalities.Orthogonality where
       g-f = λ a → idp ;
       adj = λ a → λ=-η idp }
 
-    equiv-preserves-orth-l : {A B X : Type ℓ} → (A ≃ B) → ⟦ A ⊥ X ⟧ → ⟦ B ⊥ X ⟧
+    Δ-equiv-is-contr : (A : Type i) → is-equiv (Δ A A) → is-contr A
+    Δ-equiv-is-contr A e = is-equiv.g e (idf A) , (λ a → app= (is-equiv.f-g e (idf A)) a)
+
+    self-orth-is-contr : (A : Type i) → ⟦ A ⊥ A ⟧ → is-contr A
+    self-orth-is-contr A ω = Δ-equiv-is-contr A ω
+
+    equiv-preserves-orth-l : {A B X : Type i} → (A ≃ B) → ⟦ A ⊥ X ⟧ → ⟦ B ⊥ X ⟧
     equiv-preserves-orth-l {A} {B} {X} (f , f-ise) ω = is-eq (Δ X B) g f-g ω.g-f
 
       where module ω = is-equiv ω
@@ -70,7 +76,7 @@ module stash.modalities.Orthogonality where
             f-g : (φ : B → X) → Δ X B (g φ) == φ
             f-g φ = λ= λ b → app= (ω.f-g (φ ∘ f)) (f.g b) ∙ ap φ (f.f-g b)
 
-    equiv-preserves-orth-r : {A X Y : Type ℓ} → (X ≃ Y) → ⟦ A ⊥ X ⟧ → ⟦ A ⊥ Y ⟧
+    equiv-preserves-orth-r : {A X Y : Type i} → (X ≃ Y) → ⟦ A ⊥ X ⟧ → ⟦ A ⊥ Y ⟧
     equiv-preserves-orth-r {A} {X} {Y} (f , f-ise) ω = is-eq (Δ Y A) g f-g g-f
 
       where module ω = is-equiv ω
@@ -85,6 +91,19 @@ module stash.modalities.Orthogonality where
             g-f : (y : Y) → g (Δ Y A y) == y
             g-f y = ap f (ω.g-f (f.g y)) ∙ f.f-g y
 
+    Σ-orth : {A X : Type i} {B : A → Type i} → ⟦ A ⊥ X ⟧ → (B⊥ : (a : A) → ⟦ B a ⊥ X ⟧) → ⟦ Σ A B ⊥ X ⟧
+    Σ-orth {A} {X} {B} A⊥ B⊥ = is-eq _ from to-from from-to
+
+      where from : (Σ A B → X) → X
+            from φ = ctr A⊥ (λ a → ctr (B⊥ a) (λ b → φ (a , b)))
+
+            to-from : (φ : Σ A B → X) → cst (from φ) == φ
+            to-from φ = λ= (λ { (a , b) → app= (ctr-null A⊥ (λ a → ctr (B⊥ a) (λ b → φ (a , b)))) a ∙
+                                           app= (ctr-null (B⊥ a) (λ b → φ (a , b))) b })
+
+            from-to : (x : X) → from (cst x) == x
+            from-to x = ap (ctr A⊥) (λ= (λ a → ctr-cst (B⊥ a) x)) ∙ ctr-cst A⊥ x
+
     -- -- This works if the base is connected, but you'll have to add that
     -- fib-orth : {A X : Type i} {B : A → Type i} → ⟦ Σ A B ⊥ X ⟧ →  (a : A) → ⟦ B a ⊥ X ⟧
     -- fib-orth {A} {X} {B} Σ⊥ a = is-eq _ g {!!} {!!}
@@ -105,6 +124,22 @@ module stash.modalities.Orthogonality where
     ×-orth : {A B X : Type i} → ⟦ A ⊥ X ⟧ → ⟦ B ⊥ X ⟧ → ⟦ A × B ⊥ X ⟧
     ×-orth {B = B} A⊥ B⊥ = Σ-orth {B = λ _ → B} A⊥ (λ _ → B⊥)
 
+    -- Okay, you need to find a simpler way.
+    -- *-orth : {A B X : Type i} → ⟦ B ⊥ X ⟧ → ⟦ A * B ⊥ X ⟧
+    -- *-orth {A} {B} {X} ω = is-eq (Δ X (A * B)) from to-from from-to
+
+    --   where from : (A * B → X) → X
+    --         from f = is-equiv.g ω (f ∘ right)
+
+    --           where test : A → hfiber cst (f ∘ right)
+    --                 test =  snd (–> (join-adj A B X) f) 
+
+    --         to-from : (f : A * B → X) → Δ X (A * B) (from f) == f
+    --         to-from f = {!!}
+
+    --         from-to : (x : X) → from (Δ X (A * B) x) == x
+    --         from-to x = {!is-equiv.g-f ω x!}
+
     postulate
 
       -- Right, this is a special case of the join adjunction ...
@@ -155,8 +190,8 @@ module stash.modalities.Orthogonality where
     _≻_ : Type i → Type i → Type _
     X ≻ A = (Y : Type i) → ⟦ A ⊥ Y ⟧ → ⟦ X ⊥ Y ⟧
 
-    ≻-emap : {X Y : Type i} {A : Type i} → X ≻ A → X ≃ Y → Y ≻ A
-    ≻-emap {X} {Y} {A} ω e Z o = orth-emap (ω Z o) e
+    equiv-preserves-≻-l : {X Y : Type i} {A : Type i} → X ≃ Y → X ≻ A → Y ≻ A
+    equiv-preserves-≻-l {X} {Y} {A} e ω Z o = equiv-preserves-orth-l e (ω Z o)
 
     ≻-trivial : (A : Type i) → (Lift ⊤) ≻ A
     ≻-trivial A X _ = Unit-orth X
@@ -180,8 +215,9 @@ module stash.modalities.Orthogonality where
     hp-kills-paths : (A : Type i) → is-hyper-prop A
       → (X : Type i) → X ≻ A
       → (x y : X) → (x == y) ≻ A
-    hp-kills-paths A hp X X≻A x y = ≻-emap (hp (Lift ⊤) X (λ _ → x) (≻-trivial A) X≻A y)
+    hp-kills-paths A hp X X≻A x y = equiv-preserves-≻-l
       (equiv snd (λ p → (_ , p)) (λ _ → idp) (λ _ → idp))
+      (hp (Lift ⊤) X (λ _ → x) (≻-trivial A) X≻A y)
 
     -- Okay, so in some sense this is much more natural.
     -- It just says the connected guys have to be closed under