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 : Type β'} {n}
β β¦ Connected A n β¦ β β¦ Connected B n β¦
β Connected (A Γ B) n
Connected-Γ {n = n} β¦ conn-instance ac β¦ β¦ conn-instance bc β¦ = conn-instance
(Γ-is-n-connected n ac 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)