open import 1Lab.Prelude

open import Data.Nat.Properties

open import Homotopy.Connectedness

module Homotopy.Connectedness.Automation where

AutomationπŸ”—

Just like for h-levels, we can leverage Agda’s instance search to make proving things about connected types easier. The only difference is that the offsetting goes the other way, since connectedness is downwards-closed.

record Connected {β„“} (T : Type β„“) (n : Nat) : Type β„“ where
  constructor conn-instance
  field
    has-n-connected : is-n-connected T n

n-connected : βˆ€ {β„“} {T : Type β„“} n ⦃ x : Connected T n ⦄ β†’ is-n-connected T n
n-connected n ⦃ c ⦄ = Connected.has-n-connected c

basic-conn-instance
  : βˆ€ {β„“} {T : Type β„“} n {k}
  β†’ is-n-connected T (n + k) β†’ Connected T n
basic-conn-instance {T = T} n {k} c = conn-instance (is-connected-+ n k
  (subst (is-n-connected T) (+-commutative n k) c))

connected : βˆ€ {β„“} {T : Type β„“} β†’ ⦃ Connected T 2 ⦄
  β†’ βˆ€ (a b : T) β†’ βˆ₯ a ≑ b βˆ₯
connected ⦃ conn-instance c ⦄ a b =
  n-connected-βˆ₯-βˆ₯.to 2 c .snd a b .fst

simply-connected : βˆ€ {β„“} {T : Type β„“} β†’ ⦃ Connected T 3 ⦄
  β†’ βˆ€ {a b : T} (p q : a ≑ b) β†’ βˆ₯ p ≑ q βˆ₯
simply-connected ⦃ conn-instance c ⦄ {a} {b} p q =
  n-connected-βˆ₯-βˆ₯.to 3 c .snd a b .snd p q .fst

is-contr→is-connected
  : βˆ€ {β„“} {A : Type β„“} β†’ is-contr A
  β†’ βˆ€ {n} β†’ is-n-connected-βˆ₯-βˆ₯ A n
is-contr→is-connected c {zero} = _
is-contr→is-connected c {suc n} .fst = inc (c .centre)
is-contr→is-connected c {suc n} .snd _ _ =
  is-contr→is-connected (Path-is-hlevel 0 c)

instance
  -- Note that this overlaps with other instances, but Agda doesn't mind
  -- because all instances of Connected A 0 are equal!
  0-Connected : βˆ€ {β„“} {A : Type β„“} β†’ Connected A 0
  0-Connected = _

  Connected-⊀ : βˆ€ {n} β†’ Connected ⊀ n
  Connected-⊀ {n} = conn-instance (n-connected-βˆ₯-βˆ₯.from n
    (is-contr→is-connected (hlevel 0)))

  Connected-Ξ£
    : βˆ€ {β„“ β„“'} {A : Type β„“} {B : A β†’ Type β„“'} {n}
    β†’ ⦃ Connected A n ⦄ β†’ ⦃ βˆ€ {a} β†’ Connected (B a) n ⦄
    β†’ Connected (Ξ£ A B) n
  Connected-Ξ£ {n = n} ⦃ conn-instance ac ⦄ ⦃ bc ⦄ = conn-instance
    (Ξ£-is-n-connected n ac Ξ» _ β†’ Connected.has-n-connected bc)

  Connected-Path
    : βˆ€ {β„“} {A : Type β„“} {x y : A} {n}
    β†’ ⦃ Connected A (suc n) ⦄
    β†’ Connected (Path A x y) n
  Connected-Path {n = n} ⦃ conn-instance ac ⦄ = conn-instance
    (Path-is-connected n ac)

  Connected-Lift
    : βˆ€ {β„“ β„“'} {A : Type β„“} {n}
    β†’ ⦃ Connected A n ⦄
    β†’ Connected (Lift β„“' A) n
  Connected-Lift {n = n} ⦃ conn-instance ac ⦄ = conn-instance
    (is-n-connected-≃ n (Lift-≃ e⁻¹) ac)