text:
module StateSizedIO.GUI.WxBindingsFFI where

open import Data.Bool.Base
open import Data.Integer
open import Data.Nat

open import Data.Product hiding (map)

open import NativeIO

{-# FOREIGN GHC import qualified GHC.Conc.Sync #-}
{-# FOREIGN GHC import qualified Control.Concurrent #-}
{-# FOREIGN GHC import qualified Data.IORef #-}

{-# FOREIGN GHC import qualified Graphics.UI.WX #-}
{-# FOREIGN GHC import qualified Graphics.UI.WX.Timer #-}
{-# FOREIGN GHC import qualified Graphics.UI.WXCore #-}
{-# FOREIGN GHC import qualified Graphics.UI.WXCore.Events #-}

postulate Frame : Set
{-# COMPILE GHC Frame = type (Graphics.UI.WX.Frame ()) #-}

postulate Button : Set
{-# COMPILE GHC Button = type (Graphics.UI.WX.Button ()) #-}

postulate TextCtrl : Set
{-# COMPILE GHC TextCtrl = type (Graphics.UI.WX.TextCtrl ()) #-}

postulate Timer : Set
{-# COMPILE GHC Timer = type Graphics.UI.WX.Timer.Timer #-}

postulate nativeNewFrame : String -> NativeIO Frame
{-# COMPILE GHC nativeNewFrame = (\s -> Graphics.UI.WX.frame [Graphics.UI.WX.text Graphics.UI.WX.:= "Window"]) #-}

--
-- Frame Layout
--
{-# FOREIGN GHC
setChildrenLayout' ::   Graphics.UI.WX.Frame () -> Integer -> Integer -> Integer -> Integer -> IO ()
setChildrenLayout' win rowWidth' marginWidth' vspa' hspa' = do

  let rowWidth = fromIntegral rowWidth'
  let marginWidth = fromIntegral marginWidth'
  let vspa = fromIntegral vspa'
  let hspa = fromIntegral hspa'

  let list2Matrix n xs = map (\(x ,y)-> (take n) $ (drop (n*x)) y) $ zip [0..] $ replicate (div (length xs)  n) xs

  blist <- Graphics.UI.WXCore.windowChildren win
  putStrLn ("Layout of frame, got " ++ (show $ length $ blist) ++ "children")

  let  blist' = list2Matrix rowWidth blist
  let  blist'' = (map . map) Graphics.UI.WX.widget blist'

  Graphics.UI.WX.set win [ Graphics.UI.WX.layout Graphics.UI.WX.:= Graphics.UI.WX.margin marginWidth $ Graphics.UI.WX.dynamic $ Graphics.UI.WX.grid vspa hspa $ blist'']

#-}

postulate nativeSetChildredLayout : Frame → ℕ → ℕ → ℕ → ℕ → NativeIO Unit
{-# COMPILE GHC nativeSetChildredLayout = setChildrenLayout' #-}

postulate nativeDoThreadDelay : NativeIO Bool
{-# COMPILE GHC nativeDoThreadDelay = ((Control.Concurrent.threadDelay 100) >>= (\x -> return True)) #-}

postulate nativeSetIdle : Frame -> NativeIO Bool -> NativeIO Unit
{-# COMPILE GHC nativeSetIdle = (\fra prog -> Graphics.UI.WX.set fra [Graphics.UI.WX.on Graphics.UI.WX.idle Graphics.UI.WX.:= prog]) #-}

nativeCreateFrame : NativeIO Frame
nativeCreateFrame =
  nativeNewFrame "Start Text" native>>= (\f ->
  nativeSetIdle f nativeDoThreadDelay native>>= (\x ->
  nativeReturn f))

postulate nativeMakeButton : Frame → String → NativeIO Button
{-# COMPILE GHC nativeMakeButton = (\myFrame str -> Graphics.UI.WX.button myFrame [Graphics.UI.WX.text Graphics.UI.WX.:= (Data.Text.unpack str)]) #-}

postulate nativeMakeTextCtrl : Frame  → String → NativeIO TextCtrl
{-# COMPILE GHC nativeMakeTextCtrl = (\myFrame str -> Graphics.UI.WX.entry myFrame [Graphics.UI.WX.text Graphics.UI.WX.:= (Data.Text.unpack str)]) #-}

postulate nativeAddButton : Frame → Button → NativeIO Unit
{-# COMPILE GHC nativeAddButton = (\myFrame bt -> Graphics.UI.WX.set myFrame [Graphics.UI.WX.layout Graphics.UI.WX.:= Graphics.UI.WX.minsize (Graphics.UI.WX.sz 500 400) $ Graphics.UI.WX.column 1 [Graphics.UI.WX.hfill (Graphics.UI.WX.widget bt)]]) #-}

postulate WxColor : Set
{-# COMPILE GHC WxColor = type Graphics.UI.WX.Color #-}

postulate nativeSetColorButton : Button → WxColor → NativeIO Unit
{-# COMPILE GHC  nativeSetColorButton = (\ bt co -> Graphics.UI.WX.set bt [ Graphics.UI.WX.color Graphics.UI.WX.:= co] ) #-}

postulate nativeSetColorTextCtrl : TextCtrl → WxColor → NativeIO Unit
{-# COMPILE GHC  nativeSetColorTextCtrl = (\ txt co -> Graphics.UI.WX.set txt [ Graphics.UI.WX.color Graphics.UI.WX.:= co] ) #-}

postulate rgb : ℕ → ℕ → ℕ → WxColor
{-# COMPILE GHC rgb = (\ r b g -> Graphics.UI.WX.rgb r g b) #-}

postulate  TVar : Set → Set
{-# COMPILE GHC TVar = type Control.Concurrent.STM.TVar.TVar #-}

postulate  MVar : Set → Set
{-# COMPILE GHC MVar = type Control.Concurrent.MVar #-}

Var : Set → Set
Var = MVar

postulate
  nativeNewVar : {A : Set} → A → NativeIO (Var A)
  nativeTakeVar : {A : Set} → Var A → NativeIO A
  nativePutVar : {A : Set} → Var A → A → NativeIO Unit

{-# COMPILE GHC nativeNewVar = (\ _ -> Control.Concurrent.newMVar ) #-}
{-# COMPILE GHC nativeTakeVar = (\ _ -> Control.Concurrent.takeMVar ) #-}
{-# COMPILE GHC nativePutVar = (\ _ -> Control.Concurrent.putMVar ) #-}

-- Fire Custom Event
--
postulate nativeFireCustomEvent : Frame → NativeIO Unit
{-# COMPILE GHC nativeFireCustomEvent = (\f -> Graphics.UI.WXCore.commandEventCreate Graphics.UI.WXCore.wxEVT_COMMAND_MENU_SELECTED (Graphics.UI.WXCore.wxID_HIGHEST+1) >>= (\ev -> fmap (\x -> ()) (Graphics.UI.WXCore.evtHandlerProcessEvent f ev))) #-}

postulate nativeRegisterCustomEvent : Frame → NativeIO Unit → NativeIO Unit
{-# COMPILE GHC nativeRegisterCustomEvent = (\win prog -> Graphics.UI.WXCore.evtHandlerOnMenuCommand win (Graphics.UI.WXCore.wxID_HIGHEST+1) (putStrLn " >>> CUSTOM EVENT FIRED <<<" >> Control.Concurrent.forkIO prog >> return ())) #-}

{-
for debugging
postulate nativeRegisterDummyCustomEvent : Frame → NativeIO Unit
{-# COMPILE GHC nativeRegisterDummyCustomEvent = (\win -> Graphics.UI.WXCore.evtHandlerOnMenuCommand win (Graphics.UI.WXCore.wxID_HIGHEST+1) (putStrLn " >>> CUSTOM EVENT FIRED <<<")) #-}
-}

postulate nativeSetButtonHandler : Button → NativeIO Unit → NativeIO Unit
{-# COMPILE GHC nativeSetButtonHandler = (\ bt prog -> Graphics.UI.WX.set bt [Graphics.UI.WX.on Graphics.UI.WX.command Graphics.UI.WX.:= prog ]) #-}

postulate prog : NativeIO Unit
{-# COMPILE GHC prog = (putStrLn "timer goes off!") #-}

postulate nativeSetTimer : Frame → ℤ → NativeIO Unit → NativeIO Timer
{-# COMPILE GHC nativeSetTimer = (\ fra x prog -> Graphics.UI.WX.timer fra [ Graphics.UI.WX.interval Graphics.UI.WX.:= (fromInteger x) , Graphics.UI.WX.on Graphics.UI.WX.command Graphics.UI.WX.:= prog ]) #-}

postulate ThreadId : Set
{-# COMPILE GHC ThreadId = type GHC.Conc.Sync.ThreadId #-}

postulate forkIO : NativeIO Unit → NativeIO ThreadId
{-# COMPILE GHC forkIO = GHC.Conc.Sync.forkIO #-}

postulate Bitmap : Set
{-# COMPILE GHC Bitmap = type (Graphics.UI.WXCore.Bitmap ())  #-}

postulate bitmap : String → Bitmap
{-# COMPILE GHC bitmap = (\s -> Graphics.UI.WX.bitmap (Data.Text.unpack s)) #-}

postulate DC : Set
{-# COMPILE GHC DC = type (Graphics.UI.WXCore.DC ()) #-}

postulate Rect : Set
{-# COMPILE GHC Rect = type Graphics.UI.WXCore.Rect #-}

postulate nativeSetClickRight : Frame  → NativeIO Unit → NativeIO Unit
{-# COMPILE GHC nativeSetClickRight = (\ fra prog -> Graphics.UI.WX.set fra [Graphics.UI.WX.on Graphics.UI.WX.clickRight Graphics.UI.WX.:= (\x -> prog)]) #-}

postulate nativeSetOnPaint : Frame → (DC → Rect → NativeIO Unit) → NativeIO Unit
{-# COMPILE GHC nativeSetOnPaint = (\ fra prog -> Graphics.UI.WX.set fra [Graphics.UI.WX.on Graphics.UI.WX.paint Graphics.UI.WX.:= prog]) #-}

postulate nativeRepaint : Frame → NativeIO Unit
{-# COMPILE GHC nativeRepaint = Graphics.UI.WX.repaint #-}

Point : Set
Point = (ℤ × ℤ)

postulate NativePoint : Set
{-# COMPILE GHC NativePoint = type Graphics.UI.WXCore.Point #-}

postulate nativePoint : ℤ → ℤ → NativePoint
{-# COMPILE GHC nativePoint = (\ x y -> Graphics.UI.WXCore.point (fromInteger x) (fromInteger y)) #-}

postulate nativeDrawBitmapNativePoint : DC → Bitmap → NativePoint → Bool → NativeIO Unit
{-# COMPILE GHC nativeDrawBitmapNativePoint = (\ d bi p bo -> Graphics.UI.WX.drawBitmap d bi p bo [] ) #-}

nativeDrawBitmap : DC → Bitmap → Point → Bool → NativeIO Unit
nativeDrawBitmap d bi (x , y) bo = nativeDrawBitmapNativePoint d bi (nativePoint x y) bo

{-# FOREIGN GHC import Graphics.UI.WXCore.WxcClassesAL #-}

postulate nativeBitmapGetWidth : Bitmap → NativeIO ℤ
{-# COMPILE GHC nativeBitmapGetWidth = (\ b -> fmap fromIntegral (Graphics.UI.WXCore.WxcClassesAL.bitmapGetWidth b)) #-}

postulate start : NativeIO Unit → NativeIO Unit
{-# COMPILE GHC start = Graphics.UI.WX.start #-}

--
--  Note: we add the "key pressed" event to a button
--  and not to a frame, because of a bug in wxHaskell that prevents
--  adding a key pressed event to a frame (at least on linux plattforms).
--

postulate
  Key : Set
  showKey : Key -> String
  nativeSetKeyHandler : Button → (Key → NativeIO Unit) → NativeIO Unit

{-# COMPILE GHC Key = type Graphics.UI.WXCore.Events.Key #-}
{-# COMPILE GHC showKey = (\ k -> (Data.Text.pack (Graphics.UI.WXCore.Events.showKey k))) #-}

{-# COMPILE GHC nativeSetKeyHandler = (\bt prog -> Graphics.UI.WX.set bt [Graphics.UI.WX.on Graphics.UI.WX.anyKey Graphics.UI.WX.:= prog]) #-}

--
-- Delete Objects
--

-- note: can be solved with instance arguments in the future
postulate objectDeleteFrame : Frame → NativeIO Unit
{-# COMPILE GHC objectDeleteFrame = (\f -> Graphics.UI.WX.objectDelete f) #-}

postulate nativeDeleteButton : Button → NativeIO Unit
{-# COMPILE GHC nativeDeleteButton = (\f -> Graphics.UI.WX.objectDelete f) #-}

postulate nativeDeleteTextCtrl : TextCtrl → NativeIO Unit
{-# COMPILE GHC nativeDeleteTextCtrl = (\f -> Graphics.UI.WX.objectDelete f) #-}

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
{-# OPTIONS --type-in-type #-}

module BialgebraSorting where

import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Function
open import Data.Product using (Σ; _,_; proj₁; proj₂)

record Functor (F : Set → Set) : Set where
  field
    map  : {A B : Set} → (A → B) → F A → F B
    map-∘ : {A B C : Set} {f : A → B} {g : B → C} → map g ∘ map f ≡ map (g ∘ f)
    map-id : {A : Set} → map (id {A = A}) ≡ id

postulate
  extensionality : {S : Set}{T : S -> Set}
                  {f g : (x : S) -> T x} ->
                  ((x : S) -> f x ≡ g x) ->
                  f ≡ g

record InitialAlgebra {F : Set → Set} (F-Functor : Functor F) : Set where
  open Functor F-Functor
  field
    Mu : Set
    In : F Mu → Mu
    inᵒ : Mu → F Mu
    In-inᵒ : In ∘ inᵒ ≡ id
    inᵒ-In : inᵒ ∘ In ≡ id
    fold
        : {A : Set} (f : F A → A)
        → Mu
        → A
    fold-∘
        : {A : Set} (f : F A → A)
        → (x : F Mu)
        → fold f (In x) ≡ f (map (fold f) x)
    fold-unique
        : {A : Set} {f : F A → A}
        → (h : Mu → A)
        → ((y : F Mu) → h (In y) ≡ f (map h y))
        → (x : Mu)
        → h x ≡ fold f x

record TerminalCoalgebra {F : Set → Set} (F-Functor : Functor F) : Set where
  open Functor F-Functor
  field
    Nu : Set
    Out : Nu → F Nu
    outᵒ : F Nu → Nu
    Out-outᵒ : Out ∘ outᵒ ≡ id
    outᵒ-Out : outᵒ ∘ Out ≡ id
    unfold : {A : Set} → (A → F A) → A → Nu
    unfold-∘
        : {A : Set} (f : A → F A)
        → (x : A)
        → Out (unfold f x) ≡ map (unfold f) (f x)
    unfold-unique
        : {A : Set} {f : A → F A}
        → (h : A → Nu)
        → ((y : A) → Out (unfold f y) ≡ map (unfold f) (f y))
        → (x : A)
        → h x ≡ unfold f x

module Example {F : Set → Set} {F-Functor : Functor F} (alg : InitialAlgebra F-Functor) where
  open Functor F-Functor
  open InitialAlgebra alg

  {-# TERMINATING #-}
  in-is-in
      : inᵒ ≡ fold (map In)
  in-is-in = extensionality $ \ x →
    let f = map In in
    begin
      inᵒ x
    ≡⟨⟩
      id (inᵒ x)
    ≡⟨ cong (_$ inᵒ x) $ sym map-id ⟩
      map id (inᵒ x)
    ≡⟨ cong (\p → map p (inᵒ x)) $ sym In-inᵒ ⟩
      map (In ∘ inᵒ) (inᵒ x)
    ≡⟨ cong (_$ inᵒ x) $ sym map-∘ ⟩
      map In (map inᵒ (inᵒ x))
    ≡⟨ cong (\p → map In ((map p) (inᵒ x))) in-is-in ⟩
      map In (map (fold (map In)) (inᵒ x))
    ≡⟨⟩
      map In (map (fold f) (inᵒ x))
    ≡⟨⟩
      f (map (fold f) (inᵒ x))
    ≡⟨ sym $ fold-∘ f (inᵒ x) ⟩
      fold f (In (inᵒ x))
    ≡⟨ cong (\p → fold f (p x)) In-inᵒ ⟩
      fold f x
    ≡⟨⟩
      fold (map In) x
    ∎

module Paper
    {F : Set → Set}
    {F-Functor : Functor F}
    (alg : InitialAlgebra F-Functor)
    (coalg : TerminalCoalgebra F-Functor) where
  open Functor F-Functor public
  open InitialAlgebra alg public
  open TerminalCoalgebra coalg public

  {-# TERMINATING #-}
  downcast : Nu → Mu
  downcast = In ∘ map downcast ∘ Out

  upcast : Mu → Nu
  upcast = fold outᵒ

data List (A : Set) (K : Set) : Set where
  Nil : List A K
  Cons : A → K → List A K

data Ordering : Set where
  LT : Ordering
  EQ : Ordering
  GT : Ordering

record Ord (A : Set) : Set where
  field
    compare : A → A → Ordering

data Bool : Set where
  false : Bool
  true  : Bool

_&&_ : Bool → Bool → Bool
false && _ = false
true && b = b

not : Bool → Bool
not false = true
not true = false

_==_ : Ordering → Ordering → Bool
_==_ EQ EQ = true
_==_ LT LT = true
_==_ GT GT = true
_==_ _ _ = false

_!=_ : Ordering → Ordering → Bool
_!=_ a b = not (a == b)

data Maybe (A : Set) : Set where
  just : A → Maybe A
  nothing : Maybe A

module Paper₂
    {A : Set}
    (Ord-A : Ord A)
    (List-Functor : Functor (List A))
    (alg : InitialAlgebra List-Functor)
    (coalg : TerminalCoalgebra List-Functor) where
  open Paper alg coalg
  open Ord Ord-A public

  is-sorted : Nu → Bool
  is-sorted = proj₂ ∘ fold (\ { Nil → nothing , true
                              ; (Cons a (nothing , x)) → just a , x
                              ; (Cons a (just a' , x)) → just a' , (x && (compare a a' != GT))
                              } ) ∘ downcast

  -- SortedList : {A : Set} → Ord A → Set
  -- SortedList ord = Σ Nu is-sorted

open Functor

record Bialgebra
       {F G : Set → Set}
       {F-functor : Functor F}
       {G-functor : Functor G}
       (f : {X : Set} → F (G X) → G (F X)) : Set where
  field
    a : {X : Set} → F X → X
    c : {X : Set} → X → G X
    bialgebra-proof
      : {X : Set}
      → c {X} ∘ a ≡ map G-functor a ∘ f ∘ map F-functor c

bubbleSort : Bialgebra ?
bubbleSort = ?

ext: agda

max_stars_repo_name: dominiquedevriese/reviews

max_issues_repo_name: dominiquedevriese/reviews

max_forks_repo_name: dominiquedevriese/reviews


text:
------------------------------------------------------------------------------
-- Testing the use of various options using only an OPTIONS pragma
------------------------------------------------------------------------------

{-# OPTIONS --exact-split
            --no-sized-types
            --no-universe-polymorphism
            --without-K
#-}

-- (24 January 2014) From the Agda implementation, the above list of
-- options is saved in the interface file as an one element list,
-- where the element is a list of the three options.

module OptionsLList where

postulate
  D : Set
  ∃ : (A : D → Set) → Set

postulate foo : (A : D → Set) → ∃ A → ∃ A
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
------------------------------------------------------------------------
-- The All predicate, defined using _∈_
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Equality

module List.All {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bag-equivalence eq
open import Bijection eq as Bijection using (_↔_)
import Equality.Groupoid eq as EG
open import Function-universe eq as F hiding (id; _∘_)
open import Groupoid eq
open import H-level eq
open import H-level.Closure eq
open import List eq as L using (_++_)
open import Monad eq hiding (map)
open import Vec.Function eq as Vec using (Vec)

private
  variable
    a b ℓ p q : Level
    A B       : Type a
    P         : A → Type p
    Q         : A → Type q
    k x y     : A
    n         : ℕ
    xs ys     : List A

-- All P xs means that P holds for every element of xs.

All : {A : Type a} → (A → Type p) → List A → Type (a ⊔ p)
All P xs = ∀ x → x ∈ xs → P x

-- The type xs ⊆ ys means that every element of xs is also an element
-- of ys.

infix 4 _⊆_

_⊆_ : {A : Type a} → List A → List A → Type a
xs ⊆ ys = All (_∈ ys) xs

-- The _⊆_ relation matches _∼[ implication ]_.

⊆↔∼[implication] : xs ⊆ ys ↔ xs ∼[ implication ] ys
⊆↔∼[implication] {xs = xs} {ys = ys} =
  xs ⊆ ys                  ↔⟨⟩
  All (_∈ ys) xs           ↔⟨⟩
  (∀ x → x ∈ xs → x ∈ ys)  ↔⟨⟩
  xs ∼[ implication ] ys   □

-- Some rearrangement lemmas.

All-[] :
  ∀ {k} {A : Type a} (P : A → Type p) →
  Extensionality? k a (a ⊔ p) →
  All P [] ↝[ k ] ⊤
All-[] {a = a} {k = k} {A} P ext =
  All P []              ↔⟨⟩
  (∀ y → y ∈ [] → P y)  ↔⟨⟩
  (∀ y → ⊥ → P y)       ↝⟨ (∀-cong ext λ _ → Π⊥↔⊤ (lower-extensionality? k a a ext)) ⟩
  (A → ⊤)               ↔⟨ →-right-zero ⟩□
  ⊤                     □

module _ {k} {A : Type a} {P : A → Type p}
         (ext : Extensionality? k a (a ⊔ p)) where

  private
    ext′ : Extensionality? k a p
    ext′ = lower-extensionality? k a a ext

  All-∷ : All P (x ∷ xs) ↝[ k ] P x × All P xs
  All-∷ {x = x} {xs = xs} =
    All P (x ∷ xs)                              ↔⟨⟩
    (∀ y → y ∈ x ∷ xs → P y)                    ↔⟨⟩
    (∀ y → y ≡ x ⊎ y ∈ xs → P y)                ↝⟨ ∀-cong ext (λ _ → Π⊎↔Π×Π ext′) ⟩
    (∀ y → (y ≡ x → P y) × (y ∈ xs → P y))      ↔⟨ ΠΣ-comm ⟩
    (∀ y → y ≡ x → P y) × (∀ y → y ∈ xs → P y)  ↝⟨ (×-cong₁ λ _ → ∀-cong ext λ _ → →-cong₁ ext′ ≡-comm) ⟩
    (∀ y → x ≡ y → P y) × (∀ y → y ∈ xs → P y)  ↝⟨ inverse-ext? (λ ext → ∀-intro _ ext) ext ×-cong F.id ⟩□
    P x × All P xs                              □

  All-++ : All P (xs ++ ys) ↝[ k ] All P xs × All P ys
  All-++ {xs = xs} {ys = ys} =
    All P (xs ++ ys)                             ↔⟨⟩
    (∀ x → x ∈ xs ++ ys → P x)                   ↝⟨ (∀-cong ext λ _ → →-cong₁ ext′ (Any-++ _ _ _)) ⟩
    (∀ x → x ∈ xs ⊎ x ∈ ys → P x)                ↝⟨ (∀-cong ext λ _ → Π⊎↔Π×Π ext′) ⟩
    (∀ x → (x ∈ xs → P x) × (x ∈ ys → P x))      ↔⟨ ΠΣ-comm ⟩
    (∀ x → x ∈ xs → P x) × (∀ x → x ∈ ys → P x)  ↔⟨⟩
    All P xs × All P ys                          □

  All-concat : All P (L.concat xs) ↝[ k ] All (All P) xs
  All-concat {xs = xss} =
    (∀ x → x ∈ L.concat xss → P x)              ↝⟨ ∀-cong ext (λ _ → →-cong₁ ext′ (Any-concat _ _)) ⟩
    (∀ x → Any (x ∈_) xss → P x)                ↝⟨ ∀-cong ext (λ _ → →-cong₁ ext′ (Any-∈ _ _)) ⟩
    (∀ x → (∃ λ xs → x ∈ xs × xs ∈ xss) → P x)  ↝⟨ ∀-cong ext (λ _ → from-bijection currying) ⟩
    (∀ x → ∀ xs → x ∈ xs × xs ∈ xss → P x)      ↔⟨ Π-comm ⟩
    (∀ xs → ∀ x → x ∈ xs × xs ∈ xss → P x)      ↝⟨ ∀-cong ext (λ _ → ∀-cong ext λ _ → from-bijection currying) ⟩
    (∀ xs → ∀ x → x ∈ xs → xs ∈ xss → P x)      ↝⟨ ∀-cong ext (λ _ → ∀-cong ext λ _ → from-bijection Π-comm) ⟩
    (∀ xs → ∀ x → xs ∈ xss → x ∈ xs → P x)      ↝⟨ ∀-cong ext (λ _ → from-bijection Π-comm) ⟩□
    (∀ xs → xs ∈ xss → ∀ x → x ∈ xs → P x)      □

All-map :
  ∀ {k} {A : Type a} {B : Type b} {P : B → Type p}
    {f : A → B} {xs : List A} →
  (ext : Extensionality? k (a ⊔ b) (a ⊔ b ⊔ p)) →
  All P (L.map f xs) ↝[ k ] All (P ∘ f) xs
All-map {a = a} {b = b} {p = p} {k = k} {P = P} {f} {xs} ext =
  (∀ x → x ∈ L.map f xs → P x)              ↝⟨ (∀-cong ext₁ λ _ → →-cong₁ ext₂ (Any-map _ _ _)) ⟩
  (∀ x → Any (λ y → x ≡ f y) xs → P x)      ↝⟨ (∀-cong ext₃ λ _ → →-cong₁ ext₄ (Any-∈ _ _)) ⟩
  (∀ x → (∃ λ y → x ≡ f y × y ∈ xs) → P x)  ↝⟨ (∀-cong ext₃ λ _ → from-bijection currying) ⟩
  (∀ x → ∀ y → x ≡ f y × y ∈ xs → P x)      ↝⟨ (∀-cong ext₃ λ _ → ∀-cong ext₅ λ _ → from-bijection currying) ⟩
  (∀ x → ∀ y → x ≡ f y → y ∈ xs → P x)      ↔⟨ Π-comm ⟩
  (∀ x → ∀ y → y ≡ f x → x ∈ xs → P y)      ↝⟨ (∀-cong ext₅ λ _ → ∀-cong ext₃ λ _ → →-cong₁ ext₆ ≡-comm) ⟩
  (∀ x → ∀ y → f x ≡ y → x ∈ xs → P y)      ↝⟨ (∀-cong ext₅ λ _ → inverse-ext? (λ ext → ∀-intro _ ext) ext₃) ⟩□
  (∀ x → x ∈ xs → P (f x))                  □
  where
  ext₁ = lower-extensionality? k a     a       ext
  ext₂ = lower-extensionality? k a     (a ⊔ b) ext
  ext₃ = lower-extensionality? k a     lzero   ext
  ext₄ = lower-extensionality? k lzero (a ⊔ b) ext
  ext₅ = lower-extensionality? k b     lzero   ext
  ext₆ = lower-extensionality? k a     b       ext

All->>= :
  ∀ {k} {A B : Type ℓ} {P : B → Type p} {f : A → List B} {xs : List A} →
  (ext : Extensionality? k ℓ (ℓ ⊔ p)) →
  All P (xs >>= f) ↝[ k ] All (All P ∘ f) xs
All->>= {P = P} {f = f} {xs = xs} ext =
  All P (L.concat (L.map f xs))  ↝⟨ All-concat ext ⟩
  All (All P) (L.map f xs)       ↝⟨ All-map ext ⟩□
  All (All P ∘ f) xs             □

All-const :
  {A : Type a} {B : Type b} {xs : List B} →
  Extensionality? k b a →
  All (const A) xs ↝[ k ] Vec A (L.length xs)
All-const {A = A} {xs = xs} ext =
  (∀ x → x ∈ xs → A)       ↔⟨ inverse currying ⟩
  (∃ (_∈ xs) → A)          ↝⟨ →-cong₁ ext (Fin-length _) ⟩□
  (Fin (L.length xs) → A)  □

private

  -- The following lemma that relates All-const and Fin-length holds
  -- by definition.

  All-const-Fin-length :
    ∀ {xs : List A} {bs : All (const B) xs} {i} →
    All-const _ bs i ≡
    uncurry bs (_↔_.from (Fin-length xs) i)
  All-const-Fin-length = refl _

All-const-replicate :
  {A : Type a} →
  Extensionality? k lzero a →
  All (const A) (L.replicate n tt) ↝[ k ] Vec A n
All-const-replicate {n = n} {A = A} ext =
  All (const A) (L.replicate n tt)     ↝⟨ All-const ext ⟩
  Vec A (L.length (L.replicate n tt))  ↝⟨ →-cong₁ ext $ ≡⇒↝ bijection $ cong Fin (L.length-replicate _) ⟩□
  Vec A n                              □

All-Σ :
  {A : Type a} {P : A → Type p} {Q : ∀ x → P x → Type q} {xs : List A} →
  Extensionality? k a (a ⊔ p ⊔ q) →
  All (λ x → Σ (P x) (Q x)) xs ↝[ k ]
  ∃ λ (ps : All P xs) → ∀ x (x∈xs : x ∈ xs) → Q x (ps x x∈xs)
All-Σ {P = P} {Q = Q} {xs = xs} ext =
  All (λ x → Σ (P x) (Q x)) xs                                   ↔⟨⟩

  (∀ x → x ∈ xs → Σ (P x) (Q x))                                 ↝⟨ (∀-cong ext λ _ → from-isomorphism ΠΣ-comm) ⟩

  (∀ x → ∃ λ (ps : x ∈ xs → P x) →
     (x∈xs : x ∈ xs) → Q x (ps x∈xs))                            ↔⟨ ΠΣ-comm ⟩

  (∃ λ (ps : ∀ x → x ∈ xs → P x) →
     ∀ x (x∈xs : x ∈ xs) → Q x (ps x x∈xs))                      ↔⟨⟩

  (∃ λ (ps : All P xs) → ∀ x (x∈xs : x ∈ xs) → Q x (ps x x∈xs))  □

-- Some abbreviations.

nil : All P []
nil {P = P} = _⇔_.from (All-[] P _) _

cons : P x → All P xs → All P (x ∷ xs)
cons = curry (_⇔_.from (All-∷ _))

head : All P (x ∷ xs) → P x
head = proj₁ ∘ _⇔_.to (All-∷ _)

tail : All P (x ∷ xs) → All P xs
tail = proj₂ ∘ _⇔_.to (All-∷ _)

append : All P xs → All P ys → All P (xs ++ ys)
append = curry (_⇔_.from (All-++ _))

-- All preserves h-levels (assuming extensionality).

H-level-All :
  {A : Type a} {P : A → Type p} →
  Extensionality a (a ⊔ p) →
  ∀ n →
  (∀ x → H-level n (P x)) →
  (∀ xs → H-level n (All P xs))
H-level-All {a = a} ext n h xs =
  Π-closure ext n λ _ →
  Π-closure (lower-extensionality a a ext) n λ _ →
  h _

-- Some lemmas related to append.

append-Any-++-inj₁ :
  ∀ {xs ys} {ps : All P xs} {qs : All P ys}
  (x∈xs : x ∈ xs) →
  append ps qs _ (_↔_.from (Any-++ _ _ _) (inj₁ x∈xs)) ≡
  ps _ x∈xs
append-Any-++-inj₁ {P = P} {x = x} {ps = ps} {qs} x∈xs =
  append ps qs _ (_↔_.from (Any-++ _ _ _) (inj₁ x∈xs))       ≡⟨⟩

  [ ps _ , qs _ ] (_↔_.to (Any-++ _ _ _)
                     (_↔_.from (Any-++ _ _ _) (inj₁ x∈xs)))  ≡⟨ cong [ ps _ , qs _ ] (_↔_.right-inverse-of (Any-++ _ _ _) _) ⟩

  [_,_] {C = λ _ → P x} (ps _) (qs _) (inj₁ x∈xs)            ≡⟨⟩

  ps _ x∈xs                                                  ∎

append-Any-++-inj₂ :
  ∀ xs {ys} {ps : All P xs} {qs : All P ys} {y∈ys : y ∈ ys} →
  append ps qs _ (_↔_.from (Any-++ _ xs _) (inj₂ y∈ys)) ≡
  qs _ y∈ys
append-Any-++-inj₂ {P = P} {y = y} xs {ps = ps} {qs} {y∈ys} =
  append ps qs _ (_↔_.from (Any-++ _ xs _) (inj₂ y∈ys))       ≡⟨⟩

  [ ps _ , qs _ ] (_↔_.to (Any-++ _ _ _)
                     (_↔_.from (Any-++ _ xs _) (inj₂ y∈ys)))  ≡⟨ cong [ ps _ , qs _ ] (_↔_.right-inverse-of (Any-++ _ _ _) _) ⟩

  [_,_] {C = λ _ → P y} (ps _) (qs _) (inj₂ y∈ys)             ≡⟨⟩

  qs _ y∈ys                                                   ∎

-- Some congruence lemmas.

All-cong :
  ∀ {k} {A : Type a} {P : A → Type p} {Q : A → Type q} {xs ys} →
  Extensionality? ⌊ k ⌋-sym a (a ⊔ p ⊔ q) →
  (∀ x → P x ↝[ ⌊ k ⌋-sym ] Q x) →
  xs ∼[ ⌊ k ⌋-sym ] ys →
  All P xs ↝[ ⌊ k ⌋-sym ] All Q ys
All-cong {a = a} {k = k} {P = P} {Q} {xs} {ys} ext P↝Q xs∼ys =
  All P xs              ↔⟨⟩
  (∀ x → x ∈ xs → P x)  ↝⟨ ∀-cong ext (λ _ → →-cong (lower-extensionality? ⌊ k ⌋-sym a a ext) (xs∼ys _) (P↝Q _)) ⟩
  (∀ x → x ∈ ys → Q x)  ↔⟨⟩
  All Q ys              □

All-cong-→ :
  (∀ x → P x → Q x) →
  ys ∼[ implication ] xs →
  All P xs → All Q ys
All-cong-→ {P = P} {Q = Q} {ys = ys} {xs = xs} P→Q ys∼xs =
  All P xs              ↔⟨⟩
  (∀ x → x ∈ xs → P x)  ↝⟨ ∀-cong _ (λ _ → →-cong-→ (ys∼xs _) (P→Q _)) ⟩
  (∀ x → x ∈ ys → Q x)  ↔⟨⟩
  All Q ys              □

map : (∀ x → P x → Q x) → ys ⊆ xs → All P xs → All Q ys
map P→Q ys∼xs = All-cong-→ P→Q ys∼xs

map₁ : (∀ x → P x → Q x) → All P xs → All Q xs
map₁ P→Q = map P→Q (λ _ → id)

map₂ : ys ⊆ xs → All P xs → All P ys
map₂ ys⊆xs = map (λ _ → id) ys⊆xs

private

  map₁-∘ :
    ∀ {P : A → Type p} {xs} {f : ∀ x → P x → Q x} {ps : All P xs} →
    map₁ f ps ≡ λ _ → f _ ∘ ps _
  map₁-∘ = refl _

  map₂-∘ :
    ∀ {xs ys} {ys⊆xs : ys ⊆ xs} {ps : All P xs} →
    map₂ ys⊆xs ps ≡ λ _ → ps _ ∘ ys⊆xs _
  map₂-∘ = refl _

-- Some properties that hold by definition.

map₂∘map₂ :
  ∀ {xs ys zs} {xs⊆ys : xs ⊆ ys} {ys⊆zs : ys ⊆ zs} {ps : All P zs} →
  map₂ xs⊆ys (map₂ ys⊆zs ps) ≡ map₂ (map₁ ys⊆zs xs⊆ys) ps
map₂∘map₂ = refl _

map₂-inj₂-∘ :
  ∀ {xs ys} {f : ys ⊆ xs} {p : P x} {ps : All P xs} →
  map₂ (λ _ → inj₂ ∘ f _) (cons p ps) ≡ map₂ f ps
map₂-inj₂-∘ = refl _

map₂-id :
  ∀ {xs} {ps : All P xs} →
  map₂ (λ _ → id) ps ≡ ps
map₂-id = refl _

map₂-inj₂ :
  ∀ {xs} {p : P x} {ps : All P xs} →
  map₂ (λ _ → inj₂) (cons p ps) ≡ ps
map₂-inj₂ = refl _

-- Some rearrangement lemmas for map₂.

map₂-⊎-map-id :
  {A : Type a} {P : A → Type p} →
  Extensionality a (a ⊔ p) →
  ∀ {x xs ys} {f : ys ⊆ xs} {p : P x} {ps : All P xs} →
  map₂ (λ _ → ⊎-map id (f _)) (cons p ps) ≡ cons p (map₂ f ps)
map₂-⊎-map-id {a = a} ext {f = f} {p} {ps} =
  apply-ext ext λ _ →
  apply-ext (lower-extensionality lzero a ext)
    [ (λ _ → refl _) , (λ _ → refl _) ]

map₂-⊎-map-id-inj₂ :
  {A : Type a} {P : A → Type p} →
  Extensionality a (a ⊔ p) →
  ∀ {x y xs} {p : P x} {q : P y} {ps : All P xs} →
  map₂ (λ _ → ⊎-map id inj₂) (cons p (cons q ps)) ≡ cons p ps
map₂-⊎-map-id-inj₂ ext {p = p} {q} {ps} =
  map₂ (λ _ → ⊎-map id inj₂) (cons p (cons q ps))  ≡⟨ map₂-⊎-map-id ext ⟩
  cons p (map₂ (λ _ → inj₂) (cons q ps))           ≡⟨⟩
  cons p ps                                        ∎

map₂-++-cong :
  {A : Type a} {P : A → Type p} →
  Extensionality a (a ⊔ p) →
  ∀ xs₁ {ys₁ xs₂ ys₂} {ps : All P xs₂} {qs : All P ys₂}
  {f : xs₁ ⊆ xs₂} {g : ys₁ ⊆ ys₂} →
  map₂ (++-cong f g) (append ps qs) ≡
  append (map₂ f ps) (map₂ g qs)
map₂-++-cong {a = a} ext _ {ps = ps} {qs} {f} {g} =
  apply-ext ext λ _ →
  apply-ext (lower-extensionality lzero a ext) λ x∈ →

    let lemma : ∀ x → [ ps _ , qs _ ] (⊎-map (f _) (g _) x) ≡
                      [ ps _ ∘ f _ , qs _ ∘ g _ ] x
        lemma = [ (λ _ → refl _) , (λ _ → refl _) ]
    in

    [ ps _ , qs _ ] (_↔_.to (Any-++ _ _ _) (_↔_.from (Any-++ _ _ _)
                       (⊎-map (f _) (g _) (_↔_.to (Any-++ _ _ _) x∈))))  ≡⟨ cong [ ps _ , qs _ ] (_↔_.right-inverse-of (Any-++ _ _ _) _) ⟩

    [ ps _ , qs _ ] (⊎-map (f _) (g _) (_↔_.to (Any-++ _ _ _) x∈))       ≡⟨ lemma (_↔_.to (Any-++ _ _ _) x∈) ⟩∎

    [ ps _ ∘ f _ , qs _ ∘ g _ ] (_↔_.to (Any-++ _ _ _) x∈)               ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Common.Prelude

test : Nat → Nat
test = _Common.Prelude.+ 2

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module UniDB.Core where

open import Data.Nat public using (ℕ; suc; zero)
open import Data.Fin public using (Fin; suc; zero)
open import Function public using (id; _∘_)
open import Relation.Binary.PropositionalEquality as PropEq public
  using (_≡_; _≢_; refl; sym; cong; cong₂; trans; subst; module ≡-Reasoning)

open ≡-Reasoning public

Inj : {A B : Set} (f : A → B) → Set
Inj {A} f = {x y : A} → f x ≡ f y → x ≡ y

--------------------------------------------------------------------------------

Dom : Set
Dom = ℕ

infixl 10 _∪_
_∪_ : Dom → Dom → Dom
γ ∪ zero  = γ
γ ∪ suc δ = suc (γ ∪ δ)

∪-assoc : (γ₁ γ₂ γ₃ : Dom) → γ₁ ∪ (γ₂ ∪ γ₃) ≡ (γ₁ ∪ γ₂) ∪ γ₃
∪-assoc γ₁ γ₂ zero     = refl
∪-assoc γ₁ γ₂ (suc γ₃) = cong suc (∪-assoc γ₁ γ₂ γ₃)

--------------------------------------------------------------------------------

STX : Set₁
STX = Dom → Set

MOR : Set₁
MOR = Dom → Dom → Set

--------------------------------------------------------------------------------

Ix : STX
Ix = Fin

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
module hcio where

-- https://github.com/alhassy/AgdaCheatSheet#interacting-with-the-real-world-compilation-haskell-and-io

open import Agda.Builtin.Coinduction using (♯_)
open import Agda.Builtin.Unit        using (⊤)
open import Codata.Musical.Colist    as CL using (take)
open import Codata.Musical.Costring  using (Costring)
open import Data.String              as S using (String; fromList)
open import Data.Vec.Bounded         as B using (toList)
open import Function                 using (const; _∘_)
open import IO                       as IO using ()
import      IO.Primitive             as Primitive

infixr 1 _>>=_ _>>_

_>>=_ : ∀ {ℓ} {α β : Set ℓ} → IO.IO α → (α → IO.IO β) → IO.IO β
this >>= f = ♯ this IO.>>= λ x → ♯ f x

_>>_ : ∀{ℓ} {α β : Set ℓ} → IO.IO α → IO.IO β → IO.IO β
x >> y = x >>= const y

postulate
  getLine∞ : Primitive.IO Costring

{-# FOREIGN GHC
  toColist :: [a] -> MAlonzo.Code.Codata.Musical.Colist.AgdaColist a
  toColist []       = MAlonzo.Code.Codata.Musical.Colist.Nil
  toColist (x : xs) = MAlonzo.Code.Codata.Musical.Colist.Cons x (MAlonzo.RTE.Sharp (toColist xs))
#-}

{-# FOREIGN GHC import Prelude as Haskell #-} -- rename for clarity
{-# COMPILE GHC getLine∞ = fmap toColist Haskell.getLine #-}

getLine : IO.IO String
getLine =
  IO.lift (getLine∞ Primitive.>>= (Primitive.return ∘ S.fromList ∘ B.toList ∘ CL.take 100))

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Homotopy.Group.SuspensionMap where

open import Cubical.Homotopy.Group.Base
open import Cubical.Homotopy.Loopspace
open import Cubical.Homotopy.Freudenthal
open import Cubical.Homotopy.Connected

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Pointed.Homogeneous
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws renaming (assoc to ∙assoc)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.Path
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Transport

open import Cubical.Functions.Morphism

open import Cubical.HITs.Sn
open import Cubical.HITs.Susp renaming (toSusp to σ ; toSuspPointed to σ∙)
open import Cubical.HITs.S1

open import Cubical.Data.Bool hiding (_≟_)
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid

open import Cubical.HITs.PropositionalTruncation
  renaming (rec to pRec ; rec2 to pRec2 ; elim to pElim)
open import Cubical.HITs.SetTruncation
  renaming (rec to sRec ; rec2 to sRec2 ; elim to sElim
          ; elim2 to sElim2 ; elim3 to sElim3 ; map to sMap)
open import Cubical.HITs.Truncation
  renaming (rec to trRec)

open Iso
open IsGroup
open IsSemigroup
open IsMonoid
open GroupStr

{-
This file concerns the suspension maps
suspMapΩ : πₙA → πₙ₊₁ΣA and
suspMap : π'ₙA → π'ₙ₊₁ΣA
For instance, we want to transport freudenthal
for suspMapΩ to suspMap by establishing a dependent
path between the two functions.

This gives, in particular, surjectivity of
πₙ₊₁(Sⁿ) → πₙ₊₂(Sⁿ⁺¹) for n ≥ 2.
-}

-- Definition of the suspension functions
suspMap : ∀ {ℓ} {A : Pointed ℓ}(n : ℕ)
        → S₊∙ (suc n) →∙ A
        → S₊∙ (suc (suc n)) →∙ Susp∙ (typ A)
fst (suspMap n f) north = north
fst (suspMap n f) south = north
fst (suspMap {A = A} n f) (merid a i) =
  (merid (fst f a) ∙ sym (merid (pt A))) i
snd (suspMap n f) = refl

suspMapΩ∙ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
        → ((Ω^ n) A)
        →∙ ((Ω^ (suc n)) (Susp∙ (typ A)))
fst (suspMapΩ∙ {A = A} zero) a = merid a ∙ sym (merid (pt A))
snd (suspMapΩ∙ {A = A} zero) = rCancel (merid (pt A))
suspMapΩ∙ {A = A} (suc n) = Ω→ (suspMapΩ∙ {A = A} n)

suspMapΩ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
         → typ ((Ω^ n) A) → typ ((Ω^ (suc n)) (Susp∙ (typ A)))
suspMapΩ {A = A} n = suspMapΩ∙ {A = A} n .fst

suspMapπ' : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ}
  → π' (suc n) A
  → π' (suc (suc n)) (Susp∙ (typ A))
suspMapπ' n = sMap (suspMap n)

suspMapπ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
        → π n A → π (suc n) (Susp∙ (typ A))
suspMapπ n = sMap (suspMapΩ n)

{-          suspMapΩ
 Ωⁿ A  --------------------> Ω¹⁺ⁿ (Susp A)
 |                           |
 | =                         | ≃ flipΩ
 |          Ωⁿ→ σ           v
Ωⁿ A -------------------> Ωⁿ (Ω (Susp A))
 |                           |
 |                           |
 | ≃ Ω→SphereMap            | ≃ Ω→SphereMap
 |                           |
 v           post∘∙ . σ      v
 (Sⁿ →∙ A) -------------- > (Sⁿ →∙ Ω (Susp A))
 |                           |
 | =                         | ≃ botᵣ
 |                           |
 v            suspMap        v
 (Sⁿ →∙ A) -------------- > (Sⁿ⁺¹→∙ Susp A)
 -}

botᵣ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
  → (S₊∙ n →∙ Ω (Susp∙ (typ A)))
  → S₊∙ (suc n) →∙ Susp∙ (typ A)
fst (botᵣ zero (f , p)) base = north
fst (botᵣ zero (f , p)) (loop i) = f false i
snd (botᵣ zero (f , p)) = refl
fst (botᵣ (suc n) (f , p)) north = north
fst (botᵣ (suc n) (f , p)) south = north
fst (botᵣ (suc n) (f , p)) (merid a i) = f a i
snd (botᵣ (suc n) (f , p)) = refl

----- Top square filler -----
top□ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
      → Ω^→ (suc n) (σ∙ A)
      ≡ (((Iso.fun (flipΩIso (suc n))) , flipΩrefl n)
        ∘∙ suspMapΩ∙ (suc n))
top□ {A = A} zero =
  →∙Homogeneous≡ (isHomogeneousPath _ _)
    (funExt λ p → sym (transportRefl _))
top□ {A = A} (suc n) =
    cong Ω→ (top□ {A = A} n)
  ∙ →∙Homogeneous≡
    (isHomogeneousPath _ _)
    (funExt λ x
      → Ω→∘ (fun (flipΩIso (suc n)) , flipΩrefl n) (suspMapΩ∙ (suc n)) x)

----- Middle square filler -----
module _ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ')
  (homogB : isHomogeneous B) (f : A →∙ B)  where
  nat = isNaturalΩSphereMap A B homogB f
  mutual
    isNatural-Ω→SphereMap : ∀ n p → f ∘∙ Ω→SphereMap n p
                                   ≡ Ω→SphereMap n (Ω^→ n f .fst p)
    isNatural-Ω→SphereMap 0 p =
      →∙Homogeneous≡ homogB (funExt λ {true → f .snd; false → refl})
    isNatural-Ω→SphereMap (n@(suc n')) p =
      cong (f ∘∙_) (Ω→SphereMap-split n' p)
      ∙ nat n' (Ω→SphereMapSplit₁ n' p)
      ∙ cong (ΩSphereMap n') inner
      ∙ sym (Ω→SphereMap-split n' (Ω^→ n f .fst p))
      where
      inner : Ω→ (post∘∙ (S₊∙ n') f) .fst (Ω→ (Ω→SphereMap∙ n') .fst p)
            ≡ Ω→ (Ω→SphereMap∙ n') .fst (Ω^→ (suc n') f .fst p)
      inner =
        sym (Ω→∘ (post∘∙ (S₊∙ n') f) (Ω→SphereMap∙ n') p)
        ∙ cong (λ g∙ → Ω→ g∙ .fst p) (isNatural-Ω→SphereMap∙ n')
        ∙ Ω→∘ (Ω→SphereMap∙ n') (Ω^→ n' f) p

    isNatural-Ω→SphereMap∙ : ∀ n
      → post∘∙ (S₊∙ n) f ∘∙ (Ω→SphereMap∙ n)
      ≡ (Ω→SphereMap∙ n {A = B} ∘∙ Ω^→ n f)
    isNatural-Ω→SphereMap∙ n =
      →∙Homogeneous≡ (isHomogeneous→∙ homogB)
        (funExt (isNatural-Ω→SphereMap n))

mid□ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
         → (p : typ ((Ω^ (suc n)) A))
        → fst (post∘∙ (S₊∙ (suc n)) (σ∙ A)) (Ω→SphereMap (suc n) p)
        ≡ Ω→SphereMap (suc n) (fst (Ω^→ (suc n) (σ∙ A)) p)
mid□ {A = A} n p =
  funExt⁻
    (cong fst
      (isNatural-Ω→SphereMap∙
        A (Ω (Susp∙ (typ A)))
        (isHomogeneousPath _ _)
        (σ∙ A) (suc n))) p

----- Bottom square filler -----
bot□ : ∀ {ℓ} {A : Pointed ℓ}  (n : ℕ) (f : (S₊∙ (suc n) →∙ A))
      → suspMap n f
       ≡ botᵣ {A = A} (suc n) (post∘∙ (S₊∙ (suc n)) (σ∙ A) .fst f)
bot□ {A = A} n f =
  ΣPathP ((funExt (λ { north → refl
                     ; south → refl
                     ; (merid a i) → refl}))
         , refl)

-- We prove that botᵣ is an equivalence
botᵣ⁻' : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
         → S₊∙ (suc n) →∙ Susp∙ (typ A) → (S₊ n → typ (Ω (Susp∙ (typ A))))
botᵣ⁻' zero f false =
  sym (snd f) ∙∙ cong (fst f) loop ∙∙ snd f
botᵣ⁻' zero f true = refl
botᵣ⁻' (suc n) f x =
     sym (snd f)
  ∙∙ cong (fst f) (merid x ∙ sym (merid (ptSn (suc n))))
  ∙∙ snd f

botᵣ⁻ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
  → S₊∙ (suc n) →∙ Susp∙ (typ A)
  → (S₊∙ n →∙ Ω (Susp∙ (typ A)))
fst (botᵣ⁻ {A = A} n f) = botᵣ⁻' {A = A} n f
snd (botᵣ⁻ {A = A} zero f) = refl
snd (botᵣ⁻ {A = A} (suc n) f) =
  cong (sym (snd f) ∙∙_∙∙ snd f)
       (cong (cong (fst f)) (rCancel (merid (ptSn _))))
     ∙ ∙∙lCancel (snd f)

botᵣIso : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
    → Iso (S₊∙ n →∙ Ω (Susp∙ (typ A)))
           (S₊∙ (suc n) →∙ Susp∙ (typ A))
botᵣIso {A = A} n = (iso (botᵣ {A = A} n) (botᵣ⁻ {A = A} n) (h n) (retr n))
  where
  h : (n : ℕ) → section (botᵣ {A = A} n) (botᵣ⁻ {A = A} n)
  h zero (f , p) =
    ΣPathP (funExt (λ { base → sym p
                      ; (loop i) j → doubleCompPath-filler
                                       (sym p) (cong f loop) p (~ j) i})
          , λ i j → p (~ i ∨ j))
  h (suc n) (f , p) =
    ΣPathP (funExt (λ { north → sym p
                      ; south → sym p ∙ cong f (merid (ptSn _))
                      ; (merid a i) j
                       → hcomp (λ k
                         → λ { (i = i0) → p (~ j ∧ k)
                              ; (i = i1) → compPath-filler'
                                           (sym p) (cong f (merid (ptSn _))) k j
                              ; (j = i1) → f (merid a i)})
                           (f (compPath-filler
                              (merid a) (sym (merid (ptSn _))) (~ j) i))})
         , λ i j → p (~ i ∨ j))

  retr : (n : ℕ) → retract (botᵣ {A = A} n) (botᵣ⁻ {A = A} n)
  retr zero (f , p) =
    ΣPathP ((funExt (λ { false → sym (rUnit _) ; true → sym p}))
       , λ i j → p (~ i ∨ j))
  retr (suc n) (f , p) =
    →∙Homogeneous≡ (isHomogeneousPath _ _)
                   (funExt λ x → (λ i
                     → rUnit (cong-∙ (fst ((botᵣ {A = A}(suc n) (f , p))))
                                      (merid x)
                                      (sym (merid (ptSn (suc n)))) i) (~ i))
                   ∙∙ (λ i → f x ∙ sym (p i) )
                   ∙∙ sym (rUnit (f x)))

-- Right hand composite iso
IsoΩSphereMapᵣ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
  → Iso (typ ((Ω^ (suc n)) (Susp∙ (typ A)))) ((S₊∙ (suc n) →∙ Susp∙ (typ A)))
IsoΩSphereMapᵣ {A = A} n =
  compIso (flipΩIso n)
    (compIso (IsoΩSphereMap n) (botᵣIso {A = A} n))

-- The dependent path between the two suspension functions
suspMapPathP : ∀ {ℓ} (A : Pointed ℓ) (n : ℕ)
  → (typ ((Ω^ (suc n)) A) → (typ ((Ω^ (suc (suc n))) (Susp∙ (typ A)))))
   ≡ ((S₊∙ (suc n) →∙ A) → S₊∙ (suc (suc n)) →∙ (Susp∙ (typ A)))
suspMapPathP A n i =
    isoToPath (IsoΩSphereMap {A = A} (suc n)) i
  → isoToPath (IsoΩSphereMapᵣ {A = A} (suc n)) i

Ωσ→suspMap : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
           → PathP (λ i → suspMapPathP A n i)
                    (suspMapΩ (suc n))
                    (suspMap n)
Ωσ→suspMap {A = A} n =
  toPathP (funExt (λ p →
       (λ i → transportRefl
                (Iso.fun (IsoΩSphereMapᵣ {A = A} (suc n))
                  (suspMapΩ {A = A} (suc n)
                    (Iso.inv (IsoΩSphereMap {A = A} (suc n))
                      (transportRefl p i)))) i)
    ∙∙ cong (botᵣ {A = A} (suc n))
            (cong (Ω→SphereMap (suc n) {A = Ω (Susp∙ (typ A)) })
                  ((sym (funExt⁻ (cong fst (top□ {A = A} n))
                     (invEq (Ω→SphereMap (suc n)
                           , isEquiv-Ω→SphereMap (suc n)) p))))
           ∙ (sym (mid□ n (invEq (Ω→SphereMap (suc n)
                                , isEquiv-Ω→SphereMap (suc n)) p))
             ∙ cong (σ∙ (fst A , snd A) ∘∙_)
                    (secEq (Ω→SphereMap (suc n)
                          , isEquiv-Ω→SphereMap (suc n)) p)))
    ∙∙ sym (bot□ n p)))

-- Connectedness of suspFunΩ (Freudenthal)
suspMapΩ-connected : ∀ {ℓ} (n : HLevel) (m : ℕ) {A : Pointed ℓ}
     (connA : isConnected (suc (suc n)) (typ A))
  → isConnectedFun ((suc n + suc n) ∸ m) (suspMapΩ {A = A} m)
suspMapΩ-connected n zero {A = A} connA = isConnectedσ n connA
suspMapΩ-connected n (suc m) {A = A} connA with ((n + suc n) ≟ m)
... | (lt p) = subst (λ x → isConnectedFun x (suspMapΩ {A = A} (suc m)))
                     (sym (n∸m≡0 _ m (<-weaken p)))
                     λ b → tt* , (λ {tt* → refl})
... | (eq q) = subst (λ x → isConnectedFun x (suspMapΩ {A = A} (suc m)))
                     (sym (n∸n≡0 m) ∙ cong (_∸ m) (sym q))
                     λ b → tt* , (λ {tt* → refl})
... | (gt p) = isConnectedCong' (n + suc n ∸ m) (suspMapΩ {A = A} m)
    (subst (λ x → isConnectedFun x (suspMapΩ {A = A} m))
           (sym (suc∸-fst (n + suc n) m p))
           (suspMapΩ-connected n m connA))
    (snd (suspMapΩ∙ m))

-- We prove that the right iso is structure preserving
private
  invComp : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
          → S₊∙ n →∙ Ω (Susp∙ (typ A))
          → S₊∙ n →∙ Ω (Susp∙ (typ A))
          → S₊∙ n →∙ Ω (Susp∙ (typ A))
  fst (invComp n f g) x = (fst f x) ∙ (fst g x)
  snd (invComp n f g) = cong₂ _∙_ (snd f) (snd g) ∙ sym (rUnit refl)

  -- We prove that it agrees with ∙Π
  ∙Π≡invComp : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
          → (f g : S₊∙ (suc n) →∙ Ω (Susp∙ (typ A)))
          → ∙Π f g ≡ invComp {A = A} (suc n) f g
  ∙Π≡invComp zero f g =
    →∙Homogeneous≡ (isHomogeneousPath _ _)
      (funExt (λ { base → rUnit refl
                         ∙ sym (cong (_∙ fst g (snd (S₊∙ 1))) (snd f)
                              ∙ cong (refl ∙_) (snd g))
                 ; (loop i) j →
        hcomp (λ k →
          λ { (i = i0) → (rUnit refl
                          ∙ sym (cong (_∙ fst g (snd (S₊∙ 1))) (snd f)
                          ∙ cong (refl ∙_) (snd g))) j
            ; (i = i1) → (rUnit refl
                           ∙ sym (cong (_∙ fst g (snd (S₊∙ 1))) (snd f)
                           ∙ cong (refl ∙_) (snd g))) j
            ; (j = i0) → ((sym (snd f) ∙∙ cong (fst f) loop ∙∙ snd f)
                         ∙ (sym (snd g) ∙∙ cong (fst g) loop ∙∙ snd g)) i
            ; (j = i1) → cong₂Funct _∙_
                           (cong (fst f) loop) (cong (fst g) loop) (~ k) i})
         (hcomp (λ k →
           λ { (i = i0) → (rUnit refl
                           ∙ sym (cong (_∙ snd g (~ k)) (λ j → snd f (j ∨ ~ k))
                           ∙ cong (refl ∙_) (λ j → snd g (j ∨ ~ k)))) j
             ; (i = i1) → (rUnit refl
                           ∙ sym (cong (_∙ snd g (~ k)) (λ j → snd f (j ∨ ~ k))
                           ∙ cong (refl ∙_) (λ j → snd g (j ∨ ~ k)))) j
             ; (j = i0) → ((sym (snd f) ∙∙ cong (fst f) loop ∙∙ snd f)
                           ∙ (sym (snd g) ∙∙ cong (fst g) loop ∙∙ snd g)) i
             ; (j = i1) → (cong (_∙ snd g (~ k))
                              (doubleCompPath-filler (sym (snd f))
                                  (cong (fst f) loop)
                                               (snd f) (~ k)) ∙
                            cong ((snd f (~ k)) ∙_)
                              (doubleCompPath-filler (sym (snd g))
                                (cong (fst g) loop) (snd g) (~ k))) i})
           (hcomp (λ k →
             λ { (i = i0) → (rUnit (rUnit refl)
                            ∙ cong (rUnit refl ∙_) (cong sym (rUnit refl))) k j
               ; (i = i1) → (rUnit (rUnit refl)
                            ∙ cong (rUnit refl ∙_) (cong sym (rUnit refl))) k j
               ; (j = i0) → ((sym (snd f) ∙∙ cong (fst f) loop ∙∙ snd f)
                            ∙ (sym (snd g) ∙∙ cong (fst g) loop ∙∙ snd g)) i
               ; (j = i1) → (cong (_∙ refl)
                               ((sym (snd f) ∙∙ cong (fst f) loop ∙∙ snd f))
                            ∙ cong (refl ∙_)
                               (sym (snd g) ∙∙ cong (fst g) loop ∙∙ snd g)) i})
                ((cong (λ x → rUnit x j)
                       (sym (snd f) ∙∙ cong (fst f) loop ∙∙ snd f)
                ∙ cong (λ x → lUnit x j)
                       (sym (snd g) ∙∙ cong (fst g) loop ∙∙ snd g)) i)))}))
  ∙Π≡invComp {A = A} (suc n) f g =
    →∙Homogeneous≡ (isHomogeneousPath _ _)
      (funExt λ { north → rUnit refl
                         ∙ sym (cong (fst f north ∙_) (snd g)
                         ∙ cong (_∙ refl) (snd f))
                ; south → rUnit refl
                         ∙ sym (cong₂ _∙_
                               (cong (fst f) (sym (merid (ptSn _))) ∙ snd f)
                               (cong (fst g) (sym (merid (ptSn _))) ∙ snd g))
                ; (merid a i) j → p a i j})
    where
    module _ (a : S₊ (suc n)) where
      f-n = fst f north
      g-n = fst g north
      cong-f = (cong (fst f) (merid a ∙ sym (merid (ptSn _))))
      cong-g = (cong (fst g) (merid a ∙ sym (merid (ptSn _))))
      c-f = sym (snd f) ∙∙ cong-f ∙∙ snd f
      c-g = sym (snd g) ∙∙ cong-g ∙∙ snd g

      p : I → I → fst (Ω (Susp∙ (typ A)))
      p i j =
        hcomp (λ k →
          λ { (i = i0) → (rUnit (λ _ → snd (Susp∙ (typ A)))
                         ∙ sym ((cong (fst f north ∙_) (snd g)
                               ∙ cong (_∙ refl) (snd f)))) j
             ; (i = i1) → (rUnit refl
                    ∙  sym (cong₂ _∙_
                          (compPath-filler'
                            (cong (fst f) (sym (merid (ptSn _)))) (snd f) k)
                          (compPath-filler'
                            (cong (fst g) (sym (merid (ptSn _)))) (snd g) k))) j
             ; (j = i0) → (c-f ∙ c-g) i
             ; (j = i1) → fst f (compPath-filler
                                  (merid a)
                                  (sym (merid (ptSn _))) (~ k) i)
                         ∙ fst g (compPath-filler
                                  (merid a)
                                  (sym (merid (ptSn _))) (~ k) i)})
         (hcomp (λ k →
           λ {(i = i0) → (rUnit (λ _ → snd (Susp∙ (typ A)))
                        ∙ sym ((cong (fst f north ∙_) (snd g)
                             ∙ cong (_∙ refl) (snd f)))) j
            ; (i = i1) → (rUnit refl ∙ sym (cong₂ _∙_ (snd f) (snd g))) j
            ; (j = i0) → (c-f ∙ c-g) i
            ; (j = i1) → cong₂Funct _∙_ cong-f cong-g (~ k) i})
           (hcomp (λ k →
           λ {(i = i0) → (rUnit refl
                        ∙ sym (compPath-filler'
                               ((cong (fst f north ∙_) (snd g)))
                                (cong (_∙ refl) (snd f)) k)) j
            ; (i = i1) → (rUnit refl
                        ∙  sym (cong₂ _∙_ (λ i → snd f (i ∨ ~ k)) (snd g))) j
            ; (j = i0) → (c-f ∙ c-g) i
            ; (j = i1) → (cong (λ x → x ∙ snd g (~ k))
                           (doubleCompPath-filler refl
                            cong-f (snd f) (~ k))
                         ∙ cong ((snd f (~ k)) ∙_)
                              (doubleCompPath-filler
                                (sym (snd g)) cong-g refl (~ k))) i})
            (hcomp (λ k →
             λ {(i = i0) → compPath-filler
                            (rUnit (λ _ → snd (Susp∙ (typ A))))
                            (sym ((cong (_∙ refl) (snd f)))) k j
            ; (i = i1) → compPath-filler
                              (rUnit refl)
                              (sym (cong (refl ∙_) (snd g))) k j
            ; (j = i0) → (c-f ∙ c-g) i
            ; (j = i1) → (cong (_∙ refl)
                            ((λ j → snd f (~ j ∧ ~ k)) ∙∙ cong-f ∙∙ snd f)
                      ∙ cong (refl ∙_)
                         (sym (snd g) ∙∙ cong-g ∙∙ (λ j → snd g (j ∧ ~ k)))) i})
             (((cong (λ x → rUnit x j) c-f) ∙ (cong (λ x → lUnit x j) c-g)) i))))

hom-botᵣ⁻ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
  → (f g : S₊∙ (suc n) →∙ Susp∙ (typ A))
  → botᵣ⁻ {A = A} n (∙Π f g)
   ≡ invComp {A = A} n (botᵣ⁻ {A = A} n f) (botᵣ⁻ {A = A} n g)
hom-botᵣ⁻ zero f g =
  ΣPathP ((funExt (λ { false → sym (rUnit _)
                     ; true → (rUnit _)}))
                     , ((λ i j → rUnit refl (i ∧ ~ j))
                      ▷ lUnit (sym (rUnit refl))))
hom-botᵣ⁻ (suc n) f g =
  →∙Homogeneous≡ (isHomogeneousPath _ _)
    (funExt (λ x → (sym (rUnit (cong (fst (∙Π f g)) (merid x ∙ sym (merid (ptSn _))))))
                      ∙∙ cong-∙ (fst (∙Π f g)) (merid x) (sym (merid (ptSn _)))
                      ∙∙ cong (cong (fst (∙Π f g)) (merid x) ∙_) (cong sym lem)
                       ∙ sym (rUnit (cong (fst (∙Π f g)) (merid x)))))
  where
  lem : cong (fst (∙Π f g)) (merid (ptSn (suc n))) ≡ refl
  lem = (λ i → (sym (snd f) ∙∙ cong (fst f) (rCancel (merid (ptSn _)) i) ∙∙ snd f)
              ∙ (sym (snd g) ∙∙ cong (fst g) (rCancel (merid (ptSn _)) i) ∙∙ snd g))
      ∙ (λ i → ∙∙lCancel (snd f) i ∙ ∙∙lCancel (snd g) i)
       ∙ sym (rUnit refl)

-- We get that botᵣ⁻ (and hence botᵣ) is homomorphism
hom-botᵣ⁻' : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
  → (f g : S₊∙ (suc (suc n)) →∙ Susp∙ (typ A))
  → botᵣ⁻ {A = A} (suc n) (∙Π f g)
   ≡ ∙Π (botᵣ⁻ {A = A} (suc n) f) (botᵣ⁻ {A = A} (suc n) g)
hom-botᵣ⁻' {A = A} n f g =
    hom-botᵣ⁻ {A = A} (suc n) f g
  ∙ sym (∙Π≡invComp {A = A} _ (botᵣ⁻ {A = A} _ f) (botᵣ⁻ {A = A} _ g))

hom-botᵣ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
  → (f g : S₊∙ (suc n) →∙ Ω (Susp∙ (typ A)))
  → botᵣ {A = A} (suc n) (∙Π f g)
  ≡ ∙Π (botᵣ {A = A} (suc n) f) (botᵣ {A = A} (suc n) g)
hom-botᵣ {A = A} n f g =
  morphLemmas.isMorphInv ∙Π ∙Π (botᵣ⁻ {A = A} (suc n))
    (hom-botᵣ⁻' {A = A} n)
    (botᵣ {A = A} (suc n))
    (leftInv (botᵣIso {A = A} (suc n)))
    (rightInv (botᵣIso {A = A} (suc n)))
    f g

isHom-IsoΩSphereMapᵣ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
                    (p q : typ ((Ω^ (2 + n)) (Susp∙ (typ A))))
                 → Iso.fun (IsoΩSphereMapᵣ (suc n)) (p ∙ q)
                  ≡ ∙Π (Iso.fun (IsoΩSphereMapᵣ (suc n)) p)
                       (Iso.fun (IsoΩSphereMapᵣ (suc n)) q)
isHom-IsoΩSphereMapᵣ {A = A} n p q =
     cong (botᵣ {A = A} (suc n))
       (cong (Ω→SphereMap (suc n) {A = Ω (Susp∙ (typ A))})
         (flipΩIsopres· n p q)
     ∙ isHom-Ω→SphereMap n (fun (flipΩIso (suc n)) p)
                    (fun (flipΩIso (suc n)) q))
     ∙ hom-botᵣ n _ _

suspMapΩ→hom : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (p q : typ ((Ω^ (suc n)) A))
  → suspMapΩ (suc n) (p ∙ q)
   ≡ suspMapΩ (suc n) p ∙ suspMapΩ (suc n) q
suspMapΩ→hom {A = A} n p q =
     cong (sym (snd (suspMapΩ∙ {A = A} n)) ∙∙_∙∙ snd (suspMapΩ∙ {A = A} n))
          (cong-∙ (fst (suspMapΩ∙ {A = A} n)) p q)
   ∙ help (snd (suspMapΩ∙ {A = A} n)) _ _
  where
  help : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y) (q s : x ≡ x)
    → sym p ∙∙ (q ∙ s) ∙∙ p
    ≡ (sym p ∙∙ q ∙∙ p) ∙ (sym p ∙∙ s ∙∙ p)
  help {x = x} =
    J (λ y p → (q s : x ≡ x)
    → sym p ∙∙ (q ∙ s) ∙∙ p
    ≡ (sym p ∙∙ q ∙∙ p ) ∙ (sym p ∙∙ s ∙∙ p))
       λ q s → sym (rUnit (q ∙ s))
             ∙ cong₂ _∙_ (rUnit q) (rUnit s)

private
  transportLem : ∀ {ℓ} {A B : Type ℓ}
                   (_+A_ : A → A → A) (_+B_ : B → B → B)
                 → (e : Iso A B)
                 → ((x y : A) → fun e (x +A y) ≡ fun e x +B fun e y)
                 → PathP (λ i → isoToPath e i → isoToPath e i → isoToPath e i)
                         _+A_ _+B_
  transportLem _+A_ _+B_ e hom =
    toPathP (funExt (λ p → funExt λ q →
         (λ i → transportRefl
                  (fun e (inv e (transportRefl p i)
                       +A inv e (transportRefl q i))) i)
      ∙∙ hom (inv e p) (inv e q)
      ∙∙ cong₂ _+B_ (rightInv e p) (rightInv e q)))

  pₗ : ∀ {ℓ} (A : Pointed ℓ) (n : ℕ)
    → typ (Ω ((Ω^ n) A)) ≡ (S₊∙ (suc n) →∙ A)
  pₗ A n = isoToPath (IsoΩSphereMap {A = A} (suc n))

  pᵣ : ∀ {ℓ} (A : Pointed ℓ) (n : ℕ)
    → typ ((Ω^ (2 + n)) (Susp∙ (typ A)))
     ≡ (S₊∙ (suc (suc n)) →∙ Susp∙ (typ A))
  pᵣ A n = isoToPath (IsoΩSphereMapᵣ {A = A} (suc n))

∙Π→∙ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
     → PathP (λ i → pₗ A n i → pₗ A n i → pₗ A n i) _∙_ ∙Π
∙Π→∙ {A = A} n =
  transportLem _∙_ ∙Π (IsoΩSphereMap {A = A} (suc n)) (isHom-Ω→SphereMap n)

∙Π→∙ᵣ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
     → PathP (λ i → pᵣ A n i → pᵣ A n i → pᵣ A n i) _∙_ ∙Π
∙Π→∙ᵣ {A = A} n =
  transportLem _∙_ ∙Π (IsoΩSphereMapᵣ {A = A} (suc n)) (isHom-IsoΩSphereMapᵣ n)

isHom-suspMap : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (f g : S₊∙ (suc n) →∙ A)
           → suspMap n (∙Π f g)
           ≡ ∙Π (suspMap n f) (suspMap n g)
isHom-suspMap {A = A} n =
   transport (λ i → (f g : isoToPath (IsoΩSphereMap {A = A} (suc n)) i)
                 → Ωσ→suspMap n i (∙Π→∙ n i f g)
                 ≡ ∙Π→∙ᵣ n i (Ωσ→suspMap n i f) (Ωσ→suspMap n i g))
             (suspMapΩ→hom n)

suspMapπHom : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
            → GroupHom (πGr n A) (πGr (suc n) (Susp∙ (typ A)))
fst (suspMapπHom {A = A} n) = suspMapπ (suc n)
snd (suspMapπHom {A = A} n) =
  makeIsGroupHom
    (sElim2 (λ _ _ → isSetPathImplicit)
      λ p q → cong ∣_∣₂ (suspMapΩ→hom n p q))

suspMapπ'Hom : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
  → GroupHom (π'Gr n A) (π'Gr (suc n) (Susp∙ (typ A)))
fst (suspMapπ'Hom {A = A} n) = suspMapπ' n
snd (suspMapπ'Hom {A = A} n) =
  makeIsGroupHom (sElim2 (λ _ _ → isSetPathImplicit)
    λ f g → cong ∣_∣₂ (isHom-suspMap n f g))

πGr≅π'Grᵣ : ∀ {ℓ} (n : ℕ) (A : Pointed ℓ)
          → GroupIso (πGr (suc n) (Susp∙ (typ A)))
                      (π'Gr (suc n) (Susp∙ (typ A)))
fst (πGr≅π'Grᵣ n A) = setTruncIso (IsoΩSphereMapᵣ (suc n))
snd (πGr≅π'Grᵣ n A) =
  makeIsGroupHom (sElim2 (λ _ _ → isSetPathImplicit)
    λ f g → cong ∣_∣₂ (isHom-IsoΩSphereMapᵣ n f g))

private
  isConnectedPres : ∀ {ℓ} {A : Pointed ℓ} (con n : ℕ)
                  → isConnectedFun con (suspMapΩ∙ {A = A} (suc n) .fst)
                  → isConnectedFun con (suspMap {A = A} n)
  isConnectedPres {A = A} con n hyp =
    transport (λ i → isConnectedFun con (Ωσ→suspMap {A = A} n i)) hyp

isConnectedSuspMap : (n m : ℕ)
  → isConnectedFun ((m + suc m) ∸ n) (suspMap {A = S₊∙ (suc m)} n)
isConnectedSuspMap n m =
  isConnectedPres _ _ (suspMapΩ-connected m (suc n) (sphereConnected (suc m)))

isSurjectiveSuspMap : (n : ℕ)
  → isSurjective (suspMapπ'Hom {A = S₊∙ (2 + n)} (2 + n))
isSurjectiveSuspMap n =
  sElim (λ _ → isProp→isSet squash₁)
    λ f →
      trRec
        ((subst (λ x → isOfHLevel x (isInIm (suspMapπ'Hom (2 + n)) ∣ f ∣₂))
                      (sym (snd (lem n n)))
                      (isProp→isOfHLevelSuc {A = isInIm (suspMapπ'Hom (2 + n)) ∣ f ∣₂}
                      (fst (lem n n)) squash₁)))
        (λ p → ∣ ∣ fst p ∣₂ , (cong ∣_∣₂ (snd p)) ∣₁)
        (fst (isConnectedSuspMap (2 + n) (suc n) f))
  where
  lem : (m n : ℕ) → Σ[ x ∈ ℕ ] ((m + suc (suc n) ∸ suc n) ≡ suc x)
  lem zero zero = 0 , refl
  lem (suc m) zero = suc m , +-comm m 2
  lem zero (suc n) = lem zero n
  lem (suc m) (suc n) = fst (lem (suc m) n) , (cong (_∸ (suc n)) (+-comm m (3 + n))
                     ∙∙ cong (_∸ n) (+-comm (suc (suc n)) m)
                     ∙∙ snd (lem (suc m) n))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module PiFrac.Category where
open import Categories.Category.Monoidal
open import Categories.Category.Monoidal.Braided
open import Categories.Category.Monoidal.Symmetric
open import Categories.Category.Monoidal.Rigid
open import Categories.Category.Monoidal.CompactClosed
open import Categories.Functor.Bifunctor
open import Categories.Category
open import Categories.Category.Product
open import Categories.Category.Groupoid
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product
open import Data.Maybe
open import Relation.Binary.Core
open import Relation.Binary hiding (Symmetric)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_)
open import PiFrac.Syntax
open import PiFrac.Opsem
open import PiFrac.Interp
open import PiFrac.Properties

Pi∙ : Category _ _ _
Pi∙ = record
    { Obj = Σ[ t ∈ 𝕌 ] ⟦ t ⟧
    ; _⇒_ = λ (A , a) (B , b) → Σ[ c ∈ (A ↔ B) ] (interp c a ≡ just b)
    ; _≈_ = λ {(A , a)} {(B , b)} (c , eq) (c' , eq) → ⊤
    ; id = id↔ , refl
    ; _∘_ = λ (c₂ , eq₂) (c₁ , eq₁) → comp (c₁ , eq₁) (c₂ , eq₂)
    ; assoc = tt
    ; sym-assoc = tt
    ; identityˡ = tt
    ; identityʳ = tt
    ; identity² = tt
    ; equiv = record { refl = tt ; sym = λ _ → tt ; trans = λ _ _ → tt }
    ; ∘-resp-≈ = λ _ _ → tt
    }
    where
    comp : ∀ {A B C a b c} → Σ[ c₁ ∈ (A ↔ B) ] (interp c₁ a ≡ just b) → Σ[ c₂ ∈ (B ↔ C) ] (interp c₂ b ≡ just c)
         → Σ[ c' ∈ (A ↔ C) ] (interp c' a ≡ just c)
    comp {c = c} (c₁ , eq₁) (c₂ , eq₂) = (c₁ ⨾ c₂) , subst (λ x → (x >>= interp c₂) ≡ just c) (sym eq₁) eq₂

Pi∙Groupoid : Groupoid _ _ _
Pi∙Groupoid = record { category = Pi∙
                     ; isGroupoid = record { _⁻¹ = λ (c , eq) → ! c , interp! c _ _ eq
                                           ; iso = record { isoˡ = tt
                                                          ; isoʳ = tt } } }

Pi∙Monoidal : Monoidal Pi∙
Pi∙Monoidal = record
            { ⊗ = record
                { F₀ = λ ((A , a) , (B , b)) → (A ×ᵤ B) , (a , b)
                ; F₁ = λ {((A , a) , (B , b))} {((C , c) , (D , d))} ((c₁ , eq₁) , (c₂ , eq₂)) →
                         (c₁ ⊗ c₂) , subst (λ x → (x >>= (λ v₁' → interp c₂ b >>= λ v₂' → just (v₁' , v₂'))) ≡ just (c , d))
                                           (sym eq₁) (subst (λ x → (x >>= λ v₂' → just (c , v₂')) ≡ just (c , d)) (sym eq₂) refl)
                ; identity = tt
                ; homomorphism = tt
                ; F-resp-≈ = λ _ → tt
                }
            ; unit = (𝟙 , tt)
            ; unitorˡ = record { from = unite⋆l , refl
                               ; to   = uniti⋆l , refl
                               ; iso  = record { isoˡ = tt ; isoʳ = tt } }
            ; unitorʳ = record { from = unite⋆r , refl
                               ; to   = uniti⋆r , refl
                               ; iso  = record { isoˡ = tt ; isoʳ = tt } }
            ; associator = record { from = assocr⋆ , refl
                                  ; to   = assocl⋆ , refl
                                  ; iso  = record { isoˡ = tt ; isoʳ = tt } }
            ; unitorˡ-commute-from = tt
            ; unitorˡ-commute-to = tt
            ; unitorʳ-commute-from = tt
            ; unitorʳ-commute-to = tt
            ; assoc-commute-from = tt
            ; assoc-commute-to = tt
            ; triangle = tt
            ; pentagon = tt
            }

Pi∙Braided : Braided Pi∙Monoidal
Pi∙Braided = record { braiding = record { F⇒G = record { η = λ _ → swap⋆ , refl
                                                       ; commute = λ _ → tt
                                                       ; sym-commute = λ _ → tt }
                                        ; F⇐G = record { η = λ _ → swap⋆ , refl
                                                       ; commute = λ _ → tt
                                                       ; sym-commute = λ _ → tt }
                                        ; iso = λ X → record { isoˡ = tt ; isoʳ = tt } }
                    ; hexagon₁ = tt
                    ; hexagon₂ = tt }

Pi∙Symmetric : Symmetric Pi∙Monoidal
Pi∙Symmetric = record { braided = Pi∙Braided
                      ; commutative = tt}

Pi∙Rigid : LeftRigid Pi∙Monoidal
Pi∙Rigid = record { _⁻¹ = λ {(A , a) → 𝟙/ a , ↻}
                  ; η = λ {(X , x)} → ηₓ x , refl
                  ; ε = λ {(X , x)} → (swap⋆ ⨾ εₓ x) , εₓ≡
                  ; snake₁ = tt
                  ; snake₂ = tt}
           where
             εₓ≡ : ∀ {X} {x : ⟦ X ⟧} → interp (swap⋆ ⨾ εₓ x) (↻ , x) ≡ just tt
             εₓ≡ {X} {x} with x ≟  x
             ... | yes refl = refl
             ... | no  neq  = ⊥-elim (neq refl)

Pi∙CompactClosed : CompactClosed Pi∙Monoidal
Pi∙CompactClosed = record { symmetric = Pi∙Symmetric
                          ; rigid     = inj₁ Pi∙Rigid }


text:
{-

          Types Summer School 2007

                 Bertinoro
             Aug 19 - 31, 2007

                   Agda

                Ulf Norell

-}

{-

  Learn more about Agda on the Agda wiki:

    http://www.cs.chalmers.se/~ulfn/Agda

  This is where you find the exercises for the afternoon.

-}

-- Each Agda file contains a top-level module, whose
-- name corresponds to the file name.

module Basics where

{-

  Expressions (types and terms)

-}

-- The expression language of Agda is your favorite dependently
-- typed λ-calculus.

-- For instance:
id₁ : (A : Set) -> A -> A
id₁ = \ A x -> x

id₂ : (A : Set) -> A -> A
id₂ = \ A x -> id₁ A (id₁ A x)

-- Note: Agda likes white space. This is not correct:
--   id:(A:Set)->A->A

-- Why not? In Agda the following strings are valid identifiers:
--   id:
--   A:Set
--   ->A->A

-- Another useful function, featuring telescopes
-- and typed λs.
compose : (A B C : Set) -> (B -> C) -> (A -> B) -> A -> C
compose = \(A B C : Set) f g x -> f (g x)

compose' : (A B : Set)(C : B -> Set)
           (f : (x : B) -> C x)(g : A -> B) ->
           (x : A) -> C (g x)
compose' = \A B C f g x -> f (g x)

{-

  Implicit arguments

-}

-- Writing down type arguments explicitly soon gets old.
-- Enter implicit arguments.

-- Note the curlies in the telescope. And A mysteriously disappeares
-- in the definition.
id₃ : {A : Set} -> A -> A
id₃ = \ x -> x

-- And it's not there when applying the function.
id₄ : {A : Set} -> A -> A
id₄ = \ x -> (id₃ (id₃ x))

-- If you think the type checker should figure out the value of
-- something explicit, you write _.
id₆ : {A : Set} -> A -> A
id₆ x = id₁ _ x

-- Interesting though it is, eventually you'll get bored
-- with the λ-calculus...

-- Move on to: Datatypes.agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic lemmas showing that various types are related (isomorphic or
-- equivalent or…)
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Function.Related.TypeIsomorphisms where

open import Algebra
import Algebra.FunctionProperties as FP
open import Axiom.Extensionality.Propositional using (Extensionality)
open import Algebra.Structures
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product as Prod hiding (swap)
open import Data.Product.Function.NonDependent.Propositional
open import Data.Sum as Sum
open import Data.Sum.Properties using (swap-involutive)
open import Data.Sum.Function.Propositional using (_⊎-cong_)
open import Data.Unit using (⊤)
open import Level using (Level; Lift; lower; 0ℓ; suc)
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Eq using (_⇔_; Equivalence)
open import Function.Inverse as Inv using (_↔_; Inverse; inverse)
open import Function.Related
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)
open import Relation.Nullary using (Dec; ¬_; yes; no)
open import Relation.Nullary.Decidable using (True)

------------------------------------------------------------------------
-- Properties of Σ and _×_

-- Σ is associative
Σ-assoc : ∀ {a b c}
            {A : Set a} {B : A → Set b} {C : (a : A) → B a → Set c} →
          Σ (Σ A B) (uncurry C) ↔ Σ A (λ a → Σ (B a) (C a))
Σ-assoc = inverse (λ where ((a , b) , c) → (a , b , c))
                  (λ where (a , b , c) → ((a , b) , c))
                  (λ _ → P.refl) (λ _ → P.refl)

-- × is commutative

×-comm : ∀ {a b} (A : Set a) (B : Set b) → (A × B) ↔ (B × A)
×-comm _ _ = inverse Prod.swap Prod.swap (λ _ → P.refl) λ _ → P.refl

-- × has ⊤ as its identity

×-identityˡ : ∀ ℓ → FP.LeftIdentity _↔_ (Lift ℓ ⊤) _×_
×-identityˡ _ _ = inverse proj₂ -,_ (λ _ → P.refl) (λ _ → P.refl)

×-identityʳ : ∀ ℓ → FP.RightIdentity _↔_ (Lift ℓ ⊤) _×_
×-identityʳ _ _ = inverse proj₁ (_, _) (λ _ → P.refl) (λ _ → P.refl)

×-identity : ∀ ℓ → FP.Identity _↔_ (Lift ℓ ⊤) _×_
×-identity ℓ = ×-identityˡ ℓ , ×-identityʳ ℓ

-- × has ⊥ has its zero

×-zeroˡ : ∀ ℓ → FP.LeftZero _↔_ (Lift ℓ ⊥) _×_
×-zeroˡ ℓ A = inverse proj₁ (⊥-elim ∘′ lower)
                      (⊥-elim ∘ lower ∘ proj₁) (⊥-elim ∘ lower)

×-zeroʳ : ∀ ℓ → FP.RightZero _↔_ (Lift ℓ ⊥) _×_
×-zeroʳ ℓ A = inverse proj₂ (⊥-elim ∘′ lower)
                     (⊥-elim ∘ lower ∘ proj₂) (⊥-elim ∘ lower)

×-zero : ∀ ℓ → FP.Zero _↔_ (Lift ℓ ⊥) _×_
×-zero ℓ  = ×-zeroˡ ℓ , ×-zeroʳ ℓ

------------------------------------------------------------------------
-- Properties of ⊎

-- ⊎ is associative

⊎-assoc : ∀ ℓ → FP.Associative {ℓ = ℓ} _↔_ _⊎_
⊎-assoc ℓ _ _ _ = inverse
  [ [ inj₁ , inj₂ ∘′ inj₁ ]′ , inj₂ ∘′ inj₂ ]′
  [ inj₁ ∘′ inj₁ , [ inj₁ ∘′ inj₂ , inj₂ ]′ ]′
  [ [ (λ _ → P.refl) , (λ _ → P.refl) ] , (λ _ → P.refl) ]
  [ (λ _ → P.refl) , [ (λ _ → P.refl) , (λ _ → P.refl) ] ]

-- ⊎ is commutative

⊎-comm : ∀ {a b} (A : Set a) (B : Set b) → (A ⊎ B) ↔ (B ⊎ A)
⊎-comm _ _ = inverse swap swap swap-involutive swap-involutive

-- ⊎ has ⊥ as its identity

⊎-identityˡ : ∀ ℓ → FP.LeftIdentity _↔_ (Lift ℓ ⊥) _⊎_
⊎-identityˡ _ _ = inverse [ (λ ()) , id ]′ inj₂
                          [ (λ ()) , (λ _ → P.refl) ] (λ _ → P.refl)

⊎-identityʳ : ∀ ℓ → FP.RightIdentity _↔_ (Lift ℓ ⊥) _⊎_
⊎-identityʳ _ _ = inverse [ id , (λ ()) ]′ inj₁
                          [ (λ _ → P.refl) , (λ ()) ] (λ _ → P.refl)

⊎-identity : ∀ ℓ → FP.Identity _↔_ (Lift ℓ ⊥) _⊎_
⊎-identity ℓ = ⊎-identityˡ ℓ , ⊎-identityʳ ℓ

------------------------------------------------------------------------
-- Properties of × and ⊎

-- × distributes over ⊎

×-distribˡ-⊎ : ∀ ℓ → FP._DistributesOverˡ_ {ℓ = ℓ} _↔_ _×_ _⊎_
×-distribˡ-⊎ ℓ _ _ _ = inverse
  (uncurry λ x → [ inj₁ ∘′ (x ,_) , inj₂ ∘′ (x ,_) ]′)
  [ Prod.map₂ inj₁ , Prod.map₂ inj₂ ]′
  (uncurry λ _ → [ (λ _ → P.refl) , (λ _ → P.refl) ])
  [ (λ _ → P.refl) , (λ _ → P.refl) ]

×-distribʳ-⊎ : ∀ ℓ → FP._DistributesOverʳ_ {ℓ = ℓ} _↔_ _×_ _⊎_
×-distribʳ-⊎ ℓ _ _ _ = inverse
  (uncurry [ curry inj₁ , curry inj₂ ]′)
  [ Prod.map₁ inj₁ , Prod.map₁ inj₂ ]′
  (uncurry [ (λ _ _ → P.refl) , (λ _ _ → P.refl) ])
  [ (λ _ → P.refl) , (λ _ → P.refl) ]

×-distrib-⊎ : ∀ ℓ → FP._DistributesOver_ {ℓ = ℓ} _↔_ _×_ _⊎_
×-distrib-⊎ ℓ = ×-distribˡ-⊎ ℓ , ×-distribʳ-⊎ ℓ

------------------------------------------------------------------------
-- ⊥, ⊤, _×_ and _⊎_ form a commutative semiring

-- ⊤, _×_ form a commutative monoid

×-isMagma : ∀ k ℓ → IsMagma {Level.suc ℓ} (Related ⌊ k ⌋) _×_
×-isMagma k ℓ = record
  { isEquivalence = SK-isEquivalence k ℓ
  ; ∙-cong        = _×-cong_
  }

×-magma : Symmetric-kind → (ℓ : Level) → Magma _ _
×-magma k ℓ = record
  { isMagma = ×-isMagma k ℓ
  }

×-isSemigroup : ∀ k ℓ → IsSemigroup {Level.suc ℓ} (Related ⌊ k ⌋) _×_
×-isSemigroup k ℓ = record
  { isMagma = ×-isMagma k ℓ
  ; assoc   = λ _ _ _ → ↔⇒ Σ-assoc
  }

×-semigroup : Symmetric-kind → (ℓ : Level) → Semigroup _ _
×-semigroup k ℓ = record
  { isSemigroup = ×-isSemigroup k ℓ
  }

×-isMonoid : ∀ k ℓ → IsMonoid (Related ⌊ k ⌋) _×_ (Lift ℓ ⊤)
×-isMonoid k ℓ = record
  { isSemigroup = ×-isSemigroup k ℓ
  ; identity    = (↔⇒ ∘ ×-identityˡ ℓ) , (↔⇒ ∘ ×-identityʳ ℓ)
  }

×-monoid : Symmetric-kind → (ℓ : Level) → Monoid _ _
×-monoid k ℓ = record
  { isMonoid = ×-isMonoid k ℓ
  }

×-isCommutativeMonoid : ∀ k ℓ → IsCommutativeMonoid (Related ⌊ k ⌋) _×_ (Lift ℓ ⊤)
×-isCommutativeMonoid k ℓ = record
  { isSemigroup = ×-isSemigroup k ℓ
  ; identityˡ   = ↔⇒ ∘ ×-identityˡ ℓ
  ; comm        = λ _ _ → ↔⇒ (×-comm _ _)
  }

×-commutativeMonoid : Symmetric-kind → (ℓ : Level) → CommutativeMonoid _ _
×-commutativeMonoid k ℓ = record
  { isCommutativeMonoid = ×-isCommutativeMonoid k ℓ
  }

-- ⊥, _⊎_ form a commutative monoid

⊎-isMagma : ∀ k ℓ → IsMagma {Level.suc ℓ} (Related ⌊ k ⌋) _⊎_
⊎-isMagma k ℓ = record
  { isEquivalence = SK-isEquivalence k ℓ
  ; ∙-cong        = _⊎-cong_
  }

⊎-magma : Symmetric-kind → (ℓ : Level) → Magma _ _
⊎-magma k ℓ = record
  { isMagma = ⊎-isMagma k ℓ
  }

⊎-isSemigroup : ∀ k ℓ → IsSemigroup {Level.suc ℓ} (Related ⌊ k ⌋) _⊎_
⊎-isSemigroup k ℓ = record
  { isMagma = ⊎-isMagma k ℓ
  ; assoc   = λ A B C → ↔⇒ (⊎-assoc ℓ A B C)
  }

⊎-semigroup : Symmetric-kind → (ℓ : Level) → Semigroup _ _
⊎-semigroup k ℓ = record
  { isSemigroup = ⊎-isSemigroup k ℓ
  }

⊎-isMonoid : ∀ k ℓ → IsMonoid (Related ⌊ k ⌋) _⊎_ (Lift ℓ ⊥)
⊎-isMonoid k ℓ = record
  { isSemigroup = ⊎-isSemigroup k ℓ
  ; identity    = (↔⇒ ∘ ⊎-identityˡ ℓ) , (↔⇒ ∘ ⊎-identityʳ ℓ)
  }

⊎-monoid : Symmetric-kind → (ℓ : Level) → Monoid _ _
⊎-monoid k ℓ = record
  { isMonoid = ⊎-isMonoid k ℓ
  }

⊎-isCommutativeMonoid : ∀ k ℓ → IsCommutativeMonoid (Related ⌊ k ⌋) _⊎_ (Lift ℓ ⊥)
⊎-isCommutativeMonoid k ℓ = record
  { isSemigroup = ⊎-isSemigroup k ℓ
  ; identityˡ   = ↔⇒ ∘ ⊎-identityˡ ℓ
  ; comm        = λ _ _ → ↔⇒ (⊎-comm _ _)
  }

⊎-commutativeMonoid : Symmetric-kind → (ℓ : Level) →
                      CommutativeMonoid _ _
⊎-commutativeMonoid k ℓ = record
  { isCommutativeMonoid = ⊎-isCommutativeMonoid k ℓ
  }

×-⊎-isCommutativeSemiring : ∀ k ℓ →
  IsCommutativeSemiring (Related ⌊ k ⌋) _⊎_ _×_ (Lift ℓ ⊥) (Lift ℓ ⊤)
×-⊎-isCommutativeSemiring k ℓ = record
  { +-isCommutativeMonoid = ⊎-isCommutativeMonoid k ℓ
  ; *-isCommutativeMonoid = ×-isCommutativeMonoid k ℓ
  ; distribʳ              = λ A B C → ↔⇒ (×-distribʳ-⊎ ℓ A B C)
  ; zeroˡ                 = ↔⇒ ∘ ×-zeroˡ ℓ
  }

×-⊎-commutativeSemiring : Symmetric-kind → (ℓ : Level) →
                          CommutativeSemiring (Level.suc ℓ) ℓ
×-⊎-commutativeSemiring k ℓ = record
  { isCommutativeSemiring = ×-⊎-isCommutativeSemiring k ℓ
  }

------------------------------------------------------------------------
-- Some reordering lemmas

ΠΠ↔ΠΠ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p) →
        ((x : A) (y : B) → P x y) ↔ ((y : B) (x : A) → P x y)
ΠΠ↔ΠΠ _ = inverse flip flip (λ _ → P.refl) (λ _ → P.refl)

∃∃↔∃∃ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p) →
        (∃₂ λ x y → P x y) ↔ (∃₂ λ y x → P x y)
∃∃↔∃∃ P = inverse to from (λ _ → P.refl) (λ _ → P.refl)
  where
  to : (∃₂ λ x y → P x y) → (∃₂ λ y x → P x y)
  to (x , y , Pxy) = (y , x , Pxy)

  from : (∃₂ λ y x → P x y) → (∃₂ λ x y → P x y)
  from (y , x , Pxy) = (x , y , Pxy)

------------------------------------------------------------------------
-- Implicit and explicit function spaces are isomorphic

Π↔Π : ∀ {a b} {A : Set a} {B : A → Set b} →
      ((x : A) → B x) ↔ ({x : A} → B x)
Π↔Π = inverse (λ f {x} → f x) (λ f x → f) (λ _ → P.refl) (λ _ → P.refl)

------------------------------------------------------------------------
-- _→_ preserves the symmetric relations

_→-cong-⇔_ :
  ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
  A ⇔ B → C ⇔ D → (A → C) ⇔ (B → D)
A⇔B →-cong-⇔ C⇔D = Eq.equivalence
  (λ f x → Equivalence.to   C⇔D ⟨$⟩ f (Equivalence.from A⇔B ⟨$⟩ x))
  (λ f x → Equivalence.from C⇔D ⟨$⟩ f (Equivalence.to   A⇔B ⟨$⟩ x))

→-cong :
  ∀ {a b c d} →
  Extensionality a c → Extensionality b d →
  ∀ {k} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
  A ∼[ ⌊ k ⌋ ] B → C ∼[ ⌊ k ⌋ ] D → (A → C) ∼[ ⌊ k ⌋ ] (B → D)
→-cong extAC extBD {equivalence} A⇔B C⇔D = A⇔B →-cong-⇔ C⇔D
→-cong extAC extBD {bijection}   A↔B C↔D = record
  { to         = Equivalence.to   A→C⇔B→D
  ; from       = Equivalence.from A→C⇔B→D
  ; inverse-of = record
    { left-inverse-of  = λ f → extAC λ x → begin
        Inverse.from C↔D ⟨$⟩ (Inverse.to C↔D ⟨$⟩
          f (Inverse.from A↔B ⟨$⟩ (Inverse.to A↔B ⟨$⟩ x)))  ≡⟨ Inverse.left-inverse-of C↔D _ ⟩
        f (Inverse.from A↔B ⟨$⟩ (Inverse.to A↔B ⟨$⟩ x))     ≡⟨ P.cong f $ Inverse.left-inverse-of A↔B x ⟩
        f x                                                 ∎
    ; right-inverse-of = λ f → extBD λ x → begin
        Inverse.to C↔D ⟨$⟩ (Inverse.from C↔D ⟨$⟩
          f (Inverse.to A↔B ⟨$⟩ (Inverse.from A↔B ⟨$⟩ x)))  ≡⟨ Inverse.right-inverse-of C↔D _ ⟩
        f (Inverse.to A↔B ⟨$⟩ (Inverse.from A↔B ⟨$⟩ x))     ≡⟨ P.cong f $ Inverse.right-inverse-of A↔B x ⟩
        f x                                                 ∎
    }
  }
  where
  open P.≡-Reasoning
  A→C⇔B→D = ↔⇒ A↔B →-cong-⇔ ↔⇒ C↔D

------------------------------------------------------------------------
-- ¬_ preserves the symmetric relations

¬-cong-⇔ : ∀ {a b} {A : Set a} {B : Set b} →
           A ⇔ B → (¬ A) ⇔ (¬ B)
¬-cong-⇔ A⇔B = A⇔B →-cong-⇔ (⊥ ∎)
  where open EquationalReasoning

¬-cong : ∀ {a b} → Extensionality a 0ℓ → Extensionality b 0ℓ →
         ∀ {k} {A : Set a} {B : Set b} →
         A ∼[ ⌊ k ⌋ ] B → (¬ A) ∼[ ⌊ k ⌋ ] (¬ B)
¬-cong extA extB A≈B = →-cong extA extB A≈B (⊥ ∎)
  where open EquationalReasoning

------------------------------------------------------------------------
-- _⇔_ preserves _⇔_

-- The type of the following proof is a bit more general.

Related-cong :
  ∀ {k a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
  A ∼[ ⌊ k ⌋ ] B → C ∼[ ⌊ k ⌋ ] D → (A ∼[ ⌊ k ⌋ ] C) ⇔ (B ∼[ ⌊ k ⌋ ] D)
Related-cong {A = A} {B} {C} {D} A≈B C≈D =
  Eq.equivalence (λ A≈C → B  ∼⟨ SK-sym A≈B ⟩
                          A  ∼⟨ A≈C ⟩
                          C  ∼⟨ C≈D ⟩
                          D  ∎)
                 (λ B≈D → A  ∼⟨ A≈B ⟩
                          B  ∼⟨ B≈D ⟩
                          D  ∼⟨ SK-sym C≈D ⟩
                          C  ∎)
  where open EquationalReasoning

------------------------------------------------------------------------
-- A lemma relating True dec and P, where dec : Dec P

True↔ : ∀ {p} {P : Set p}
        (dec : Dec P) → ((p₁ p₂ : P) → p₁ ≡ p₂) → True dec ↔ P
True↔ (yes p) irr = inverse (λ _ → p) (λ _ → _) (λ _ → P.refl) (irr p)
True↔ (no ¬p) _   = inverse (λ()) ¬p (λ()) (⊥-elim ∘ ¬p)

------------------------------------------------------------------------
-- Equality between pairs can be expressed as a pair of equalities

Σ-≡,≡↔≡ : ∀ {a b} {A : Set a} {B : A → Set b} {p₁ p₂ : Σ A B} →
          (∃ λ (p : proj₁ p₁ ≡ proj₁ p₂) →
             P.subst B p (proj₂ p₁) ≡ proj₂ p₂) ↔
          (p₁ ≡ p₂)
Σ-≡,≡↔≡ {A = A} {B} = inverse to from left-inverse-of right-inverse-of
  where
  to : {p₁ p₂ : Σ A B} →
       Σ (proj₁ p₁ ≡ proj₁ p₂)
         (λ p → P.subst B p (proj₂ p₁) ≡ proj₂ p₂) →
       p₁ ≡ p₂
  to (P.refl , P.refl) = P.refl

  from : {p₁ p₂ : Σ A B} →
         p₁ ≡ p₂ →
         Σ (proj₁ p₁ ≡ proj₁ p₂)
           (λ p → P.subst B p (proj₂ p₁) ≡ proj₂ p₂)
  from P.refl = P.refl , P.refl

  left-inverse-of : {p₁ p₂ : Σ A B}
                    (p : Σ (proj₁ p₁ ≡ proj₁ p₂)
                           (λ x → P.subst B x (proj₂ p₁) ≡ proj₂ p₂)) →
                    from (to p) ≡ p
  left-inverse-of (P.refl , P.refl) = P.refl

  right-inverse-of : {p₁ p₂ : Σ A B} (p : p₁ ≡ p₂) → to (from p) ≡ p
  right-inverse-of P.refl = P.refl

×-≡,≡↔≡ : ∀ {a b} {A : Set a} {B : Set b} {p₁ p₂ : A × B} →
          (proj₁ p₁ ≡ proj₁ p₂ × proj₂ p₁ ≡ proj₂ p₂) ↔ p₁ ≡ p₂
×-≡,≡↔≡ {A = A} {B} = inverse to from left-inverse-of right-inverse-of
  where
  to : {p₁ p₂ : A × B} →
       (proj₁ p₁ ≡ proj₁ p₂) × (proj₂ p₁ ≡ proj₂ p₂) → p₁ ≡ p₂
  to (P.refl , P.refl) = P.refl

  from : {p₁ p₂ : A × B} → p₁ ≡ p₂ →
         (proj₁ p₁ ≡ proj₁ p₂) × (proj₂ p₁ ≡ proj₂ p₂)
  from P.refl = P.refl , P.refl

  left-inverse-of : {p₁ p₂ : A × B} →
                    (p : (proj₁ p₁ ≡ proj₁ p₂) × (proj₂ p₁ ≡ proj₂ p₂)) →
                    from (to p) ≡ p
  left-inverse-of (P.refl , P.refl) = P.refl

  right-inverse-of : {p₁ p₂ : A × B} (p : p₁ ≡ p₂) → to (from p) ≡ p
  right-inverse-of P.refl = P.refl

×-≡×≡↔≡,≡ : ∀ {a b} {A : Set a} {B : Set b} {x y} (p : A × B) →
            (x ≡ proj₁ p × y ≡ proj₂ p) ↔ (x , y) ≡ p
×-≡×≡↔≡,≡ {x = x} {y} p = inverse to from from∘to to∘from
   where
   to : (x ≡ proj₁ p × y ≡ proj₂ p) → (x , y) ≡ p
   to = uncurry $ P.cong₂ _,_

   from : (x , y) ≡ p → (x ≡ proj₁ p × y ≡ proj₂ p)
   from = < P.cong proj₁ , P.cong proj₂ >

   from∘to : ∀ v → from (to v) ≡ v
   from∘to (P.refl , P.refl) = P.refl

   to∘from : ∀ v → to (from v) ≡ v
   to∘from P.refl = P.refl

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.17

×-CommutativeMonoid = ×-commutativeMonoid
{-# WARNING_ON_USAGE ×-CommutativeMonoid
"Warning: ×-CommutativeMonoid was deprecated in v0.17.
Please use ×-commutativeMonoid instead."
#-}
⊎-CommutativeMonoid = ⊎-commutativeMonoid
{-# WARNING_ON_USAGE ⊎-CommutativeMonoid
"Warning: ⊎-CommutativeMonoid was deprecated in v0.17.
Please use ⊎-commutativeMonoid instead."
#-}
×⊎-CommutativeSemiring = ×-⊎-commutativeSemiring
{-# WARNING_ON_USAGE ×⊎-CommutativeSemiring
"Warning: ×⊎-CommutativeSemiring was deprecated in v0.17.
Please use ×-⊎-commutativeSemiring instead."
#-}


text:
{-

          Types Summer School 2007

                 Bertinoro
             Aug 19 - 31, 2007

                   Agda

                Ulf Norell

-}

-- This is where the fun begins.
-- Unleashing datatypes, pattern matching and recursion.

module Datatypes where

{-

  Simple datatypes.

-}

-- Let's define natural numbers.

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

-- A simple function.
pred : Nat -> Nat
pred zero    = zero
pred (suc n) = n

-- Now let's do recursion.
_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

infixl 60 _+_

-- An aside on infix operators:
-- Any name containing _ can be used as a mixfix operator.
-- The arguments simply go in place of the _. For instance:

data Bool : Set where
  true  : Bool
  false : Bool

if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true  then x else y = x
-- if false then x else y = y
if_then_else_ false x y = y

{-

  Parameterised datatypes

-}

data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

-- The parameters are implicit arguments to the constructors.
nil : (A : Set) -> List A
nil A = [] {A}

map : {A B : Set} -> (A -> B) -> List A -> List B
map f []        = []
map f (x :: xs) = f x :: map f xs

{-

  Empty datatypes

-}

-- A very useful guy is the empty datatype.
data False : Set where

-- When pattern matching on an element of an empty type, something
-- interesting happens:

elim-False : {A : Set} -> False -> A
elim-False ()  -- Look Ma, no right hand side!

-- The pattern () is called an absurd pattern and matches elements
-- of an empty type.

{-

  What's next?

-}

-- The Curry-Howard isomorphism.
--   CurryHoward.agda


text:
module Oscar.Definition where

{-

unpack : AList m n → Fin m → Term n -- sub
substitute : (Fin m → Term n) → Term m → Term n -- _◃_
substitutes : ∀ N → (Fin m → Term n) → Terms N m → Terms N n -- _◃s_
stepify : (Term m → Term n) → Step m → Step n -- fmapS
collapse : (List ∘ Step) n → Term n → Term n -- _⊹_

Substitist =
Substitunction = Fin m → Term n

Oscar.Data.Proposequality
Oscar.Data.Proposextensequality
Oscar.Data.Term
Oscar.Data.Terms
Oscar.Data.PropositionalEquality
  setoidPropositionalEquality : Set → Setoid
Oscar.Data.IndexedPropositionalEquality
  setoidIndexedPropEq : ∀ {A : Set} {B : A → Set} → ((x : A) → B x) → ((x : A) → B x) → Setoid
Oscar.Data.Substitist

Oscar.Setoid.PropositionalEquality
Oscar.Morphism.Substitist
Oscar.Unification
Oscar.Data.Substitunction
  Substitunction m n = Fin m → Term n
  : Morphism ℕ
  :

Oscar.Definition.Substitist
  : Morphism ℕ
  = alistSetoid
  : IsSemigroupoid
  : Semigroupoid _++_
  : IsCategory
  : Category
  Oscar.Definition.Substitist.internal
    AList
    alistSetoid : ℕ → ℕ → Setoid
    ε = anil
    _++_

-}


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

module Haskell.Prelude where

open import Haskell.Modules.Either public
open import Haskell.Modules.Eq public
open import Haskell.Modules.FunctorApplicativeMonad public
open import Haskell.Modules.ToBool public
------------------------------------------------------------------------------
open import Level
  renaming (suc to ℓ+1; zero to ℓ0; _⊔_ to _ℓ⊔_)
open import Data.Bool
  hiding (not; _≟_; _<_; _<?_; _≤_; _≤?_)
  public
open import Data.List
  hiding (map; filter; lookup; tabulate; foldl; fromMaybe; [_])
  public
import      Data.Nat            as DN
import      Data.Nat.DivMod     as DivMod
import      Data.Nat.Properties as DNP
open import Data.Maybe
  using (Maybe; just; nothing)
  renaming (_>>=_ to _Maybe->>=_)
  public
import      Data.Product as DP
open import Data.Unit.NonEta
  using (Unit; unit)
  public
open import Function
  using (_∘_; id; typeOf; flip; const; _$_)
  public
import      Relation.Binary.PropositionalEquality as PE
  using (_≡_; refl)
import      Relation.Binary.Definitions as BD
import      Relation.Binary             as RB

------------------------------------------------------------------------------

infixl 1 _&_
_&_ = Function._|>_

-- An approximation of Haskell's backtick notation for making infix operators.
-- In Agda, there must be spaces between f and backticks
flip' : _  -- Avoids warning about definition and syntax declaration being in different scopes.
flip' = flip
syntax flip' f = ` f `

------------------------------------------------------------------------------
-- Guard Syntax --
--
-- Example Usage:
--
-- > f : ℕ → ℕ
-- > f x = grd‖ x ≟ℕ 10  ≔ 12
-- >          ‖ otherwise≔ 40 + 2
--
--
-- > g : ℕ ⊎ ℕ → ℕ
-- > g x = case x of λ
-- >     { (inj₁ x) → grd‖ x ≤? 10  ≔ 2 * x
-- >                     ‖ otherwise≔ 42
-- >     ; (inj₂ y) → y
-- >     }
--
-- To type: ‖  -->  \Vert
--          ≔  -->  \:=

infix 3 _≔_
data GuardClause {a}{b}(A : Set a) : Set (a ℓ⊔ ℓ+1 b) where
  _≔_ : {B : Set b}{{ bb : ToBool B }} → B → A → GuardClause A

infix 3 otherwise≔_
data Guards {a}{b}(A : Set a) : Set (a ℓ⊔ ℓ+1 b) where
 otherwise≔_ : A → Guards A
 clause     : GuardClause{a}{b} A → Guards{a}{b} A → Guards A

infixr 2 _‖_
_‖_ : ∀{a}{b}{A : Set a} → GuardClause{a}{b} A → Guards A → Guards A
_‖_ = clause

infix 1 grd‖_
grd‖_ : ∀{a}{b}{A : Set a} → Guards{a}{b} A → A
grd‖_ (otherwise≔ a) = a
grd‖_ (clause (b ≔ a) g)  = if toBool b then a else (grd‖ g)

------------------------------------------------------------------------------
-- List

infixl 9 _!?_
_!?_ : {A : Set} → List A → DN.ℕ → Maybe A
[]       !?         _   = nothing
(x ∷ _ ) !?         0   = just x
(_ ∷ xs) !? (DN.suc n)  = xs !? n

find' : ∀ {A B : Set} → (A → Maybe B) → List A → Maybe B
find' f      []  = nothing
find' f (a ∷ xs) = Data.Maybe.maybe′ f (find' f xs) (just a)

foldl' = Data.List.foldl

------------------------------------------------------------------------------
-- Maybe

maybe : ∀ {A B : Set} → B → (A → B) → Maybe A → B
maybe b a→b = Data.Maybe.maybe′ a→b b

------------------------------------------------------------------------------
-- Nat

div = DivMod._/_

data Ordering : Set where
  LT EQ GT : Ordering

compare : DN.ℕ → DN.ℕ → Ordering
compare m n
  with DNP.<-cmp m n
... | BD.tri< a ¬b ¬c = LT
... | BD.tri≈ ¬a b ¬c = EQ
... | BD.tri> ¬a ¬b c = GT

------------------------------------------------------------------------------
-- Product

fst = DP.proj₁
snd = DP.proj₂

------------------------------------------------------------------------------
-- Monad

foldlM : ∀ {ℓ₁ ℓ₂} {A B : Set ℓ₁} {M : Set ℓ₁ → Set ℓ₂} ⦃ _ : Monad M ⦄
       → (B → A → M B) → B → List A → M B
foldlM _ z      []  = pure z
foldlM f z (x ∷ xs) = do
  z' ← f z x
  foldlM f z' xs

foldrM : ∀ {ℓ₁ ℓ₂} {A B : Set ℓ₁} {M : Set ℓ₁ → Set ℓ₂} ⦃ _ : Monad M ⦄
       → (A → B → M B) → B → List A → M B
foldrM _ b      []  = return b
foldrM f b (a ∷ as) = foldrM f b as >>= f a

foldM = foldlM

foldM_ : {A B : Set} {M : Set → Set} ⦃ _ : Monad M ⦄ → (B → A → M B) → B → List A → M Unit
foldM_ f a xs = foldlM f a xs >> pure unit

fromMaybeM : ∀ {ℓ} {A : Set} {m : Set → Set ℓ} ⦃ _ : Monad m ⦄ → m A → m (Maybe A) → m A
fromMaybeM ma mma = do
  mma >>= λ where
    nothing  → ma
    (just a) → pure a

-- NOTE: because 'forM_' is defined above, it is necessary to
-- call 'forM' with parenthesis (e.g., recursive call in definition)
-- to disambiguate it for the Agda parser.
forM  : ∀ {ℓ} {A B : Set} {M : Set → Set ℓ} ⦃ _ : Monad M ⦄ → List A → (A → M B) → M (List B)
forM      []  _ = return []
forM (x ∷ xs) f = do
  fx  ← f x
  fxs ← (forM) xs f
  return (fx ∷ fxs)

forM_ : ∀ {ℓ} {A B : Set} {M : Set → Set ℓ} ⦃ _ : Monad M ⦄ → List A → (A → M B) → M Unit
forM_      []  _ = return unit
forM_ (x ∷ xs) f = f x >> forM_ xs f


text:
module Ex6AgdaSetup where

{- This file contains all the basic types you need for the editor. You should
   read and understand the Agda in this file, but not bother too much about
   the funny compiler directives. -}

open import CS410-Prelude
open import CS410-Nat

record _**_ (S T : Set) : Set where
  constructor _,_
  field
    outl : S
    outr : T
open _**_
{-# COMPILED_DATA _**_ (,) (,) #-}
infixr 4 _**_ _,_

_<=_ : Nat -> Nat -> Two
zero   <=  y      = tt
suc x  <=  zero   = ff
suc x  <=  suc y  = x <= y

_++_ : {A : Set} -> List A -> List A -> List A
[]         ++ ys = ys
(x :: xs)  ++ ys = x :: (xs ++ ys)

{- Here are backward lists, which are useful when the closest element is
   conceptually at the right end. They aren't really crucial as you could use
   ordinary lists but think of the data as being reversed, but I prefer to
   keep my thinking straight and use data which look like what I have in mind. -}

data Bwd (X : Set) : Set where
  []    : Bwd X
  _<:_  : Bwd X -> X -> Bwd X
infixl 3 _<:_

{- You will need access to characters, imported from Haskell. You can write
   character literals like 'c'. You also get strings, with String literals like
   "fred" -}

postulate       -- Haskell has a monad for doing IO, which we use at the top level
  IO      : Set -> Set
  return  : {A : Set} -> A -> IO A
  _>>=_   : {A B : Set} -> IO A -> (A -> IO B) -> IO B
infixl 1 _>>=_
{-# BUILTIN IO IO #-}
{-# COMPILED_TYPE IO IO #-}
{-# COMPILED return (\ _ -> return)    #-}
{-# COMPILED _>>=_  (\ _ _ -> (>>=)) #-}

{- Here's the characterization of keys I give you -}
data Direction : Set where up down left right : Direction
data Modifier : Set where normal shift control : Modifier
data Key : Set where
  char       : Char -> Key
  arrow      : Modifier -> Direction -> Key
  enter      : Key
  backspace  : Key
  delete     : Key
  escape     : Key
  tab        : Key
data Event : Set where
  key     : (k : Key) -> Event
  resize  : (w h : Nat) -> Event

{- This type classifies the difference between two editor states. -}
data Change : Set where
  allQuiet    : Change      -- the buffer should be exactly the same
  cursorMove  : Change      -- the cursor has moved but the text is the same
  lineEdit    : Change      -- only the text on the current line has changed
  bigChange   : Change      -- goodness knows!

{- This type collects the things you're allowed to do with the text window. -}
data Action : Set where
  goRowCol : Nat -> Nat -> Action    -- send the cursor somewhere
  sendText : List Char -> Action     -- send some text
  move     : Direction -> Nat -> Action  -- which way and how much
  fgText   : Colour -> Action
  bgText   : Colour -> Action

{- I wire all of that stuff up to its Haskell counterpart. -}
{-# IMPORT ANSIEscapes #-}
{-# IMPORT HaskellSetup #-}
{-# COMPILED_DATA Direction
      ANSIEscapes.Dir
      ANSIEscapes.DU ANSIEscapes.DD ANSIEscapes.DL ANSIEscapes.DR #-}
{-# COMPILED_DATA Modifier
      HaskellSetup.Modifier
      HaskellSetup.Normal HaskellSetup.Shift HaskellSetup.Control #-}
{-# COMPILED_DATA Key
      HaskellSetup.Key
      HaskellSetup.Char HaskellSetup.Arrow HaskellSetup.Enter
      HaskellSetup.Backspace HaskellSetup.Delete HaskellSetup.Escape
      HaskellSetup.Tab #-}
{-# COMPILED_DATA Event
      HaskellSetup.Event
      HaskellSetup.Key HaskellSetup.Resize #-}
{-# COMPILED_DATA Change
      HaskellSetup.Change
      HaskellSetup.AllQuiet HaskellSetup.CursorMove HaskellSetup.LineEdit
      HaskellSetup.BigChange #-}
{-# COMPILED_DATA Action HaskellSetup.Action
      HaskellSetup.GoRowCol HaskellSetup.SendText HaskellSetup.Move
      HaskellSetup.FgText HaskellSetup.BgText #-}

{- This is the bit of code I wrote to animate your code. -}
postulate
  mainLoop : {B : Set} ->             -- buffer type
    -- INITIALIZER
    (List (List Char) -> B) ->        -- make a buffer from some lines of text
    -- KEYSTROKE HANDLER
    (Key -> B ->                      -- keystroke and buffer in
     Change ** B) ->                 -- change report and buffer out
    -- RENDERER
    ((Nat ** Nat) ->                 -- height and width of screen
     (Nat ** Nat) ->                 -- top line number, left column number
     (Change ** B) ->           -- change report and buffer to render
     (List Action **                 -- how to update the display
      (Nat ** Nat))) ->              -- new top line number, left column number
    -- PUT 'EM TOGETHER AND YOU'VE GOT AN EDITOR!
    IO One
{-# COMPILED mainLoop (\ _ -> HaskellSetup.mainLoop) #-}

{- You can use this to put noisy debug messages in Agda code. So
      trace "fred" tt
   evaluates to tt, but prints "fred" in the process. -}
postulate
  trace : {A : Set} -> String -> A -> A
{-# IMPORT Debug.Trace #-}
{-# COMPILED trace (\ _ -> Debug.Trace.trace) #-}

{- You can use this to print an error message when you don't know what else to do.
   It's very useful for filling in unfinished holes to persuade the compiler to
   compile your code even though it isn't finished: you get an error if you try
   to run a missing bit. -}
postulate
  error : {A : Set} -> String -> A
{-# COMPILED error (\ _ -> error) #-}

{- Equality -}
{- x == y is a type whenever x and y are values in the same type -}
{-
data _==_ {X : Set}(x : X) : X -> Set where
  refl : x == x  -- and x == y has a constructor only when y actually is x!
infixl 1 _==_
-- {-# BUILTIN EQUALITY _==_ #-}
-- {-# BUILTIN REFL refl #-}
{-# COMPILED_DATA _==_ HaskellSetup.EQ HaskellSetup.Refl #-}

within_turn_into_because_ :
   {X Y : Set}(f : X -> Y)(x x' : X) ->
   x == x' -> f x == f x'
within f turn x into .x because refl = refl
                     -- the dot tells Agda that *only* x can go there

symmetry : {X : Set}{x x' : X} -> x == x' -> x' == x
symmetry refl = refl

transitivity : {X : Set}{x0 x1 x2 : X} -> x0 == x1 -> x1 == x2 -> x0 == x2
transitivity refl refl = refl
-}

within_turn_into_because_ :
    {X Y : Set}(f : X -> Y)(x x' : X) ->
    x == x' -> f x == f x'
within f turn x into .x because refl = refl

{-
postulate
  _==_ : {X : Set} -> X -> X -> Set   -- the evidence that two X-values are equal
  refl : {X : Set}{x : X} -> x == x
  symmetry : {X : Set}{x x' : X} -> x == x' -> x' == x
  transitivity : {X : Set}{x0 x1 x2 : X} -> x0 == x1 -> x1 == x2 -> x0 == x2
  within_turn_into_because_ :
    {X Y : Set}(f : X -> Y)(x x' : X) ->
    x == x' -> f x == f x'
infix 1 _==_

{-# COMPILED_TYPE _==_ HaskellSetup.EQ #-}

{- Here's an example. -}

additionAssociative : (x y z : Nat) -> (x + y) + z == x + (y + z)
additionAssociative zero y z    = refl
additionAssociative (suc x) y z
  = within suc turn ((x + y) + z) into (x + (y + z))
      because additionAssociative x y z
-}