text:
{-# OPTIONS --without-K #-}

open import Base
open import Spaces.Interval

module Spaces.IntervalProps where

bool-split : bool {zero} → Set
bool-split true = unit
bool-split false = ⊥

-- If [bool] is contractible, then [true ≡ false]
bool-contr-path : is-contr (bool {zero}) → true ≡ false
bool-contr-path (x , f) = (f true) ∘ ! (f false)

-- But if [true ≡ false], then [⊥]
bool-is-not-contr : ¬ (is-contr bool)
bool-is-not-contr f = transport bool-split (bool-contr-path f) tt

I-is-contr : is-contr I
I-is-contr =
  (zer , I-rec (λ (t : I) → t ≡ zer) refl (! seg)
                (trans-id≡cst seg refl ∘ refl-right-unit (! seg)))

interval-implies-funext : ∀ {i j} (A : Set i) (B : Set j) (f g : A → B)
  (h : (x : A) → f x ≡ g x) → f ≡ g
interval-implies-funext A B f g h =
  ap (λ i a → I-rec-nondep _ (f a) (g a) (h a) i) seg

ext: agda

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- Giving /lift \phi/ the the first hole TWICE (the first time you get an type error), causes the following internal error:

--   An internal error has occurred. Please report this as a bug.
--   Location of the error:
--   src/full/Agda/TypeChecking/Reduce/Monad.hs:118

------------------------------------------------------------------------
-- Library

infixr 9 _∘_

_∘_ : ∀ {a b c}
        {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
        (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
        ((x : A) → C (g x))
f ∘ g = λ x → f (g x)

data ⊥ : Set where

data _⊎_ (A : Set) (B : Set) : Set where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

[_,_] : ∀ {A : Set} {B : Set} {C : A ⊎ B → Set} →
        ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
        ((x : A ⊎ B) → C x)
[ f , g ] (inj₁ x) = f x
[ f , g ] (inj₂ y) = g y

[_,_]₁ : ∀ {A : Set} {B : Set} {C : A ⊎ B → Set₁} →
        ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
        ((x : A ⊎ B) → C x)
[ f , g ]₁ (inj₁ x) = f x
[ f , g ]₁ (inj₂ y) = g y

record Σ (X : Set) (Y : X → Set) : Set where
  constructor _,_
  field
    proj₁ : X
    proj₂ : Y proj₁

open Σ public

_×_ : Set → Set → Set
X × Y = Σ X λ _ → Y

data _≡_ {X : Set} (x : X) : X → Set where
  refl : x ≡ x

subst : ∀ {A} (P : A → Set) {x y} → x ≡ y → P x → P y
subst P refl p = p

Pow : Set → Set₁
Pow X = X → Set

_∈_ : ∀ {X} → X → Pow X → Set
x ∈ P = P x

infix 4 _⊆_
_⊆_ : ∀ {X} → Pow X → Pow X → Set
P ⊆ Q = ∀ {x} → x ∈ P → x ∈ Q

_∪_ : ∀ {X} → Pow X → Pow X → Pow X
P ∪ Q = λ x → P x ⊎ Q x

_⇒_ : ∀ {X} → Pow X → Pow X → Pow X
P ⇒ Q = λ x → x ∈ P → x ∈ Q

record _▷_ (I O : Set) : Set₁ where
  constructor _◃_/_
  field
    Parameter  : (o : O) → Set
    Arity      : ∀ {o} (p : Parameter o) → Set
    input      : ∀ {o} (p : Parameter o) (a : Arity p) → I

open _▷_ public

Sig = λ I → I ▷ I

⟦_⟧ : ∀ {I O} → I ▷ O → (Pow I → Pow O)
⟦ P ◃ A / s ⟧ X o = Σ (P o) λ p → ((a : A p) → X (s p a))

data μ {I} (Ω : Sig I) : Pow I where
  sup : ⟦ Ω ⟧ (μ Ω) ⊆ μ Ω

const^C : ∀ {I O} → Pow O → I ▷ O
const^C X = X ◃ (λ _ → ⊥) / λ x ()

_⊎^C_ : ∀ {I O} → I ▷ O → I ▷ O → I ▷ O
(P₁ ◃ A₁ / s₁) ⊎^C (P₂ ◃ A₂ / s₂) = (P₁ ∪ P₂) ◃ [ A₁ , A₂ ]₁ / [ s₁ , s₂ ]

_⊙^C_ : ∀ {I J} → I ▷ I → J ▷ J → (I × J) ▷ (I × J)
(P₁ ◃ A₁ / s₁) ⊙^C (P₂ ◃ A₂ / s₂) = (λ { (i , j) → P₁ i ⊎ P₂ j })
  ◃ [ A₁ , A₂ ]₁
  / (λ  { {_ , j} (inj₁ p₁) a₁ → s₁ p₁ a₁ , j
        ; {i , _} (inj₂ p₂) a₂ → i , s₂ p₂ a₂
        })

_⋆^C_ : ∀ {O} → O ▷ O → Pow O → O ▷ O
Σ ⋆^C X = const^C X ⊎^C Σ

_⋆_ : ∀ {O} → O ▷ O → Pow O → Pow O
Σ ⋆ X = μ (Σ ⋆^C X)

Alg : ∀ {I} → Sig I → Pow I → Set
Alg Ω X = ⟦ Ω ⟧ X ⊆ X

do : ∀ {O} {Σ : O ▷ O} {X} → Alg Σ (Σ ⋆ X)
do (p , k) = sup (inj₂ p , k)

Hom : ∀ {I J} → Sig (I × J) → Pow (I × J) → Pow I → Sig J → Pow J → Set
Hom Ω U V Ψ W = Alg  (const^C U ⊎^C Ω)
                     ((V ∘ proj₁) ⇒ ((Ψ ⋆ W) ∘ proj₂))

_⋊_ : ∀ {I O} (C : I ▷ O) Z → (I × Z) ▷ (O × Z)
(P ◃ A / s) ⋊ Z = (P ∘ proj₁) ◃ A / λ {oz} p a → s p a , proj₂ oz

record ContainerMorphism
    {I₁ I₂ O₁ O₂}
    (C₁ : I₁ ▷ O₁) (C₂ : I₂ ▷ O₂)
    (f : I₁ → I₂) (g : O₁ → O₂)
    (_∼_ : I₂ → I₂ → Set) (_≈_ : Set → Set → Set)
    (_·_ : ∀ {A B} → A ≈ B → A → B) : Set where
  field
    parameter  : Parameter C₁ ⊆ Parameter C₂ ∘ g
    arity      : ∀ {o} {p₁ : Parameter C₁ o} →
                 Arity C₂ (parameter p₁) ≈ Arity C₁ p₁
    coherent   : ∀ {o} {p₁ : Parameter C₁ o} {a₂ : Arity C₂ (parameter p₁)} →
                 f (input C₁ p₁ (arity · a₂)) ∼ input C₂ (parameter p₁) a₂

open ContainerMorphism public

_⇛[_/_]_ : ∀ {I₁ I₂ O₁ O₂} → I₁ ▷ O₁ → (I₁ → I₂) → (O₁ → O₂) →
           I₂ ▷ O₂ → Set
C₁ ⇛[ f / g ] C₂ = ContainerMorphism C₁ C₂ f g _≡_  (λ R₂ R₁ → R₂ → R₁)
                                                    (λ f x → f x)

_⇛[_]_ : ∀ {I J} → I ▷ I → (I → J) → J ▷ J → Set
C₁ ⇛[ f ] C₂ = C₁ ⇛[ f / f ] C₂

⟪_⟫ : ∀ {I J} {C₁ : I ▷ I} {C₂ : J ▷ J} {f : I → J} →
      C₁ ⇛[ f ] C₂ → (X : Pow J) → ⟦ C₁ ⟧ (X ∘ f) ⊆ ⟦ C₂ ⟧ X ∘ f
⟪ m ⟫ X (c , k) = parameter m c , λ a₂ →
  subst X (coherent m) (k (arity m a₂))

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

weaken : ∀ {I J} {Ω : Sig I} {Ψ : Sig J} {X : Pow J} {f : I → J} →
         Alg Ψ X → Ω ⇛[ f ] Ψ → Alg Ω (X ∘ f)
weaken {X = X} φ m (p , k) = φ (⟪ m ⟫ X (p , k))

lift : ∀ {I J} {Ω : Sig I} {U : Pow (I × J)} {V : Pow I} {Ψ : Sig J} {W : Pow J} →
       Hom (Ω ⋊ J)    U V Ψ W →
       Hom (Ω ⊙^C Ψ)  U V Ψ W
lift φ (inj₁ u , _)         = φ (inj₁ u , λ ())
lift φ (inj₂ (inj₁ p) , k)  = φ (inj₂ p , k)
lift φ (inj₂ (inj₂ p) , k)  = λ v → do (p , λ a → k a v)

handle : ∀ {I J K} {Ω : Sig I} {Ω′ : Sig J} {Ω″ : Sig K}
         {U : Pow (J × K)} {V : Pow J} {W : Pow K} {f : I → J × K} →
         Hom (Ω′ ⋊ K) U V Ω″ W → Ω ⇛[ f ] (Ω′ ⊙^C Ω″) →
         ∀ {i} → i ∈ (Ω ⋆ (U ∘ f)) → let (j , k) = f i in
         j ∈ V → k ∈ (Ω″ ⋆ W)
handle φ m (sup (inj₁ u  , _))  v = φ (inj₁ u , λ ()) v
handle φ m (sup (inj₂ p  , k))  v = weaken {!lift φ!} {!!} {!!}

-- Expected outcome:
-- giving "lift φ" twice should give the same error twice.


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

module meta-cedille where

open import Data.String using (toList)
open import IO using (Main; run)
open import Monads.Except
open import Monads.ExceptT

open import Prelude
open import Prelude.Strings

open import Parse.Generate
open import Parse.TreeConvert
open import Bootstrap.InitEnv

open import CoreTheory
open import Execution

record EvalFlags : Set where
  field
    printAnything : Bool
    printInfo     : Bool -- print the results generated by a top level command

initFlagsDefault : EvalFlags
initFlagsDefault = record
  { printAnything = false
  ; printInfo     = false
  }

runtimeFlagsDefault : EvalFlags
runtimeFlagsDefault = record
  { printAnything = true
  ; printInfo     = true
  }

eval : MetaContext → String → EvalFlags → IO (MetaContext × Bool)
eval Γ ""    _     = return (Γ , true)
eval Γ input flags = let open EvalFlags flags in do
  (s , (inj₂ (out , _))) ← execute (parseAndExecute input) Γ
    where (_ , (inj₁ err)) → putStrErr err >> return (Γ , false)
  if printAnything ∧ printInfo
    then putStr $ unlines out
    else return tt
  return (contextFromState s , true)

rep : MetaContext → IO MetaContext
rep Γ = do
  putStr "\nλ> "
  flushStdout
  input ← getLine
  proj₁ <$> eval Γ input runtimeFlagsDefault

{-# NON_TERMINATING #-}
loop : ∀ {a} {A : Set a} → A → (A → IO A) → IO ⊤
loop start f = do
  res ← f start
  loop res f

repl : MetaContext → IO ⊤
repl start = loop start rep

record Options : Set where
  field
    startRepl   : Bool
    importFiles : List String
    verbose     : Bool
    showHelp    : Bool

defaultOptions : Options
defaultOptions = record
  { startRepl   = true
  ; importFiles = []
  ; verbose     = false
  ; showHelp    = false }

{-# TERMINATING #-}
readOptions : ExceptT IO String Options
readOptions = do
  args ← getArgs
  return $ readArgs args defaultOptions
  where
    argumentDec : Decidable _
    argumentDec s = false ≟ isInit "--" (toList s)

    readArgs : List String → Options → Except String Options
    readArgs [] current = return current
    readArgs ("--no-repl" ∷ input) current = readArgs input record current { startRepl = false }
    readArgs ("--verbose" ∷ input) current = readArgs input record current { verbose = true }
    readArgs ("--help"    ∷ input) current = readArgs input record current { showHelp = true }
    readArgs ("--load"    ∷ input) current with span argumentDec input
    ... | (files , rest)                   = readArgs rest record current { importFiles = files }
    readArgs (x           ∷ input) current = inj₁ ("Unknown option: " + x)

helpString : String
helpString = "Usage: meta-cedille [OPTIONS...]\n" +
  concat ((λ { (fst , snd) → "    --" + padRight ' ' padLength fst + snd + "\n" }) <$> helpTable)
  where
    helpTable : List (String × String)
    helpTable =
      ("help"         , "Show this help") ∷
      ("load [FILES]" , "Loads a list of files before starting the REPL") ∷
      ("verbose"      , "Print supressed output before starting the REPL") ∷
      ("no-repl"      , "Exits the program when the REPL would start") ∷ []

    padLength : ℕ
    padLength = 4 + maximum (Data.String.length ∘ proj₁ <$> helpTable)

initGrammar : Grammar
initGrammar = from-inj₂ $ preCoreGrammar {{Except-Monad}} {{Except-MonadExcept}}

bootstrapMetaContext : MetaContext
bootstrapMetaContext =
  emptyGlobalContext , record { grammar = initGrammar ; namespace = "" ; evaluator = Sort-A □ }

loadFiles : MetaContext → EvalFlags → List String → IO (MetaContext × Bool)
loadFiles context flags []    = return (context , true)
loadFiles context flags files =
  eval context (concat $ map (λ file → "import " + file + ".") files) flags

main : Main
main = run $ do
  (inj₂ o) ← readOptions
    where (inj₁ x) → putStr x
  let open Options o in
    if showHelp then putStr helpString else do
      (init , successInit) ← eval bootstrapMetaContext initEnv initFlagsDefault
      let initFlags = if verbose then runtimeFlagsDefault else initFlagsDefault
      (postLoad , successLoad) ← loadFiles init initFlags importFiles
      if startRepl
        then repl postLoad
        else if successInit ∧ successLoad
          then exitSuccess
          else exitFailure

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
------------------------------------------------------------------------
-- Functors and natural transformations (for 1-categories)
------------------------------------------------------------------------

-- The code is based on the presentation in the HoTT book (but might
-- not follow it exactly).

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

open import Equality

module Functor
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

import Surjection

open import Bijection eq hiding (id; _∘_; inverse; step-↔; finally-↔)
open import Category eq
open Derived-definitions-and-properties eq
open import Equivalence eq as Eq using (_≃_; module _≃_; ↔⇒≃)
open import Function-universe eq hiding (id; _∘_)
open import H-level eq
open import H-level.Closure eq
open import Logical-equivalence using (_⇔_; module _⇔_)
open import Prelude as P hiding (id; _^_)

------------------------------------------------------------------------
-- Functors

Functor : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
          Precategory ℓ₁ ℓ₂ → Precategory ℓ₃ ℓ₄ → Type _
Functor C D =
  -- Object map.
  ∃ λ (F₀ : Obj C → Obj D) →

  -- Morphism map.
  ∃ λ (F : ∀ {X Y} → Hom C X Y → Hom D (F₀ X) (F₀ Y)) →

  -- F should be homomorphic with respect to identity and composition.
  (∀ {X} → F (id C {X = X}) ≡ id D) ×
  (∀ {X Y Z} {f : Hom C X Y} {g : Hom C Y Z} →
     F (_∙_ C g f) ≡ _∙_ D (F g) (F f))

  where open Precategory

-- A wrapper.

infix 4 _⇨_

record _⇨_ {ℓ₁ ℓ₂ ℓ₃ ℓ₄}
           (C : Precategory ℓ₁ ℓ₂) (D : Precategory ℓ₃ ℓ₄) :
           Type (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
  field
    functor : Functor C D

  open Precategory

  infixr 10 _⊚_ _⊙_

  -- Object map.

  _⊚_ : Obj C → Obj D
  _⊚_ = proj₁ functor

  -- Morphism map.

  _⊙_ : ∀ {X Y} → Hom C X Y → Hom D (_⊚_ X) (_⊚_ Y)
  _⊙_ = proj₁ (proj₂ functor)

  -- The morphism map is homomorphic with respect to identity.

  ⊙-id : ∀ {X} → _⊙_ (id C {X = X}) ≡ id D
  ⊙-id = proj₁ (proj₂ (proj₂ functor))

  -- The morphism map is homomorphic with respect to composition.

  ⊙-∙ : ∀ {X Y Z} {f : Hom C X Y} {g : Hom C Y Z} →
        _⊙_ (_∙_ C g f) ≡ _∙_ D (_⊙_ g) (_⊙_ f)
  ⊙-∙ = proj₂ (proj₂ (proj₂ functor))

open _⇨_ public

private
 module Dummy₁ where
  abstract

   -- The homomorphism properties are propositional (assuming
   -- extensionality).

   functor-properties-propositional :
     ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
     Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
     {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄}
     (F : C ⇨ D) → let open Precategory in

     Is-proposition ((∀ {X} → F ⊙ id C {X = X} ≡ id D) ×
                     (∀ {X Y Z} {f : Hom C X Y} {g : Hom C Y Z} →
                      F ⊙ (_∙_ C g f) ≡ _∙_ D (F ⊙ g) (F ⊙ f)))

   functor-properties-propositional {ℓ₁} {ℓ₂} ext {D = D} _ = ×-closure 1
     (implicit-Π-closure (lower-extensionality ℓ₂ (ℓ₁ ⊔ ℓ₂) ext) 1 λ _ →
      Precategory.Hom-is-set D)
     (implicit-Π-closure (lower-extensionality ℓ₂ lzero     ext) 1 λ _ →
      implicit-Π-closure (lower-extensionality ℓ₂ lzero     ext) 1 λ _ →
      implicit-Π-closure (lower-extensionality ℓ₂ ℓ₁        ext) 1 λ _ →
      implicit-Π-closure (lower-extensionality ℓ₁ ℓ₁        ext) 1 λ _ →
      implicit-Π-closure (lower-extensionality ℓ₁ (ℓ₁ ⊔ ℓ₂) ext) 1 λ _ →
      Precategory.Hom-is-set D)

open Dummy₁ public

private
 module Dummy₂ where
  abstract

   -- Functor equality is equivalent to equality of the corresponding
   -- maps, suitably transported (assuming extensionality).

   equality-characterisation⇨ :
     ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
     Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
     {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄} {F G : C ⇨ D} →
     let open Precategory in

     (F ≡ G)

       ≃

     ∃ λ (⊚F≡⊚G : _⊚_ F ≡ _⊚_ G) →
         _≡_ {A = ∀ {X Y} → Hom C X Y → Hom D (G ⊚ X) (G ⊚ Y)}
             (subst (λ F → ∀ {X Y} → Hom C X Y → Hom D (F X) (F Y))
                    ⊚F≡⊚G (_⊙_ F))
             (_⊙_ G)

   equality-characterisation⇨ ext {C} {D} {F} {G} =
     let P : (Obj C → Obj D) → Type _
         P = λ F₀ → ∀ {X Y} → Hom C X Y → Hom D (F₀ X) (F₀ Y)

         Q : ∃ P → Type _
         Q = λ { (F₀ , F) → (∀ {X} → F (id C {X = X}) ≡ id D) ×
                            (∀ {X Y Z} {f : Hom C X Y} {g : Hom C Y Z} →
                               F (_∙_ C g f) ≡ _∙_ D (F g) (F f)) }
     in

     (F ≡ G)                                                              ↝⟨ ↔⇒≃ record
                                                                               { surjection = record
                                                                                { logical-equivalence = record
                                                                                { to   = cong functor
                                                                                ; from = cong λ f → record { functor = f }
                                                                                }
                                                                                ; right-inverse-of = λ _ → trans (cong-∘ _ _ _) (sym $ cong-id _)
                                                                                }
                                                                               ; left-inverse-of = λ _ → trans (cong-∘ _ _ _) (sym $ cong-id _)
                                                                               } ⟩
     (functor F ≡ functor G)                                              ↔⟨ inverse Σ-≡,≡↔≡ ⟩

     (∃ λ (⊚F≡⊚G : _⊚_ F ≡ _⊚_ G) →
          subst (λ F₀ → ∃ λ (F : P F₀) → Q (F₀ , F)) ⊚F≡⊚G
                (proj₂ $ functor F) ≡ proj₂ (functor G))                  ↝⟨ ∃-cong (λ ⊚F≡⊚G → ≡⇒↝ _ $ cong (λ x → x ≡ proj₂ (functor G)) $
                                                                               push-subst-pair P Q) ⟩
     (∃ λ (⊚F≡⊚G : _⊚_ F ≡ _⊚_ G) →
          _≡_ {A = ∃ λ (H : P (_⊚_ G)) → Q (_⊚_ G , H)}
          ( subst P ⊚F≡⊚G (_⊙_ F)
          , subst Q (Σ-≡,≡→≡ ⊚F≡⊚G (refl _)) (proj₂ $ proj₂ $ functor F)
          )
          (proj₂ (functor G)))                                            ↔⟨ ∃-cong (λ ⊚F≡⊚G → inverse $
                                                                               ignore-propositional-component
                                                                                (functor-properties-propositional ext G)) ⟩□
     (∃ λ (⊚F≡⊚G : _⊚_ F ≡ _⊚_ G) →
          (λ {_ _} → subst P ⊚F≡⊚G (_⊙_ F)) ≡ _⊙_ G)                      □

     where open Precategory

   -- Some simplification lemmas.

   proj₁-to-equality-characterisation⇨ :
     ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄}
     (ext : Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄))
     {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄} {F G : C ⇨ D} →
     let open Precategory in
     (F≡G : F ≡ G) →

     proj₁ (_≃_.to (equality-characterisation⇨ ext {F = F} {G = G}) F≡G)
       ≡
     cong _⊚_ F≡G

   proj₁-to-equality-characterisation⇨ ext F≡G =
     proj₁ (_≃_.to (equality-characterisation⇨ ext) F≡G)  ≡⟨ proj₁-Σ-≡,≡←≡ _ ⟩
     cong proj₁ (cong functor F≡G)                        ≡⟨ cong-∘ _ _ _ ⟩∎
     cong _⊚_ F≡G                                         ∎

   cong-⊚-from-equality-characterisation⇨ :
     ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄}
     (ext : Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄))
     {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄} {F G : C ⇨ D} →
     let open Precategory in
     (⊚F≡⊚G : _⊚_ F ≡ _⊚_ G) →
     (⊙F≡⊙G : _≡_ {A = ∀ {X Y} → Hom C X Y → Hom D (G ⊚ X) (G ⊚ Y)}
                  (subst (λ F → ∀ {X Y} → Hom C X Y → Hom D (F X) (F Y))
                         ⊚F≡⊚G (_⊙_ F))
                  (_⊙_ G)) →

     cong _⊚_ (_≃_.from (equality-characterisation⇨ ext {F = F} {G = G})
                        (⊚F≡⊚G , ⊙F≡⊙G))
       ≡
     ⊚F≡⊚G

   cong-⊚-from-equality-characterisation⇨ ext {F = F} {G} ⊚F≡⊚G ⊙F≡⊙G =
     cong _⊚_ (_≃_.from (equality-characterisation⇨ ext {F = F} {G = G})
                        (⊚F≡⊚G , ⊙F≡⊙G))                                  ≡⟨ cong-∘ _ _ _ ⟩

     cong proj₁ (Σ-≡,≡→≡ ⊚F≡⊚G _)                                         ≡⟨ proj₁-Σ-≡,≡→≡ _ _ ⟩∎

     ⊚F≡⊚G                                                                ∎

open Dummy₂ public

private
 module Dummy₃ where
  abstract

   -- Another equality characterisation lemma.

   equality-characterisation≡⇨ :
     ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
     Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
     {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄} {F G : C ⇨ D}
     {eq₁ eq₂ : F ≡ G} →
     (eq₁ ≡ eq₂) ≃ (cong _⊚_ eq₁ ≡ cong _⊚_ eq₂)
   equality-characterisation≡⇨ {ℓ₁} {ℓ₂} ext {D = D} {eq₁ = eq₁} {eq₂} =
     eq₁ ≡ eq₂                                              ↝⟨ inverse $ Eq.≃-≡ (equality-characterisation⇨ ext) ⟩

     _≃_.to (equality-characterisation⇨ ext) eq₁ ≡
     _≃_.to (equality-characterisation⇨ ext) eq₂            ↔⟨ inverse $ ignore-propositional-component
                                                                 (implicit-Π-closure (lower-extensionality ℓ₂ lzero     ext) 2 λ _ →
                                                                  implicit-Π-closure (lower-extensionality ℓ₂ ℓ₁        ext) 2 λ _ →
                                                                  Π-closure          (lower-extensionality ℓ₁ (ℓ₁ ⊔ ℓ₂) ext) 2 λ _ →
                                                                  Precategory.Hom-is-set D) ⟩
     proj₁ (_≃_.to (equality-characterisation⇨ ext) eq₁) ≡
     proj₁ (_≃_.to (equality-characterisation⇨ ext) eq₂)    ↝⟨ ≡⇒↝ _ (cong₂ _≡_ (proj₁-to-equality-characterisation⇨ _ _)
                                                                                (proj₁-to-equality-characterisation⇨ _ _)) ⟩□
     cong _⊚_ eq₁ ≡ cong _⊚_ eq₂                            □

open Dummy₃ public

-- Identity functor.

id⇨ : ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂} → C ⇨ C
functor id⇨ = P.id , P.id , refl _ , refl _

-- Composition of functors.

infixr 10 _∙⇨_

_∙⇨_ : ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
         {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄}
         {ℓ₅ ℓ₆} {E : Precategory ℓ₅ ℓ₆} →
       D ⇨ E → C ⇨ D → C ⇨ E
functor (_∙⇨_ {C = C} {D = D} {E = E} G F) =
  (G ⊚_) ∘ (F ⊚_) ,
  (G ⊙_) ∘ (F ⊙_) ,
  (G ⊙ F ⊙ id C              ≡⟨ cong (G ⊙_) $ ⊙-id F ⟩
   G ⊙ id D                  ≡⟨ ⊙-id G ⟩∎
   id E                      ∎) ,
  (λ {_ _ _ f g} →
     G ⊙ F ⊙ _∙_ C g f              ≡⟨ cong (G ⊙_) $ ⊙-∙ F ⟩
     G ⊙ _∙_ D (F ⊙ g) (F ⊙ f)      ≡⟨ ⊙-∙ G ⟩∎
     _∙_ E (G ⊙ F ⊙ g) (G ⊙ F ⊙ f)  ∎)
  where
  open Precategory

-- id⇨ is a left identity (assuming extensionality).

id⇨∙⇨ :
  ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
    {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄} →
  Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
  {F : C ⇨ D} → id⇨ ∙⇨ F ≡ F
id⇨∙⇨ ext {F} = _≃_.from (equality-characterisation⇨ ext)
  ( refl (F ⊚_)
  , (subst _ (refl (F ⊚_)) (λ {_ _} → F ⊙_)  ≡⟨ subst-refl _ _ ⟩∎
     (λ {_ _} → F ⊙_)                        ∎)
  )

-- id⇨ is a right identity (assuming extensionality).

∙⇨id⇨ :
  ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
    {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄} →
  Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
  {F : C ⇨ D} → F ∙⇨ id⇨ ≡ F
∙⇨id⇨ ext {F} = _≃_.from (equality-characterisation⇨ ext)
  ( refl (F ⊚_)
  , (subst _ (refl (F ⊚_)) (λ {_ _} → F ⊙_)  ≡⟨ subst-refl _ _ ⟩∎
     (λ {_ _} → F ⊙_)                        ∎)
  )

-- _∙⇨_ is associative (assuming extensionality).

∙⇨-assoc :
  ∀ {ℓ₁ ℓ₂} {C₁ : Precategory ℓ₁ ℓ₂}
    {ℓ₃ ℓ₄} {C₂ : Precategory ℓ₃ ℓ₄}
    {ℓ₅ ℓ₆} {C₃ : Precategory ℓ₅ ℓ₆}
    {ℓ₇ ℓ₈} {C₄ : Precategory ℓ₇ ℓ₈} →
  Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₈) →
  (F : C₃ ⇨ C₄) (G : C₂ ⇨ C₃) {H : C₁ ⇨ C₂} →
  F ∙⇨ (G ∙⇨ H) ≡ (F ∙⇨ G) ∙⇨ H
∙⇨-assoc ext F G {H} = _≃_.from (equality-characterisation⇨ ext)
  ( refl _
  , (subst _ (refl _) (λ {_ _} → (F ∙⇨ G ∙⇨ H) ⊙_)  ≡⟨ subst-refl _ _ ⟩
     (λ {_ _} → (F ∙⇨ G ∙⇨ H) ⊙_)                   ∎)
  )

------------------------------------------------------------------------
-- Natural transformations

Natural-transformation :
  ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
    {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄} →
  C ⇨ D → C ⇨ D → Type _
Natural-transformation {C = C} {D = D} F G =
  -- Morphisms.
  ∃ λ (γ : ∀ {X} → Hom D (F ⊚ X) (G ⊚ X)) →

  -- Naturality.
  ∀ {X Y} {f : Hom C X Y} → (G ⊙ f) ∙ γ ≡ γ ∙ (F ⊙ f)

  where
  open Precategory hiding (_∙_)
  open Precategory D using (_∙_)

-- A wrapper.

infix 4 _⇾_

record _⇾_ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
           {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄}
           (F G : C ⇨ D) : Type (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
  field
    natural-transformation : Natural-transformation F G

  open Precategory hiding (_∙_)
  open Precategory D using (_∙_)

  -- Morphisms.

  transformation : ∀ {X} → Hom D (F ⊚ X) (G ⊚ X)
  transformation = proj₁ natural-transformation

  -- Naturality.

  natural : ∀ {X Y} {f : Hom C X Y} →
            (G ⊙ f) ∙ transformation ≡ transformation ∙ (F ⊙ f)
  natural = proj₂ natural-transformation

private
 module Dummy₄ where
  abstract

   -- The naturality property is a proposition (assuming
   -- extensionality).

   naturality-propositional :
     ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
     Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
     {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄}
     (F G : C ⇨ D) →
     let open Precategory hiding (_∙_); open Precategory D using (_∙_) in
     {transformation : ∀ {X} → Hom D (F ⊚ X) (G ⊚ X)} →

     Is-proposition (∀ {X Y} {f : Hom C X Y} →
                     (G ⊙ f) ∙ transformation ≡
                     transformation ∙ (F ⊙ f))

   naturality-propositional {ℓ₁} {ℓ₂} ext {D = D} _ _ =
     implicit-Π-closure (lower-extensionality ℓ₂ lzero     ext) 1 λ _ →
     implicit-Π-closure (lower-extensionality ℓ₂ ℓ₁        ext) 1 λ _ →
     implicit-Π-closure (lower-extensionality ℓ₁ (ℓ₁ ⊔ ℓ₂) ext) 1 λ _ →
     Precategory.Hom-is-set D

   -- Natural transformation equality is equivalent to pointwise
   -- equality of the corresponding "transformations" (assuming
   -- extensionality).

   equality-characterisation⇾ :
     ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
     Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
     {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄}
     {F G : C ⇨ D} {γ δ : F ⇾ G} →

     (γ ≡ δ)
       ≃
     (∀ {X} → _⇾_.transformation γ {X = X} ≡
              _⇾_.transformation δ {X = X})

   equality-characterisation⇾ {ℓ₁} {ℓ₂} ext {F = F} {G} {γ} {δ} =
     γ ≡ δ                                                          ↝⟨ inverse $ Eq.≃-≡ $ ↔⇒≃ record
                                                                         { surjection = record
                                                                           { logical-equivalence = record
                                                                             { to   = _⇾_.natural-transformation
                                                                             ; from = λ γ → record { natural-transformation = γ }
                                                                             }
                                                                           ; right-inverse-of = refl
                                                                           }
                                                                         ; left-inverse-of = refl
                                                                         } ⟩
     _⇾_.natural-transformation γ ≡ _⇾_.natural-transformation δ    ↔⟨ inverse $ ignore-propositional-component
                                                                                (naturality-propositional ext F G) ⟩
     (λ {X} → _⇾_.transformation γ {X = X}) ≡ _⇾_.transformation δ  ↝⟨ inverse $ Eq.≃-≡ (Eq.↔⇒≃ implicit-Π↔Π) ⟩

     (λ X → _⇾_.transformation γ {X = X}) ≡
     (λ X → _⇾_.transformation δ {X = X})                           ↝⟨ inverse $ Eq.extensionality-isomorphism
                                                                                (lower-extensionality ℓ₂ (ℓ₁ ⊔ ℓ₂) ext) ⟩
     (∀ X → _⇾_.transformation γ {X = X} ≡
            _⇾_.transformation δ {X = X})                           ↔⟨ inverse implicit-Π↔Π ⟩□

     (∀ {X} → _⇾_.transformation γ {X = X} ≡
              _⇾_.transformation δ {X = X})                         □

   -- Natural transformations form sets (assuming extensionality).

   ⇾-set :
     ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
     Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄) →
     {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄} {F G : C ⇨ D} →
     Is-set (F ⇾ G)
   ⇾-set {ℓ₁} {ℓ₂} ext {D = D} {F = F} {G = G} =
     let surj = record
           { logical-equivalence = record
             { to   = λ γ → record { natural-transformation = γ }
             ; from = _⇾_.natural-transformation
             }
           ; right-inverse-of = refl
           } in

     respects-surjection surj 2 $
       Σ-closure 2
         (implicit-Π-closure
            (lower-extensionality ℓ₂ (ℓ₁ ⊔ ℓ₂) ext) 2 λ _ →
          Precategory.Hom-is-set D)
         (λ _ → mono₁ 1 $ naturality-propositional ext F G)

open Dummy₄ public

-- Identity natural transformation.

id⇾ : ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
        {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄}
      (F : C ⇨ D) → F ⇾ F
id⇾ {C = C} {D = D} F =
  record { natural-transformation = id , Dummy₅.nat }
  where
  open Precategory D

  module Dummy₅ where
   abstract

    nat : ∀ {X Y} {f : Precategory.Hom C X Y} →
          (F ⊙ f) ∙ id ≡ id ∙ (F ⊙ f)
    nat {f = f} =
      (F ⊙ f) ∙ id  ≡⟨ right-identity ⟩
      F ⊙ f         ≡⟨ sym $ left-identity ⟩∎
      id ∙ (F ⊙ f)  ∎

-- Composition of natural transformations.

infixr 10 _∙⇾_

_∙⇾_ : ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
         {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄}
         {F G H : C ⇨ D} →
       G ⇾ H → F ⇾ G → F ⇾ H
_∙⇾_ {C = C} {D = D} {F} {G} {H} γ δ =
  record { natural-transformation = ε , Dummy₅.nat }
  where
  open Precategory D
  open _⇾_

  ε : ∀ {X} → Hom (F ⊚ X) (H ⊚ X)
  ε = transformation γ ∙ transformation δ

  module Dummy₅ where
   abstract

    nat : ∀ {X Y} {f : Precategory.Hom C X Y} →
          (H ⊙ f) ∙ ε ≡ ε ∙ (F ⊙ f)
    nat {f = f} =
      (H ⊙ f) ∙ (transformation γ ∙ transformation δ)  ≡⟨ assoc ⟩
      ((H ⊙ f) ∙ transformation γ) ∙ transformation δ  ≡⟨ cong (λ f → f ∙ _) $ natural γ ⟩
      (transformation γ ∙ (G ⊙ f)) ∙ transformation δ  ≡⟨ sym assoc ⟩
      transformation γ ∙ ((G ⊙ f) ∙ transformation δ)  ≡⟨ cong (_∙_ _) $ natural δ ⟩
      transformation γ ∙ (transformation δ ∙ (F ⊙ f))  ≡⟨ assoc ⟩∎
      (transformation γ ∙ transformation δ) ∙ (F ⊙ f)  ∎

-- Composition of functors and natural transformations.

infixr 10 _⇾∙⇨_ _⇨∙⇾_

_⇾∙⇨_ : ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
          {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄}
          {ℓ₅ ℓ₆} {E : Precategory ℓ₅ ℓ₆}
          {G H : D ⇨ E} →
        G ⇾ H → (F : C ⇨ D) → (G ∙⇨ F) ⇾ (H ∙⇨ F)
_⇾_.natural-transformation (γ ⇾∙⇨ _) = transformation , natural
  where
  open _⇾_ γ

_⇨∙⇾_ : ∀ {ℓ₁ ℓ₂} {C : Precategory ℓ₁ ℓ₂}
          {ℓ₃ ℓ₄} {D : Precategory ℓ₃ ℓ₄}
          {ℓ₅ ℓ₆} {E : Precategory ℓ₅ ℓ₆}
          {G H : C ⇨ D} →
        (F : D ⇨ E) → G ⇾ H → (F ∙⇨ G) ⇾ (F ∙⇨ H)
_⇾_.natural-transformation (_⇨∙⇾_ {C = C} {D = D} {E = E} {G} {H} F γ) =
  ε , Dummy₅.nat
  where
  open Precategory
  open _⇾_ γ

  ε : ∀ {X} → Hom E (F ⊚ G ⊚ X) (F ⊚ H ⊚ X)
  ε = F ⊙ transformation

  module Dummy₅ where
   abstract

    nat : ∀ {X Y} {f : Hom C X Y} →
          _∙_ E (F ⊙ H ⊙ f) ε ≡ _∙_ E ε (F ⊙ G ⊙ f)
    nat {f = f} =
      _∙_ E (F ⊙ H ⊙ f) (F ⊙ transformation)  ≡⟨ sym $ ⊙-∙ F ⟩
      F ⊙ _∙_ D (H ⊙ f) transformation        ≡⟨ cong (F ⊙_) natural ⟩
      F ⊙ _∙_ D transformation (G ⊙ f)        ≡⟨ ⊙-∙ F ⟩∎
      _∙_ E (F ⊙ transformation) (F ⊙ G ⊙ f)  ∎

------------------------------------------------------------------------
-- Functor precategories

-- Functor precategories are defined using extensionality.

infix 10 _^_

_^_ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
      Precategory ℓ₁ ℓ₂ → Precategory ℓ₃ ℓ₄ →
      Extensionality (ℓ₃ ⊔ ℓ₄) (ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) →
      Precategory _ _
(D ^ C) ext = record
  { precategory =
        (C ⇨ D)
      , (λ F G → (F ⇾ G) , ⇾-set ext)
      , id⇾ _
      , _∙⇾_
      , _≃_.from (equality-characterisation⇾ ext) left-identity
      , _≃_.from (equality-characterisation⇾ ext) right-identity
      , _≃_.from (equality-characterisation⇾ ext) assoc
  }
  where
  open Precategory D

private
 module Dummy₅ where
  abstract

   -- The natural transformation γ is an isomorphism in (D ^ C) ext iff
   -- _⇾_.transformation γ {X = X} is an isomorphism in D for every X.

   natural-isomorphism-lemma :
     ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄}
     (ext : Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₄)) →
     {C : Precategory ℓ₁ ℓ₂} {D : Precategory ℓ₃ ℓ₄}
     {F G : C ⇨ D} {γ : F ⇾ G} → let open Precategory in

     Is-isomorphism ((D ^ C) ext) γ ⇔
     (∀ {X} → Is-isomorphism D (_⇾_.transformation γ {X = X}))

   natural-isomorphism-lemma ext {D = D} {F} {G} {γ} = record
     { to = λ { (δ , γδ , δγ) →
         transformation δ ,
         (transformation γ ∙ transformation δ  ≡⟨⟩
          transformation (γ ∙⇾ δ)              ≡⟨ cong (λ ε → transformation ε) γδ ⟩
          transformation (id⇾ G)               ≡⟨⟩
          id                                   ∎) ,
         (transformation δ ∙ transformation γ  ≡⟨⟩
          transformation (δ ∙⇾ γ)              ≡⟨ cong (λ ε → transformation ε) δγ ⟩
          transformation (id⇾ F)               ≡⟨⟩
          id                                   ∎) }
     ; from = λ iso →
         record { natural-transformation =
           proj₁ iso ,
           (λ {_ _ f} →
                (F ⊙ f) ∙ proj₁ iso                                     ≡⟨ sym left-identity ⟩
                id ∙ (F ⊙ f) ∙ proj₁ iso                                ≡⟨ cong (λ g → g ∙ (F ⊙ f) ∙ proj₁ iso) $ sym $ proj₂ (proj₂ iso) ⟩
                (proj₁ iso ∙ transformation γ) ∙ (F ⊙ f) ∙ proj₁ iso    ≡⟨ sym assoc ⟩
                proj₁ iso ∙ (transformation γ ∙ (F ⊙ f) ∙ proj₁ iso)    ≡⟨ cong (_ ∙_) assoc ⟩
                proj₁ iso ∙ ((transformation γ ∙ (F ⊙ f)) ∙ proj₁ iso)  ≡⟨ cong (λ g → _ ∙ (g ∙ _)) $ sym $ natural γ ⟩
                proj₁ iso ∙ (((G ⊙ f) ∙ transformation γ) ∙ proj₁ iso)  ≡⟨ cong (_ ∙_) $ sym assoc ⟩
                proj₁ iso ∙ (G ⊙ f) ∙ (transformation γ ∙ proj₁ iso)    ≡⟨ cong ((_ ∙_) ∘ ((G ⊙ f) ∙_)) $ proj₁ (proj₂ iso) ⟩
                proj₁ iso ∙ (G ⊙ f) ∙ id                                ≡⟨ assoc ⟩
                (proj₁ iso ∙ (G ⊙ f)) ∙ id                              ≡⟨ right-identity ⟩∎
                proj₁ iso ∙ (G ⊙ f)                                     ∎) } ,
         _≃_.from (equality-characterisation⇾ ext) (proj₁ (proj₂ iso)) ,
         _≃_.from (equality-characterisation⇾ ext) (proj₂ (proj₂ iso))
     }
     where
     open Precategory D
     open _⇾_

open Dummy₅ public

abstract

  -- If D is a category, then (D ^ C) ext is also a category.

  infix 10 _↑_

  _↑_ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} →
        Category ℓ₁ ℓ₂ → Precategory ℓ₃ ℓ₄ →
        Extensionality (ℓ₃ ⊔ ℓ₄) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) →
        Category (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
  _↑_ {ℓ₁} {ℓ₂} {ℓ₃} {ℓ₄} D C ext = record { category =
    D^C ,

    (λ {F G} → _≃_.is-equivalence $ ↔⇒≃ $ record
       { surjection = record
         { logical-equivalence = record
           { to   = Precategory.≡→≅ D^C
           ; from = λ { (F⇾G , F⇾G-iso) →

               let γ : ∀ X → F ⊚ X ≅ G ⊚ X
                   γ _ = _⇾_.transformation F⇾G ,
                         _⇔_.to (natural-isomorphism-lemma ext₁) F⇾G-iso

                   ⊚F≡⊚G : _⊚_ F ≡ _⊚_ G
                   ⊚F≡⊚G = apply-ext (Eq.good-ext ext₂) λ X →
                     F ⊚ X  ≡⟨ ≅→≡ (γ X) ⟩∎
                     G ⊚ X  ∎

                   cong-⊚F≡⊚G : ∀ {X} → cong (λ H → H X) ⊚F≡⊚G ≡ ≅→≡ (γ X)
                   cong-⊚F≡⊚G = Eq.cong-good-ext ext₂ (≅→≡ ∘ γ)

                   ⊙F≡⊙G : _≡_ {A = ∀ {X Y} → HomC X Y → Hom (G ⊚ X) (G ⊚ Y)}
                               (subst (λ F → ∀ {X Y} → HomC X Y → Hom (F X) (F Y))
                                      ⊚F≡⊚G
                                      (_⊙_ F))
                               (_⊙_ G)
                   ⊙F≡⊙G =
                     implicit-extensionality (lower-extensionality ℓ₄ ℓ₁        ext) λ X →
                     implicit-extensionality (lower-extensionality ℓ₄ (ℓ₁ ⊔ ℓ₃) ext) λ Y →
                     apply-ext (lower-extensionality ℓ₃ (ℓ₁ ⊔ ℓ₃ ⊔ ℓ₄) ext) λ f →

                     subst (λ F → ∀ {X Y} → HomC X Y → Hom (F X) (F Y))
                           ⊚F≡⊚G (_⊙_ F) f                               ≡⟨ cong (λ H → H f) $ sym $
                                                                                push-subst-implicit-application ⊚F≡⊚G
                                                                                (λ F X → ∀ {Y} → HomC X Y → Hom (F X) (F Y)) ⟩
                     subst (λ F → ∀ {Y} → HomC X Y → Hom (F X) (F Y))
                           ⊚F≡⊚G (_⊙_ F) f                               ≡⟨ cong (λ H → H f) $ sym $
                                                                                push-subst-implicit-application ⊚F≡⊚G
                                                                                (λ F Y → HomC X Y → Hom (F X) (F Y)) ⟩
                     subst (λ F → HomC X Y → Hom (F X) (F Y))
                           ⊚F≡⊚G (_⊙_ F) f                               ≡⟨ sym $ push-subst-application ⊚F≡⊚G
                                                                                (λ F _ → Hom (F X) (F Y)) ⟩
                     subst (λ F → Hom (F X) (F Y)) ⊚F≡⊚G (F ⊙ f)         ≡⟨ subst-∘ (uncurry Hom) (λ H → (H X , H Y)) ⊚F≡⊚G ⟩

                     subst (uncurry Hom)
                           (cong (λ H → (H X , H Y)) ⊚F≡⊚G) (F ⊙ f)      ≡⟨ cong (λ p → subst (uncurry Hom) p (F ⊙ f)) $ sym $
                                                                                cong₂-cong-cong {eq = ⊚F≡⊚G} (λ H → H X) (λ H → H Y) _,_ ⟩
                     subst (uncurry Hom)
                           (cong₂ _,_ (cong (λ H → H X) ⊚F≡⊚G)
                                      (cong (λ H → H Y) ⊚F≡⊚G)) (F ⊙ f)  ≡⟨ cong₂ (λ p q → subst (uncurry Hom) (cong₂ _,_ p q) (F ⊙ f))
                                                                                cong-⊚F≡⊚G cong-⊚F≡⊚G ⟩
                     subst (uncurry Hom)
                           (cong₂ _,_ (≅→≡ (γ X)) (≅→≡ (γ Y))) (F ⊙ f)   ≡⟨ Hom-, (≅→≡ (γ X)) (≅→≡ (γ Y)) ⟩

                     ≡→≅ (≅→≡ (γ Y)) ¹ ∙ (F ⊙ f) ∙ ≡→≅ (≅→≡ (γ X)) ⁻¹    ≡⟨ cong₂ (λ p q → p ¹ ∙ (F ⊙ f) ∙ q ⁻¹)
                                                                                (_≃_.right-inverse-of ≡≃≅ _)
                                                                                (_≃_.right-inverse-of ≡≃≅ _) ⟩
                     γ Y ¹ ∙ (F ⊙ f) ∙ γ X ⁻¹                            ≡⟨ assoc ⟩

                     (γ Y ¹ ∙ (F ⊙ f)) ∙ γ X ⁻¹                          ≡⟨ cong (_∙ γ X ⁻¹) $ sym $ _⇾_.natural F⇾G ⟩

                     ((G ⊙ f) ∙ γ X ¹) ∙ γ X ⁻¹                          ≡⟨ sym assoc ⟩

                     (G ⊙ f) ∙ γ X ¹ ∙ γ X ⁻¹                            ≡⟨ cong (_ ∙_) $ γ X ¹⁻¹ ⟩

                     (G ⊙ f) ∙ id                                        ≡⟨ right-identity ⟩∎

                     G ⊙ f                                               ∎

               in _≃_.from (equality-characterisation⇨ ext₁)
                           (⊚F≡⊚G , ⊙F≡⊙G) }
           }
         ; right-inverse-of = λ { (F⇾G , F⇾G-iso) →
             _≃_.from (Precategory.≡≃≡¹ D^C) $
             _≃_.from (equality-characterisation⇾ ext₁) λ {X} →
               _⇾_.transformation (proj₁ (Precategory.≡→≅ D^C _))         ≡⟨⟩

               _⇾_.transformation
                 (proj₁ (elim (λ {F G} _ → Precategory._≅_ D^C F G)
                              (λ _ → Precategory.id≅ D^C) _))             ≡⟨ elim (λ {F G} F≡G →
                                                                                _⇾_.transformation (proj₁ (Precategory.≡→≅ D^C F≡G)) ≡
                                                                                elim (λ {F G} _ → Hom (F X) (G X)) (λ _ → id) (cong _⊚_ F≡G))
                                                                                (λ F →
                   _⇾_.transformation
                     (proj₁ (elim (λ {F G} _ → Precategory._≅_ D^C F G)
                                  (λ _ → Precategory.id≅ D^C) (refl F)))             ≡⟨ cong (λ f → _⇾_.transformation (proj₁ f) {X = X}) $
                                                                                elim-refl (λ {X Y} _ → Precategory._≅_ D^C X Y) _ ⟩
                   _⇾_.transformation {F = F}
                     (proj₁ (Precategory.id≅ D^C))                                   ≡⟨⟩

                   id                                                                ≡⟨ sym $ elim-refl (λ {F G} _ → Hom (F X) (G X)) _ ⟩

                   elim (λ {F G} _ → Hom (F X) (G X))
                        (λ _ → id) (refl (_⊚_ F))                                    ≡⟨ cong (elim (λ {F G} _ → Hom (F X) (G X)) _) $
                                                                                sym $ cong-refl _⊚_ ⟩∎
                   elim (λ {F G} _ → Hom (F X) (G X))
                        (λ _ → id) (cong _⊚_ (refl F))                               ∎)
                                                                                _ ⟩
               elim (λ {F G} _ → Hom (F X) (G X))
                    (λ _ → id) (cong _⊚_ _)                               ≡⟨ cong (elim (λ {F G} _ → Hom (F X) (G X)) (λ _ → id)) $
                                                                               cong-⊚-from-equality-characterisation⇨ _ _ _ ⟩
               elim (λ {F G} _ → Hom (F X) (G X)) (λ _ → id)
                    (apply-ext (Eq.good-ext ext₂) λ Y →
                       ≅→≡ (_⇾_.transformation F⇾G {X = Y} , _))          ≡⟨ Eq.elim-good-ext ext₂ _ _ _ ⟩

               elim (λ {X Y} _ → Hom X Y) (λ _ → id)
                    (≅→≡ (_⇾_.transformation F⇾G {X = X} , _))            ≡⟨ elim (λ {X Y} X≡Y → elim (λ {X Y} _ → Hom X Y) (λ _ → id) X≡Y ≡
                                                                                proj₁ (≡→≅ X≡Y))
                                                                                (λ X →
                   elim (λ {X Y} _ → Hom X Y) (λ _ → id) (refl X)                    ≡⟨ elim-refl (λ {X Y} _ → Hom X Y) _ ⟩
                   id                                                                ≡⟨⟩
                   proj₁ id≅                                                         ≡⟨ cong proj₁ (sym ≡→≅-refl) ⟩∎
                   proj₁ (≡→≅ (refl X))                                              ∎ )
                                                                                _ ⟩
               proj₁ (≡→≅ (≅→≡ (_⇾_.transformation F⇾G {X = X} , _)))     ≡⟨ cong proj₁ (_≃_.right-inverse-of ≡≃≅ _) ⟩∎

               _⇾_.transformation F⇾G {X = X}                             ∎ }
           }
       ; left-inverse-of = λ F≡G →
           _≃_.from (equality-characterisation≡⇨ ext₁) (
              cong _⊚_ _                                           ≡⟨ cong-⊚-from-equality-characterisation⇨ _ _ _ ⟩

              apply-ext (Eq.good-ext ext₂) (λ X →
                ≅→≡ ( _⇾_.transformation
                        (proj₁ $ Precategory.≡→≅ D^C F≡G) {X = X}
                    , _
                    ))                                             ≡⟨ elim
                                                                        (λ {F G} F≡G → (f : (X : _) → _) →
                                                                           apply-ext (Eq.good-ext ext₂) (λ X →
                                                                             ≅→≡ (_⇾_.transformation (proj₁ $ Precategory.≡→≅ D^C F≡G) , f X)) ≡
                                                                           cong _⊚_ F≡G)
                                                                        (λ F _ →
                  apply-ext (Eq.good-ext ext₂) (λ _ →
                    ≅→≡ ( _⇾_.transformation
                            (proj₁ $ Precategory.≡→≅ D^C (refl F))
                        , _
                        ))                                                  ≡⟨ cong (apply-ext (Eq.good-ext ext₂)) (apply-ext ext₂ λ X → cong ≅→≡ $
                                                                                Σ-≡,≡→≡ (cong (λ f → _⇾_.transformation (proj₁ f) {X = X}) $
                                                                                Precategory.≡→≅-refl D^C)
                                                                                (refl _)) ⟩
                  apply-ext (Eq.good-ext ext₂) (λ _ →
                    ≅→≡ ( _⇾_.transformation {F = F}
                            (proj₁ $ Precategory.id≅ D^C)
                        , _
                        ))                                                  ≡⟨⟩

                  apply-ext (Eq.good-ext ext₂) (λ _ → ≅→≡ (id , _))         ≡⟨ cong (apply-ext (Eq.good-ext ext₂)) (apply-ext ext₂ λ _ →
                                                                                cong ≅→≡ $ _≃_.from ≡≃≡¹ $ refl _) ⟩
                  apply-ext (Eq.good-ext ext₂) (λ _ → ≅→≡ id≅)              ≡⟨ cong (apply-ext (Eq.good-ext ext₂)) (apply-ext ext₂ λ _ →
                                                                                ≅→≡-refl) ⟩
                  apply-ext (Eq.good-ext ext₂) (λ X → refl (F ⊚ X))         ≡⟨ Eq.good-ext-refl ext₂ _ ⟩

                  refl (_⊚_ F)                                              ≡⟨ sym $ cong-refl _ ⟩∎

                  cong _⊚_ (refl F)                                         ∎)
                                                                        F≡G _ ⟩∎
              cong _⊚_ F≡G                                         ∎)
       }) }
    where
    open Category D
    open Precategory C using () renaming (Hom to HomC)

    ext₁ : Extensionality (ℓ₃ ⊔ ℓ₄) (ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
    ext₁ = lower-extensionality lzero ℓ₁ ext

    ext₂ : Extensionality ℓ₃ ℓ₁
    ext₂ = lower-extensionality ℓ₄ (ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) ext

    D^C : Precategory (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
    D^C = (precategory ^ C) ext₁

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- Binding signatures
module SOAS.Syntax.Signature (T : Set) where

open import SOAS.Syntax.Arguments {T}

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable

open import SOAS.Families.Core {T}
open import SOAS.Families.BCCC {T} using (⊤ₘ)

open import SOAS.Coalgebraic.Strength
open import SOAS.Coalgebraic.Lift
open import SOAS.Coalgebraic.Map

open import SOAS.Abstract.Hom

open import SOAS.Abstract.ExpStrength
import SOAS.Abstract.Coalgebra as →□
open →□.Sorted
open →□.Unsorted renaming (Coalg to UCoalg ; Coalg⇒ to UCoalg⇒)

open import Data.List.Base using ([] ; _∷_ ; List)

private
  variable
    Γ Δ Θ : Ctx
    α τ : T

-- Binding signature for a second-order syntax, consisting of a set of operators
-- O and an arity assignment ∣_∣
record Signature (O : Set) : Set₁ where
  constructor sig
  field ∣_∣ : O → List (Ctx × T) × T

  -- Sort and arity of an operator
  Sort : O → T
  Sort o = proj₂ ∣ o ∣

  Arity : O → List (Ctx × T)
  Arity o = proj₁ ∣ o ∣

  -- Signature endofunctor
  ⅀F : Functor 𝔽amiliesₛ 𝔽amiliesₛ
  ⅀F  = record
    { F₀ = λ 𝒳 α Γ → Σ[ o ∈ O ] (α ≡ Sort o × Arg (Arity o) 𝒳 Γ)
    ; F₁ = λ{ f (o , e , ar) → o , e , (F₁ o f ar)}
    ; identity = λ{ {x = o , e , ar} → cong (λ - → o , e , -) (identity o) }
    ; homomorphism = λ{ {x = o , e , ar} → cong (λ - → o , e , -) (homomorphism o) }
    ; F-resp-≈ = λ{ p {x = o , e , ar} → cong (λ - → o , e , -) (F-resp-≈ o p) }
    } where open module AF o =  Functor (ArgF (Arity o))

  pattern _⋮_ o ar = (o , refl , ar)
  infix 1 _⋮_

  open import SOAS.Metatheory.Algebra {T} ⅀F public

  -- Coalgebraic and exponential strength for signature endofunctor
  private
    str : {𝒫 : Familyₛ}(𝒫ᴮ : Coalgₚ 𝒫)(𝒳 : Familyₛ)
          (as : List (Ctx × T))(σ : Γ ~[ 𝒫 ]↝ Δ)
        → Arg as 〖 𝒫 , 𝒳 〗 Γ → Arg as 𝒳 Δ
    str 𝒫ᴮ 𝒳 [] σ x = tt
    str 𝒫ᴮ 𝒳 ((Θ , τ) ∷ []) σ h = h (lift 𝒫ᴮ Θ σ)
    str 𝒫ᴮ 𝒳 ((Θ , τ) ∷ a ∷ as) σ (h , at) = h (lift 𝒫ᴮ Θ σ) , str 𝒫ᴮ 𝒳 (a ∷ as) σ at

    str-nat₁ : {𝒫 𝒬 𝒳 : Familyₛ} {𝒫ᴮ : Coalgₚ 𝒫} {𝒬ᴮ : Coalgₚ 𝒬}
             → {f : 𝒬 ⇾̣ 𝒫} (fᴮ⇒ : Coalgₚ⇒ 𝒬ᴮ 𝒫ᴮ f)
             → (as : List (Ctx × T))
             → (h : Arg as 〖 𝒫 , 𝒳 〗 Γ) (σ : Γ ~[ 𝒬 ]↝ Δ)
             → str 𝒫ᴮ 𝒳 as (λ x → f (σ x)) h
             ≡ str 𝒬ᴮ 𝒳 as σ (Arg₁ as (λ{ h′ ς → h′ (λ v → f (ς v))}) h)
    str-nat₁ fᴮ⇒ [] h σ = refl
    str-nat₁ {𝒳 = 𝒳} fᴮ⇒ ((Θ , τ) ∷ []) h σ = lift-comp 𝒳 Θ fᴮ⇒ h σ
    str-nat₁ {𝒳 = 𝒳} fᴮ⇒ ((Θ , τ) ∷ a ∷ as) (h , ap) σ =
      cong₂ _,_ (lift-comp 𝒳 Θ fᴮ⇒ h σ) (str-nat₁ fᴮ⇒ (a ∷ as) ap σ)

    str-nat₂ : {𝒫 𝒳 𝒴 : Familyₛ} {𝒫ᴮ : Coalgₚ 𝒫}
             → (f : 𝒳 ⇾̣ 𝒴)
             → (as : List (Ctx × T))
             → (h : Arg as 〖 𝒫 , 𝒳 〗 Γ) (σ : Γ ~[ 𝒫 ]↝ Δ)
             → str 𝒫ᴮ 𝒴 as σ (Arg₁ as (λ{ h′ ς → f (h′ ς)}) h)
             ≡ Arg₁ as f (str 𝒫ᴮ 𝒳 as σ h)
    str-nat₂ f [] h σ = refl
    str-nat₂ f ((Θ , τ) ∷ []) h σ = refl
    str-nat₂ f ((Θ , τ) ∷ a ∷ as) (h , ap) σ = cong (_ ,_) (str-nat₂ f (a ∷ as) ap σ)

    str-unit : (𝒳 : Familyₛ)
             → (as : List (Ctx × T))
             → (h : Arg as 〖 ℐ , 𝒳 〗 Γ)
             → str ℐᴮ 𝒳 as id h
             ≡ Arg₁ as (λ b → b id) h
    str-unit 𝒳 [] h = refl
    str-unit 𝒳 ((Θ , τ) ∷ []) h = rlift-id 𝒳 Θ h
    str-unit 𝒳 ((Θ , τ) ∷ a ∷ as) (h , ap) = cong₂ _,_ (rlift-id 𝒳 Θ h) (str-unit 𝒳 (a ∷ as) ap)

    str-assoc : (𝒳 : Familyₛ) {𝒫 𝒬 ℛ : Familyₛ}
                {𝒫ᴮ : Coalgₚ 𝒫} {𝒬ᴮ : Coalgₚ 𝒬} {ℛᴮ : Coalgₚ ℛ}
              → {f : 𝒫 ⇾̣ 〖 𝒬 , ℛ 〗} (fᶜ : Coalgebraic 𝒫ᴮ 𝒬ᴮ ℛᴮ f)
              → (open Coalgebraic fᶜ)
              → (as : List (Ctx × T))
              → (h : Arg as 〖 ℛ , 𝒳 〗 Γ) (σ : Γ ~[ 𝒫 ]↝ Δ) (ς : Δ ~[ 𝒬 ]↝ Θ)
              → str ℛᴮ 𝒳 as (λ v → f (σ v) ς) h
              ≡ str 𝒬ᴮ 𝒳 as ς (str 〖𝒫,𝒴〗ᴮ 〖 𝒬 , 𝒳 〗 as (f ∘ σ) (Arg₁ as (λ{ h ς σ → h (λ v → ς v σ)}) h))
    str-assoc 𝒳 fᶜ [] h σ ς = refl
    str-assoc 𝒳 fᶜ ((Ξ , τ) ∷ []) h σ ς = lift-assoc 𝒳 Ξ fᶜ h σ ς
    str-assoc 𝒳 fᶜ ((Ξ , τ) ∷ a ∷ as) (h , ap) σ ς = cong₂ _,_ (lift-assoc 𝒳 Ξ fᶜ h σ ς) (str-assoc 𝒳 fᶜ (a ∷ as) ap σ ς)

    estr : {X : Family}(Xᵇ : UCoalg X)(𝒴 : Familyₛ)
          (as : List (Ctx × T))
        → Arg as (X ⇨ 𝒴) Γ → (x : X Γ) → Arg as 𝒴 Γ
    estr Xᵇ 𝒴 [] at x = tt
    estr Xᵇ 𝒴 ((Θ , τ) ∷ []) e x = e (UCoalg.wkr Xᵇ Θ x)
    estr Xᵇ 𝒴 ((Θ , τ) ∷ a ∷ as) (e , at) x = (e (UCoalg.wkr Xᵇ Θ x)) , estr Xᵇ 𝒴 (a ∷ as) at x

    estr-nat₁ : {X X′ : Family} {Xᵇ : UCoalg X}
      {X′ᵇ : UCoalg X′} {𝒴 : Familyₛ} {f : X′ ⇾ X} →
      UCoalg⇒ X′ᵇ Xᵇ f →
      (as : List (Ctx × T))
      (h : Arg as (X ⇨ 𝒴) Γ)(x : X′ Γ)
      → estr Xᵇ 𝒴 as h (f x)
      ≡ estr X′ᵇ 𝒴 as (Arg₁ as (λ e x₁ → e (f x₁)) h) x
    estr-nat₁ fᵇ⇒ [] h x = refl
    estr-nat₁ fᵇ⇒ ((Θ , τ) ∷ []) h x = cong h (sym (UCoalg⇒.⟨r⟩ fᵇ⇒))
    estr-nat₁ fᵇ⇒ ((Θ , τ) ∷ a ∷ as) (h , at) x = cong₂ _,_ (cong h (sym (UCoalg⇒.⟨r⟩ fᵇ⇒))) (estr-nat₁ fᵇ⇒ (a ∷ as) at x)

    estr-nat₂ : {X : Family} {Xᵇ : UCoalg X}
        {𝒴 𝒴′ : Familyₛ} (g : 𝒴 ⇾̣ 𝒴′) (as : List (Ctx × T))(at : Arg as (X ⇨ 𝒴) Γ) (x : X Γ)
        → estr Xᵇ 𝒴′ as (Arg₁ as (λ e x → g (e x)) at) x
        ≡ Arg₁ as g (estr Xᵇ 𝒴 as at x)
    estr-nat₂ g [] at x = refl
    estr-nat₂ g ((Θ , τ) ∷ []) h x = refl
    estr-nat₂ g ((Θ , τ) ∷ a ∷ as) (h , at) x = cong (_ ,_) (estr-nat₂ g (a ∷ as) at x)

    estr-unit : {𝒴 : Familyₛ} (as : List (Ctx × T)) {at : Arg as (⊤ₘ ⇨ 𝒴) Γ}
        → estr ⊤ᵇ 𝒴 as at tt ≡ Arg₁ as (λ e′ → e′ tt) at
    estr-unit [] = refl
    estr-unit ((Θ , τ) ∷ []) = refl
    estr-unit ((Θ , τ) ∷ a ∷ as) = cong (_ ,_) (estr-unit (a ∷ as))

  -- Compatible strengths for the signature endofunctor
  ⅀:CompatStr : CompatStrengths ⅀F
  ⅀:CompatStr = record
    { CoalgStr = record
      { str = λ{ 𝒫ᴮ 𝒳 (o , e , ap) σ → o , (e , str 𝒫ᴮ 𝒳 (Arity o) σ ap) }
      ; str-nat₁ = λ{ fᴮ⇒ (o , e , ap) σ → cong (λ - → o , e , -) (str-nat₁ fᴮ⇒ (Arity o) ap σ)}
      ; str-nat₂ = λ{ f (o , e , ap) σ → cong (λ - → o , e , -) (str-nat₂ f (Arity o) ap σ)}
      ; str-unit = λ{ 𝒳 (o , e , ap) → cong (λ - → o , e , -) (str-unit 𝒳 (Arity o) ap)}
      ; str-assoc = λ{ 𝒳 fᶜ (o , e , ap) σ ς → cong (λ - → o , e , -) (str-assoc 𝒳 fᶜ (Arity o) ap σ ς)}
      }
    ; ExpStr = record
      { estr = λ{ Xᵇ 𝒴 (o , refl , at) x → o , refl , estr Xᵇ 𝒴 (Arity o) at x }
      ; estr-nat₁ = λ{ fᵇ⇒ (o , refl , at) x → cong (λ - → o , refl , -) (estr-nat₁ fᵇ⇒ (Arity o) at x)}
      ; estr-nat₂ = λ{ g (o , refl , at) x → cong (λ - → o , refl , -) (estr-nat₂ g (Arity o) at x) }
      ; estr-unit = λ{ {e = (o , refl , at)} → cong (λ - → o , refl , -) (estr-unit (Arity o)) } }
    }

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
{-

Definition of the torus as a HIT together with a proof that it is
equivalent to two circles

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Torus.Base where

open import Cubical.Core.Glue

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Nat
open import Cubical.Data.Int
open import Cubical.Data.Prod hiding (_×_) renaming (_×Σ_ to _×_)

open import Cubical.HITs.S1

data Torus : Type₀ where
  point : Torus
  line1 : point ≡ point
  line2 : point ≡ point
  square : PathP (λ i → line1 i ≡ line1 i) line2 line2

t2c : Torus → S¹ × S¹
t2c point        = ( base , base )
t2c (line1 i)    = ( loop i , base )
t2c (line2 j)    = ( base , loop j )
t2c (square i j) = ( loop i , loop j )

c2t : S¹ × S¹ → Torus
c2t (base   , base)   = point
c2t (loop i , base)   = line1 i
c2t (base   , loop j) = line2 j
c2t (loop i , loop j) = square i j

c2t-t2c : ∀ (t : Torus) → c2t (t2c t) ≡ t
c2t-t2c point        = refl
c2t-t2c (line1 _)    = refl
c2t-t2c (line2 _)    = refl
c2t-t2c (square _ _) = refl

t2c-c2t : ∀ (p : S¹ × S¹) → t2c (c2t p) ≡ p
t2c-c2t (base   , base)   = refl
t2c-c2t (base   , loop _) = refl
t2c-c2t (loop _ , base)   = refl
t2c-c2t (loop _ , loop _) = refl

Torus≡S¹×S¹ : Torus ≡ S¹ × S¹
Torus≡S¹×S¹ = isoToPath (iso t2c c2t t2c-c2t c2t-t2c)

ΩTorus : Type₀
ΩTorus = point ≡ point

-- TODO: upstream
lemPathAnd : ∀ {ℓ} {A B : Type ℓ} (t u : A × B) →
  Path _ (t ≡ u) ((t .fst ≡ u .fst) × ((t .snd) ≡ (u .snd)))
lemPathAnd t u = isoToPath (iso (λ tu → (λ i → tu i .fst) , λ i → tu i .snd)
                                 (λ tu i → tu .fst i , tu .snd i)
                                 (λ y → refl)
                                 (λ x → refl))

funDep : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) (u0 : A) (u1 : B) →
  (Path A u0 (transport (λ i → p (~ i)) u1)) ≡ (Path B (transport p u0) u1)
funDep p u0 u1 i = Path (p i) (transp (λ j → p (i ∧ j)) (~ i) u0) (transp (λ j → p (i ∨ ~ j)) i u1)

-- Can this proof be simplified?
ΩTorus≡Int×Int : ΩTorus ≡ Int × Int
ΩTorus≡Int×Int =
  ΩTorus
    ≡⟨ (λ i → Path Torus point (transp (\ j → Torus≡S¹×S¹ (~ j ∧ i)) (~ i)
                                       (glue (λ { (i = i0) → point
                                                ; (i = i1) → (base , base) }) (base , base)))) ⟩
  Path Torus point (transp (\ i → Torus≡S¹×S¹ (~ i)) i0 (base , base))
    ≡⟨ funDep (λ i → Torus≡S¹×S¹ i) point (base , base) ⟩
  Path (S¹ × S¹) (transp (\ i → Torus≡S¹×S¹ i) i0 point) (base , base)
    ≡⟨ (λ i → Path _ (transp (λ j → Torus≡S¹×S¹ (j ∨ i))  i
                             (glue (λ { (i = i0) → point
                                      ; (i = i1) → (base , base) }) (base , base))) (base , base)) ⟩
  Path (S¹ × S¹) (base , base) (base , base)
    ≡⟨ lemPathAnd (base , base) (base , base) ⟩
  ΩS¹ × ΩS¹
    ≡⟨ (λ i → ΩS¹≡Int i × ΩS¹≡Int i) ⟩
  Int × Int ∎

-- Computing the winding numbers on the torus
windingTorus : ΩTorus → Int × Int
windingTorus l = ( winding (λ i → t2c (l i) .fst)
                 , winding (λ i → t2c (l i) .snd))

module _ where
 private
  test1 : windingTorus (line1 ∙ line2) ≡ (pos 1 , pos 1)
  test1 = refl

  test2 : windingTorus (line1 ∙ line2 ∙ sym line1 ∙ sym line1) ≡ (negsuc 0 , pos 1)
  test2 = refl

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


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

open import Categories.Category
open import Categories.Comonad

-- verbatim dual of Categories.Category.Construction.EilenbergMoore
module Categories.Category.Construction.CoEilenbergMoore {o ℓ e} {C : Category o ℓ e} (M : Comonad C) where

open import Level

open import Categories.Morphism.Reasoning C

private
  module C = Category C
  module M = Comonad M
  open C
  open M.F
  open HomReasoning
  open Equiv

record Comodule : Set (o ⊔ ℓ ⊔ e) where
  field
    A        : Obj
    coaction   : A ⇒ F₀ A
    commute  : F₁ coaction ∘ coaction ≈ M.δ.η A ∘ coaction
    identity : M.ε.η A ∘ coaction ≈ C.id

record Comodule⇒ (X Y : Comodule) : Set (ℓ ⊔ e) where
  private
    module X = Comodule X
    module Y = Comodule Y
  field
    arr     : X.A ⇒ Y.A
    commute : Y.coaction ∘ arr ≈ F₁ arr ∘ X.coaction

CoEilenbergMoore : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e
CoEilenbergMoore =
 record
  { Obj = Comodule
  ; _⇒_ = Comodule⇒
  ; _≈_ = λ f g → Comodule⇒.arr f ≈ Comodule⇒.arr g
  ; id = record { arr = C.id ; commute = identityʳ ○ introˡ identity }
  ; _∘_ = compose
  ; assoc = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
  ; ∘-resp-≈ = ∘-resp-≈
  }
  where
   open Equiv
   compose : ∀ {X Y Z} → Comodule⇒ Y Z → Comodule⇒ X Y → Comodule⇒ X Z
   compose {X} {Y} {Z} f g = record
    { arr     = f.arr ∘ g.arr
    ; commute = begin
       Comodule.coaction Z ∘ f.arr ∘ g.arr       ≈⟨ pullˡ f.commute ⟩
       (F₁ f.arr ∘ Comodule.coaction Y) ∘ g.arr  ≈⟨ pullʳ g.commute ⟩
       F₁ f.arr ∘ F₁ g.arr ∘ Comodule.coaction X ≈⟨ pullˡ (sym homomorphism) ⟩
       F₁ (f.arr ∘ g.arr) ∘ Comodule.coaction X  ∎
    }
    where module f = Comodule⇒ f
          module g = Comodule⇒ g

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module CategoryTheory.Linear where

open import CategoryTheory.Categories
open import CategoryTheory.Functor
open import CategoryTheory.BCCCs
open import CategoryTheory.Monad
open import CategoryTheory.Instances.Kleisli

module L {n} {ℂ : Category n} (ℂ-BCCC : BicartesianClosed ℂ) (Mo : Monad ℂ) where
    open Category ℂ
    open BicartesianClosed ℂ-BCCC
    open Monad Mo
    open Functor T renaming (omap to M ; fmap to M-f)
    Kl : Category n
    Kl = Kleisli ℂ Mo

    -- Linear product of two objects
    _⊛_ : (A B : obj) -> obj
    A ⊛ B = (A ⊗ M B) ⊕ (M A ⊗ B) ⊕ (A ⊗ B)

    -- First projection from linear product
    *π₁ : ∀{A B} -> A ⊛ B ~> M A
    *π₁ {A}{B} = [ η.at A ∘ π₁ ⁏ π₁ ⁏ η.at A ∘ π₁ ]

    -- Second projection from linear product
    *π₂ : ∀{A B} -> A ⊛ B ~> M B
    *π₂ {A}{B} = [ π₂ ⁏ η.at B ∘ π₂ ⁏ η.at B ∘ π₂ ]

    -- Type class for linear products of type A ⊛ B. Need to provide
    -- linear product of morphisms and product laws in order to establish
    -- that the linear product is a product in the Kleisli category of the monad.
    record LinearProduct (A B : obj) : Set (lsuc n) where
        infix 10 ⟪_,_⟫
        field
            -- | Data
            -- Linear product
            ⟪_,_⟫ : ∀{L} -> (L ~> M A) -> (L ~> M B) -> (L ~> M (A ⊛ B))

            -- | Laws
            *π₁-comm : ∀{L} -> {l₁ : L ~> M A} {l₂ : L ~> M B}
                   -> (μ.at A ∘ M-f *π₁) ∘ ⟪ l₁ , l₂ ⟫ ≈ l₁
            *π₂-comm : ∀{L} -> {l₁ : L ~> M A} {l₂ : L ~> M B}
                   -> (μ.at B ∘ M-f *π₂) ∘ ⟪ l₁ , l₂ ⟫ ≈ l₂
            ⊛-unique : ∀{P} {p₁ : P ~> M A} {p₂ : P ~> M B} {m : P ~> M A⊕B}
                    -> (μ.at A ∘ M-f *π₁) ∘ m ≈ p₁ -> (μ.at B ∘ M-f *π₂) ∘ m ≈ p₂
                    -> ⟪ p₁ , p₂ ⟫ ≈ m

        Kl-⊛ : Product Kl A B
        Kl-⊛ = record
            { A⊗B = A ⊛ B
            ; π₁ = *π₁
            ; π₂ = *π₂
            ; ⟨_,_⟩ = ⟪_,_⟫
            ; π₁-comm = *π₁-comm
            ; π₂-comm = *π₂-comm
            ; ⊗-unique = ⊛-unique
            }

-- Type class for linear categories
record Linear {n} {ℂ : Category n}
              (ℂ-BCCC : BicartesianClosed ℂ) (Mo : Monad ℂ) : Set (lsuc n) where
    open Category ℂ
    open L ℂ-BCCC Mo

    field
        linprod : ∀(A B : obj) -> LinearProduct A B

    open module Li {A} {B} = LinearProduct (linprod A B) public

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
-- {-# OPTIONS --cubical -vtc.lhs.split.partial:20 #-}
{-# OPTIONS --cubical #-}
module _ where
open import Agda.Primitive.Cubical
open import Agda.Builtin.Equality

postulate
  X : Set
  P : I → Set
  p : P i1

module Test (A : Set) (i : I) (B : Set) where

  j = i
  R = P j
  module Z (r s : A) where
    a0 : I → Partial j R
    a0 k with k
    ... | _ = \ { (j = i1) → p }

  a : Partial j R
  a (j = i1) = p

  refining : ∀ (x y : A) → x ≡ y → A → Partial j R
  refining x y refl = \ { _ (j = i1) → p }

  refining-dot : ∀ (x y : A) → x ≡ y → A → Partial j R
  refining-dot x .x refl = \ { _ (j = i1) → p }

  refining-dot2 : ∀ (x y : A) → x ≡ y → A → Partial j R
  refining-dot2 x .x refl z = \ { (i = i1) → p }

  refining-cxt : A ≡ X → Partial j R
  refining-cxt refl = \ { (j = i1) → p }

  refining-cxt2 : B ≡ X → Partial j R
  refining-cxt2 refl = \ { (j = i1) → p }

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


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

module Experiment.ListRelationProperties where

open import Level

open import Data.Bool hiding (_≤_; _≤?_; _<_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List
import Data.List.Properties as Listₚ
import      Data.Nat as ℕ
import Data.Nat.Properties as ℕₚ
open import Data.Product hiding (swap)

import      Data.List.Relation.Binary.Equality.Setoid as ListSetoidEquality
import Data.List.Relation.Binary.Permutation.Setoid as PermutationSetoid
import Data.List.Relation.Binary.Permutation.Setoid.Properties
  as PermutationSetoidProperties
open import Data.List.Relation.Unary.All as All
import      Data.List.Relation.Unary.All.Properties as Allₚ
open import Data.List.Relation.Unary.Any as Any
open import Data.List.Relation.Unary.Linked
import      Data.List.Relation.Unary.Linked.Properties as Linkedₚ
open import Data.List.Relation.Unary.AllPairs as AllPairs
import      Data.List.Relation.Unary.AllPairs.Properties as AllPairsₚ
open import Data.List.Membership.Propositional

open import Function.Base using (_∘_; _$_; flip)

open import Relation.Binary as B
import      Relation.Binary.Properties.DecTotalOrder as DecTotalOrderProperties
open import Relation.Binary.PropositionalEquality using (_≡_)
import      Relation.Binary.PropositionalEquality as ≡ hiding ([_])
import      Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Relation.Nullary
open import Relation.Unary as U hiding (_∈_)

-- stdlib
foldr-preservesʳ : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p} {f : A → B → B}
  → (∀ x {y} → P y → P (f x y))
  → ∀ {e} → P e → ∀ xs → P (foldr f e xs)
foldr-preservesʳ pres Pe []       = Pe
foldr-preservesʳ pres Pe (x ∷ xs) = pres _ (foldr-preservesʳ pres Pe xs)

-- stdlib
module _ {a p q} {A : Set a} {P : U.Pred A p} {Q : U.Pred A q} where
  All-mapWith∈ : ∀ {xs : List A} → (∀ {x} → x ∈ xs → P x → Q x) → All P xs → All Q xs
  All-mapWith∈          f []         = []
  All-mapWith∈ {x ∷ xs} f (px ∷ pxs) =
    f (here ≡.refl) px ∷ All-mapWith∈ (λ x∈xs Px → f (there x∈xs) Px) pxs

module _ {a p} {A : Set a} {P : U.Pred A p} where
  All-singleton⁺ : ∀ {x} → P x → All P [ x ]
  All-singleton⁺ px = px ∷ []

  All-reverse⁺ : ∀ {xs} → All P xs → All P (reverse xs)
  All-reverse⁺ {[]}     []         = []
  All-reverse⁺ {x ∷ xs} (px ∷ pxs) =
    ≡.subst (All P) (≡.sym $ Listₚ.unfold-reverse x xs)
            (Allₚ.++⁺ (All-reverse⁺ pxs) (All-singleton⁺ px))

module _ {a r} {A : Set a} {R : Rel A r} where

  -- AllPairs-map⁻
  -- AllPairs-mapMaybe⁺ : (∀ x y → R x y → R (f x) (f y)) → AllPairs R xs → AllPairs R (mapMaybe f xs)
  -- AllPairs mapMaybe⁻

  AllPairs-singleton⁺ : ∀ x → AllPairs R [ x ]
  AllPairs-singleton⁺ x = [] ∷ []

  AllPairs-pair : ∀ {x y} → R x y → AllPairs R (x ∷ y ∷ [])
  AllPairs-pair Rxy = All-singleton⁺ Rxy ∷ AllPairs-singleton⁺ _

  AllPairs-++⁻ʳ : ∀ xs {ys} → AllPairs R (xs ++ ys) → AllPairs R ys
  AllPairs-++⁻ʳ []       rxs        = rxs
  AllPairs-++⁻ʳ (x ∷ xs) (rx ∷ rxs) = AllPairs-++⁻ʳ xs rxs

  AllPairs-++⁻ˡ : ∀ xs {ys} → AllPairs R (xs ++ ys) → AllPairs R xs
  AllPairs-++⁻ˡ []       rxs        = []
  AllPairs-++⁻ˡ (x ∷ xs) (rx ∷ rxs) = Allₚ.++⁻ˡ xs rx ∷ AllPairs-++⁻ˡ xs rxs

  AllPairs-++⁻-AllAll : ∀ xs {ys} →
    AllPairs R (xs ++ ys) → All (λ x → All (R x) ys) xs
  AllPairs-++⁻-AllAll []       rxs        = []
  AllPairs-++⁻-AllAll (x ∷ xs) (rx ∷ rxs) = Allₚ.++⁻ʳ _ rx ∷ AllPairs-++⁻-AllAll xs rxs

  AllPairs-++⁻ : ∀ xs {ys} → AllPairs R (xs ++ ys) →
                 AllPairs R xs × AllPairs R ys × All (λ x → All (R x) ys) xs
  AllPairs-++⁻ xs rxs = AllPairs-++⁻ˡ xs rxs , AllPairs-++⁻ʳ xs rxs , AllPairs-++⁻-AllAll xs rxs

  AllPairs-∷ʳ⁺ : ∀ {x xs} → AllPairs R xs → All (flip R x) xs → AllPairs R (xs ∷ʳ x)
  AllPairs-∷ʳ⁺ {x} {xs} rxs px =
    AllPairsₚ.++⁺ rxs (AllPairs-singleton⁺ x) (All.map All-singleton⁺ px)

  AllPairs-∷ʳ⁻ : ∀ {x xs} → AllPairs R (xs ∷ʳ x) → AllPairs R xs × All (flip R x) xs
  AllPairs-∷ʳ⁻ {x} {xs} rxs with AllPairs-++⁻ xs rxs
  ... | rxs′ , _ , pxs = rxs′ , All.map Allₚ.singleton⁻ pxs

  AllPairs-reverse⁺ : ∀ {xs} → AllPairs (flip R) xs → AllPairs R (reverse xs)
  AllPairs-reverse⁺ {[]}     []         = []
  AllPairs-reverse⁺ {x ∷ xs} (rx ∷ rxs) =
    ≡.subst (AllPairs R) (≡.sym $ Listₚ.unfold-reverse x xs)
            (AllPairs-∷ʳ⁺ (AllPairs-reverse⁺ rxs) (All-reverse⁺ rx))

module _ {a r} {A : Set a} {R : Rel A r} where
  AllPairs-sym-reverse⁺ : Symmetric R → ∀ {xs} → AllPairs R xs → AllPairs R (reverse xs)
  AllPairs-sym-reverse⁺ sym = AllPairs.map sym ∘ AllPairs-reverse⁺

AllAll : ∀ {a b r} {A : Set a} {B : Set b} → REL A B r → List A → List B → Set _
AllAll R xs ys = All (λ x → All (R x) ys) xs

module _ {a r} {A : Set a} {R : Rel A r} where
  AllPairs-reverse⁻ : ∀ {xs} → AllPairs R (reverse xs) → AllPairs (flip R) xs
  AllPairs-reverse⁻ {xs} rxs =
    ≡.subst (AllPairs (flip R)) (Listₚ.reverse-involutive xs)
            (AllPairs-reverse⁺ rxs)

  -- concat⁻
{-
  AllPairs-concat⁺ : ∀ {xss} → AllAll (AllAll R) xss xss →
                     All (AllPairs R) xss → AllPairs R (concat xss)
  AllPairs-concat⁺ {[]}       rxss         pxss         = []
  AllPairs-concat⁺ {xs ∷ xss} (rxs ∷ rxss) (pxs ∷ pxss) =
    AllPairsₚ.++⁺ {xs = xs} pxs (AllPairs-concat⁺ {! proj₂ (unconsʳ rxs)  !} pxss) {!   !}
-}
  AllPairs-universal : B.Universal R → U.Universal (AllPairs R)
  AllPairs-universal u []       = []
  AllPairs-universal u (x ∷ xs) = All.universal (u _) _ ∷ AllPairs-universal u xs

  AllPairs-replicate⁺ : ∀ n {x} → R x x → AllPairs R (replicate n x)
  AllPairs-replicate⁺ ℕ.zero    Rxx = []
  AllPairs-replicate⁺ (ℕ.suc n) Rxx = Allₚ.replicate⁺ n Rxx ∷ AllPairs-replicate⁺ n Rxx

  AllPairs-replicate⁻ : ∀ {n x} → AllPairs R (replicate (ℕ.suc (ℕ.suc n)) x) → R x x
  AllPairs-replicate⁻ (pxs ∷ rxs) = Allₚ.replicate⁻ pxs

  -- AllPairs-drop⁺

  -- AllPairs-zipWith⁺ :

module _ {c e} (S : Setoid c e) where
  open Setoid S
  open ListSetoidEquality S
  Linked-resp-≋ : ∀ {r} {R : Rel Carrier r} →
                  R Respects₂ _≈_ → (Linked R) Respects _≋_
  Linked-resp-≋ resp [] [] = []
  Linked-resp-≋ resp (_ ∷ []) [-] = [-]
  Linked-resp-≋ resp (e₁ ∷ e₂ ∷ xs≋ys) (x ∷ l) =
   (proj₂ resp e₁ $ proj₁ resp e₂ x) ∷ Linked-resp-≋ resp (e₂ ∷ xs≋ys) l

module _ {a r} {A : Set a} {R : Rel A r} where

-- Linked-pair : R x y →

  Linked-++⁻ʳ : ∀ xs {ys} → Linked R (xs ++ ys) → Linked R ys
  Linked-++⁻ʳ []               rxs       = rxs
  Linked-++⁻ʳ (x ∷ []) {[]}    rxs       = []
  Linked-++⁻ʳ (x ∷ []) {_ ∷ _} (y ∷ rxs) = rxs
  Linked-++⁻ʳ (x ∷ y ∷ xs)     (_ ∷ rxs) = Linked-++⁻ʳ (y ∷ xs) rxs

  Linked-++⁻ˡ : ∀ xs {ys} → Linked R (xs ++ ys) → Linked R xs
  Linked-++⁻ˡ []           rxs        = []
  Linked-++⁻ˡ (x ∷ [])     rxs        = [-]
  Linked-++⁻ˡ (x ∷ y ∷ xs) (rx ∷ rxs) = rx ∷ Linked-++⁻ˡ (y ∷ xs) rxs

  Linked-∷⁻ʳ : ∀ {x xs} → Linked R (x ∷ xs) → Linked R xs
  Linked-∷⁻ʳ {x = x} = Linked-++⁻ʳ [ x ]

  Linked-∷ʳ⁻ˡ : ∀ {xs x} → Linked R (xs ∷ʳ x) → Linked R xs
  Linked-∷ʳ⁻ˡ {xs = xs} = Linked-++⁻ˡ xs
{-
  Linked-∷ʳ₂⁺ : ∀ {xs x y} → Linked R (xs ∷ʳ x) → R x y → Linked R (xs ∷ʳ x ∷ʳ y)
  Linked-∷ʳ₂⁺ {[]} {x} {y} [-] Rxy = Rxy ∷ [-]
  Linked-∷ʳ₂⁺ {x′ ∷ xs} {x} {y} l Rxy = {!   !}

  Linked-reverse⁺ : ∀ {xs} → Linked (flip R) xs → Linked R (reverse xs)
  Linked-reverse⁺ {[]} l = []
  Linked-reverse⁺ {x ∷ []} l = [-]
  Linked-reverse⁺ {x ∷ y ∷ xs} (Rxy ∷ l) = {! Rxy ∷   !}
-}

  -- Linked-inits⁺
  -- respects

  -- Linked-++⁻-middle : ∀ xs {ys} → Linked R (xs ++ ys) → Last (λ x → First (R x) ys) xs

  Linked-universal : B.Universal R → U.Universal (Linked R)
  Linked-universal u [] = []
  Linked-universal u (x ∷ []) = [-]
  Linked-universal u (x ∷ x₁ ∷ xs) = u x x₁ ∷ Linked-universal u (x₁ ∷ xs)

  module _ (R-trans : Transitive R) where
    private
      L⇒A : ∀ {xs} → Linked R xs → AllPairs R xs
      L⇒A = Linkedₚ.Linked⇒AllPairs R-trans
    Linked-trans-∷ : ∀ {x xs} → All (R x) xs → Linked R xs → Linked R (x ∷ xs)
    Linked-trans-∷ a l = Linkedₚ.AllPairs⇒Linked (a ∷ L⇒A l)

    Linked-trans-head : ∀ {x xs} → Linked R (x ∷ xs) → All (R x) xs
    Linked-trans-head = AllPairs.head ∘ L⇒A

{-
Linked-++⁺ : Linked R xs → Linked R ys → Frist (λ x → Last (λ y → R xy) ys) xs → Linked R (xs ++ ys)
-}

-- stdlib?
AllPairs-trans-∷₂ : ∀ {a r} {A : Set a} {R : Rel A r} {x y ys} →
  Transitive R →
  R x y → AllPairs R (y ∷ ys) → AllPairs R (x ∷ y ∷ ys)
AllPairs-trans-∷₂ R-trans Rxy rxs@(px ∷ _) =
  (Rxy ∷ All.map (λ {z} Ryz → R-trans Rxy Ryz) px) ∷ rxs
  -- Transitive R → AllPairs R (xs ∷ʳ v) → AllPairs R (v ∷ ys)
  -- AllPairs R (xs ++ [ v ] ++ ys)

  -- Transitive R → length ys ≥ 1 → AllPairs R (xs ++ ys) → AllPairs R (ys ++ zs) →
  -- AllPairs (xs ++ ys ++ zs)


text:
module ExtractFunction where
open import Data.List
open import ParseTree
open import Data.Nat
open import Data.String hiding (_++_)
open import ScopeState using (ScopeState ; ScopeEnv ; replaceID ; liftIO ; getUniqueIdentifier)
open import ScopeParseTree
open import AgdaHelperFunctions
open import Typing
open import Data.Bool
open import MatchUpNames
open import Category.Monad.State
open import Data.Product
open import Data.Maybe
open import Relation.Nullary
open import Data.Unit using (⊤ ; tt)
open import Data.Nat.Show
open import ParseTreeOperations

--TODO: actually, it is okay if the module has no name - in this case we do not need to rename it.
getIDForModule : List ParseTree -> ScopeState Identifier
getIDForModule [] = ScopeState.fail "This module seems to have no name"
getIDForModule (moduleName id range₁ ∷ p) = ScopeState.return id
getIDForModule (x ∷ xs) = getIDForModule xs

record ExtractionEnv : Set where
  constructor extEnv
  field
   stuffBeforeFunc : List ParseTree
   stuffAfterFunc : List ParseTree
   rightHandSideBuilder : Maybe (Expr -> Expr)
   extractedExpr : Maybe Expr
   holesPassed : ℕ
   functionRebuilder : Maybe (Expr -> ParseTree)
   oldFunctionName : Maybe Identifier

ExtractionState : Set -> Set
ExtractionState = StateT ExtractionEnv ScopeState

runExtractionState :
    {a : Set} -> ExtractionState a -> ExtractionEnv -> ScopeState a
runExtractionState eMonad e = do
      (result , newState) <- eMonad e
      return result
    where open RawMonadState (StateTMonadState ScopeEnv (SumMonadT IOMonad String))

liftScopeState : {a : Set} -> ScopeState a -> ExtractionState a
liftScopeState action ee = do
  a <- action
  return (a , ee)
  where open RawMonadState (StateTMonadState ScopeEnv (SumMonadT IOMonad String))

open RawMonadState (StateTMonadState ExtractionEnv (StateTMonad ScopeEnv (SumMonadT IOMonad String)))

fail : {a : Set} -> String -> ExtractionState a
fail s = liftScopeState $ ScopeState.fail s

--assuming that start < end
isInside : Range -> ℕ -> ℕ -> Bool
isInside (range lastUnaffected lastAffected) start end
  with end ≤? lastUnaffected | lastAffected ≤? suc start
... | no p | no q = true
... | p | q = false

isInIdent : Identifier -> ℕ -> ℕ -> Bool
isInIdent (identifier name isInRange scope declaration {b}{c} {c2}) start end
  with isInRange start | isInRange end
... | after | _ = false
... | _ | before = false
... | _ | _ = true

findPartInExpr : Expr -> ℕ -> ℕ -> ExtractionState Bool
findPartInExpr (numLit {value}
    {r} {c} {c2}) start end
      with isInside r start end
... | true = do
      extEnv x y f expr h g n  <- get
      put $ extEnv x y (just(λ a -> a)) (just $ numLit {value} {r} {c} {c2}) h g n
      return true
... | false = return false
findPartInExpr (ident id) start end
  with isInIdent id start end
... | false = return false
... | true = do
    extEnv x y f expr h g n <- get
    put $ extEnv x y (just(λ a -> a)) (just $ ident id) h g n
    return true
findPartInExpr (hole {t} {p} {c} {c2}) start end
    with isInside p start end
... | true = do
  extEnv x y f expr h g n  <- get
  put $ extEnv x y (just(λ a -> a)) (just $ hole {t} {p} {c} {c2}) h g n
  return true
... | false = return false
findPartInExpr (functionApp e e₁ {false} ) start end = do
    true <- findPartInExpr e₁ start end
      where false -> do
                  true <- findPartInExpr e start end
                    where false -> return false
                  -- here we want to extract some subexpression of e
                  -- so we rebuild it with rebuilder f and put it in the functionApp
                  extEnv x y (just f) expr h g n <- get
                    where _ -> fail "Got no function despite extraction"
                  put $ extEnv x y (just(λ x -> functionApp (f x) e₁ {false})) expr h g n
                  return true
    extEnv x y (just f) expr h g n <- get
      where _ -> fail "Got no function despite extraction"
    true <- findPartInExpr e start end
      where false -> do -- extract only (part of) e₁
                put $ extEnv x y (just (λ a -> functionApp e (f a) {false})) expr h g n
                return true
    -- at this point we realize we want to extract the entire
    -- functionApp
    -- Therefore, we need to extract entire e and e₁ regardless of
    -- how far into it the selection extends.
    --extEnv x y f expr h g n <- get
    put $ extEnv x y (just (λ x -> x)) (just $ functionApp e e₁ {false} ) h g n
    return true
findPartInExpr (functionApp e e₁ {true} ) start end = do
  true <- findPartInExpr e start end
    where false -> do
           true <- findPartInExpr e₁ start end
            where false -> return false
           extEnv x y (just f) expr h g n <- get
            where _ -> fail "Got no function despite extraction"
           put $ extEnv x y (just(λ x -> functionApp e (f x) {true} )) expr h g n
           return true
  extEnv x y (just f) expr h g n <- get
   where _ -> fail "Got no function despite extraction"
  namedArgument sign <- return e
   where _ -> do
          -- e is not a named argument so can be extracted by itself
          true <- findPartInExpr e₁ start end
           where false -> do
                  put $ extEnv x y (just (λ a -> functionApp (f e) e₁ {true})) expr h g n
                  return true
          put $ extEnv x y (just (λ x -> x)) (just $ functionApp e e₁ {true}) h g n
          return true
  put $ extEnv x y (just $ λ x -> x) (just $ functionApp e e₁ {true}) h g n
  return true
findPartInExpr (implicit x) start end = do
  true <- findPartInExpr x start end
    where false -> return false
  extEnv x y (just f) expr h g n <- get
    where _ -> fail "Extraction failed"
  put $ extEnv x y (just(λ a -> implicit $ f a)) expr h g n
  return true
findPartInExpr (underscore {p} {c1} {c2}) start end with isInside p start end
... | true = do
  extEnv x y f expr h g n  <- get
  put $ extEnv x y (just(λ a -> a)) (just $ underscore {p} {c1} {c2}) h g n
  return true
... | false = return false
findPartInExpr (namedArgument (typeSignature funcName funcType) {b} {bef} {aft}) start end
  with isInIdent funcName start end
-- can't extract just the name of a variable
... | true =  do
            extEnv x y f expr h g n <- get
            put $ extEnv x y (just $ λ x -> x)
              (just $ namedArgument (typeSignature funcName funcType)  {b} {bef} {aft}) h g n
            return true
... | false = do
    true <- findPartInExpr funcType start end
      where false -> return false
    extEnv x y (just f) expr h g n  <- get
      where _ -> fail "No function in state"
    put $ extEnv x y (just $ λ x -> namedArgument (typeSignature funcName $ f x) {b} {bef} {aft}) expr h g n
    return true

sameNameAndStatus : Identifier -> Identifier -> Bool
sameNameAndStatus (identifier name isInRange scope declaration {inScope1}) (identifier name₁ isInRange₁ scope₁ declaration₁ {inScope2}) = (name == name₁) ∧ (not $ inScope1 xor inScope2)

isIdInExpr : (whatToSearchFor : Identifier) -> (whereToSearch : Expr) -> Bool
isIdInExpr i (ident identifier₁) = sameNameAndStatus i identifier₁
isIdInExpr i (functionApp x x₁) = isIdInExpr i x ∨ isIdInExpr i x₁
isIdInExpr _ _ = false

countHole : ExtractionState ⊤
countHole = do
  extEnv b a func exp h g n <- get
  put $ extEnv b a func exp (suc h) g n
  return tt

mapState : {A B : Set} -> (A -> ExtractionState B) -> List A -> ExtractionState (List B)
mapState f [] = return []
mapState f (x ∷ list) = do
  x1 <- f x
  xs <- mapState f list
  return (x1 ∷ xs)

countHolesInSignature : TypeSignature -> ExtractionState ⊤

countHolesInExpr : Expr -> ExtractionState ⊤
countHolesInExpr hole = countHole
countHolesInExpr (functionApp e e₁) = do
  countHolesInExpr e
  countHolesInExpr e₁
countHolesInExpr (namedArgument arg) = countHolesInSignature arg
countHolesInExpr _ = return tt

countHolesInSignature (typeSignature funcName funcType) =
  countHolesInExpr funcType

countHolesInTree : ParseTree -> ExtractionState ⊤
countHolesInTree (signature signature₁ range₁) = countHolesInSignature signature₁
countHolesInTree (functionDefinition definitionOf params body range₁) = countHolesInExpr body
countHolesInTree (dataStructure dataName parameters indexInfo constructors range₁) = do
  mapState countHolesInSignature parameters
  mapState countHolesInSignature constructors
  countHolesInExpr indexInfo
countHolesInTree _ = return tt

findPartToExtract : List ParseTree -> ℕ -> ℕ -> ExtractionState ⊤
findPartToExtract [] start end = fail "Found nothing that can be extracted"
findPartToExtract (functionDefinition definitionOf params body (range a z) ∷ e)
      start end with (suc a) ≤? start | end ≤? z
... | yes p | yes q = do
      true <- findPartInExpr body start end
        where false -> fail "Command start and end must be in the function body"
      extEnv bef aft func exp h g n <- get
      put $ extEnv bef e func exp h (just (λ x -> functionDefinition definitionOf params x (range a z))) $ just definitionOf
      just ex <- return exp
        where nothing -> fail "Didn't get an expression to extract"
      mapState countHolesInTree bef
      return tt
findPartToExtract (p ∷ ps) start end | yes a | no b = do
    extEnv b a func exp h g n  <- get
    put $ extEnv (b ∷ʳ p) a func exp h g n
    findPartToExtract ps start end
... | p | q = fail "Command start and end not fully inside any function"
findPartToExtract (p ∷ ps) start end = do
    extEnv b a func exp h g n <- get
    put $ extEnv (b ∷ʳ p) a func exp h g n
    findPartToExtract ps start end

makeTypeFromTypes : List Expr -> ExtractionState Expr
makeTypeFromTypes [] = fail "Can't make type from nothing"
makeTypeFromTypes (x ∷ []) = return x
makeTypeFromTypes (x ∷ xs) = do
    y <- makeTypeFromTypes xs
    return $ functionApp x y {true}

makeExprFromExprs : List Expr -> ExtractionState Expr
makeExprFromExprs [] = fail "Can't make expr from nothing"
makeExprFromExprs (x ∷ []) = return x
makeExprFromExprs (x ∷ l) = do
  y <- makeExprFromExprs l
  return $ functionApp y x {false}

-- List of type signatures is environment. Contains all variables,
-- including not-in-scope. Return list is the new function's environment.
filterEnvironment : Expr -> List TypeSignature -> (extractedExp : Expr) -> ExtractionState (List TypeSignature)
filterEnvironment resultType [] varsUsed = return []
filterEnvironment resultType (typeSignature funcName funcType ∷ environment) extractedExpr = do
  filteredEnv <- filterEnvironment resultType environment extractedExpr
  let isInExtractedExpr = isIdInExpr funcName extractedExpr
  let typesToCheck = Data.List.map (λ { (typeSignature n t) -> t}) filteredEnv
  isInTypes <- mapState (findInType funcName) typesToCheck
  let isIn = or isInTypes
  if isIn ∨ isInExtractedExpr
   then return $ (typeSignature funcName funcType) ∷ filteredEnv
   else return filteredEnv
 where
  findInType : Identifier -> Expr -> ExtractionState Bool

  findInType id (namedArgument (typeSignature funcName funcType)) = findInType id funcType
  findInType id (functionApp t t₁ {true}) = do
    one <- findInType id t
    two <- findInType id t₁
    return $ one ∨ two
  findInType id expression = return $ isIdInExpr id expression

bringIdInScope : Identifier -> Identifier
bringIdInScope (identifier name isInRange scope declaration {inScope} {a} {b}) = identifier name isInRange scope declaration {true} {a}{b}

containsIdInSign : TypeSignature -> Identifier -> Bool

containsInType : Expr -> Identifier -> Bool

containsInType (namedArgument arg) i = containsIdInSign arg i
containsInType (functionApp t t₁ {true}) i = containsInType t i ∨ containsInType t₁ i
containsInType expression i = isIdInExpr i expression

containsIdInSign (typeSignature name funcType) id = sameNameAndStatus name id ∨ containsInType funcType id

isInScope : Identifier -> Bool
isInScope (identifier _ _ _ _ {isInScope}) = isInScope

bringExprInScope : Expr -> Expr
bringExprInScope (ident id) = ident $ bringIdInScope id
bringExprInScope (functionApp e e₁ {b} ) = functionApp (bringExprInScope e) (bringExprInScope e₁) {b}
bringExprInScope (implicit e) = implicit $ bringExprInScope e
bringExprInScope x = x

bringInScope : Expr -> Expr
bringSignatureInScope : TypeSignature -> TypeSignature
bringSignatureInScope (typeSignature funcName funcType) =
  typeSignature (bringIdInScope funcName) $ bringInScope funcType

bringInScope (namedArgument arg {b} {bef} {aft}) = namedArgument (bringSignatureInScope arg) {b} {bef} {aft}
bringInScope (functionApp t t₁ {true} ) = functionApp (bringInScope t) (bringInScope t₁) {true}
bringInScope expression = bringExprInScope expression
renameNotInScopeExpr : Identifier -> Identifier -> Expr -> Expr
renameNotInScopeExpr (identifier name₁ isInRange₁ scope₁ declaration₁) to (ident (identifier name isInRange scope declaration {false} {b} {a})) with name == name₁
renameNotInScopeExpr (identifier name₁ isInRange₁ scope₁ declaration₁) (identifier name₂ isInRange₂ scope₂ declaration₂) (ident (identifier name isInRange scope declaration {false} {b} {a})) | true = ident $ identifier name₂ isInRange₂ scope₂ declaration₂ {false}{b} {a}
... | false = ident $ identifier name isInRange scope declaration {false} {b} {a}
renameNotInScopeExpr from to (functionApp e e₁ {b} ) =
  functionApp (renameNotInScopeExpr from to e) (renameNotInScopeExpr from to e₁) {b}
renameNotInScopeExpr from to (implicit e) = implicit $ renameNotInScopeExpr from to e
renameNotInScopeExpr _ _ x = x

renameNotInScopeOfName : Identifier -> Identifier -> Expr -> Expr

renameNotInScopeSign : Identifier -> Identifier -> TypeSignature -> TypeSignature
renameNotInScopeSign from to (typeSignature funcName funcType) =
  typeSignature funcName $ renameNotInScopeOfName from to funcType

renameNotInScopeOfName from to (namedArgument arg {b} {bef} {aft}) = namedArgument  (renameNotInScopeSign from to arg) {b} {bef} {aft}
renameNotInScopeOfName from to (functionApp signs signs₁ {true} ) =
  functionApp (renameNotInScopeOfName from to signs) (renameNotInScopeOfName from to signs₁) {true}
renameNotInScopeOfName from to expression = renameNotInScopeExpr from to expression

-- returns list of types, which are explicit or implicit named arguments
-- and a list of expressions which is the left-hand side of the new function, i.e. idents.
signatureToType : Expr -> List TypeSignature -> ExtractionState (List Expr × List Expr)
signatureToType result [] = return $ (result ∷ []) , []
signatureToType result (typeSignature funcName funcType ∷ laterSigns) = do
  let inScopeType = bringInScope funcType
  (restOfSigns , exprs) <- signatureToType result laterSigns
  false <- return $ isInScope funcName
    where true -> do -- in this case, we plainly don't want to rename anything
                    let newSign = namedArgument (typeSignature funcName funcType) {true} {[]}{[]}
                    return $ newSign ∷  restOfSigns , ident funcName ∷ exprs
  -- Do we need to rename the current variable?
  true <- return $ or $ Data.List.map (λ x -> containsIdInSign x $ bringIdInScope funcName) laterSigns
    where false -> do
              let newSign = namedArgument (typeSignature funcName funcType) {false} {[]}{[]}
              return $ newSign ∷  restOfSigns , exprs
  liftScopeState $ liftIO $ output "Need to rename a variable"
  newName <- liftScopeState getUniqueIdentifier
  let renamedSigns = Data.List.map (renameNotInScopeOfName funcName newName) restOfSigns
  return $ namedArgument (typeSignature newName inScopeType) {false} {[]}{[]} ∷ renamedSigns , exprs

placeInRightPlace : Identifier -> (placeOverTypeSignature : Bool) -> ParseTree -> ParseTree -> List ParseTree -> List ParseTree
placeInRightPlace oldFunctionName _ newsign newdef [] = newsign ∷ newdef ∷ []
placeInRightPlace oldFunctionName false newsign newdef (functionDefinition definitionOf params body range₁ ∷ program) with sameId oldFunctionName definitionOf
...| false = functionDefinition definitionOf params body range₁ ∷ placeInRightPlace oldFunctionName false newsign newdef program
... | true = newsign ∷ newdef ∷ functionDefinition definitionOf params body range₁ ∷ program
placeInRightPlace oldFunctionName true newsign newdef (signature (typeSignature funcName funcType) range₁ ∷ program) with sameId oldFunctionName funcName
... | false = signature (typeSignature funcName funcType) range₁ ∷ placeInRightPlace oldFunctionName true newsign newdef program
... | true = newsign ∷ newdef ∷  signature (typeSignature funcName funcType) range₁ ∷ program
placeInRightPlace x y z a (p ∷ program) = p ∷ placeInRightPlace x y z a program

doExtraction : List ParseTree -> ℕ -> ℕ -> String -> ExtractionState (List ParseTree)
doExtraction program startPoint endPoint filename = do
  scoped <- liftScopeState $ scopeParseTreeList program
  -- TODO: Assuming that the module only has a simple name.
  -- Otherwise, need to calculate the right name.
  identifier name _ _ declaration <- liftScopeState $ getIDForModule scoped
  liftScopeState $ replaceID declaration "RefactorAgdaTemporaryFile"
  renamedInputProgram <- liftScopeState $ matchUpNames scoped
  findPartToExtract renamedInputProgram startPoint endPoint
  extEnv b a (just expBuilder) (just extractedExp) h (just functionBuilder) (just oldFunctionName)  <- get
    where _ -> fail "An error in doExtraction"
  let programWithNewHole = b ++
        ((functionBuilder $ expBuilder $ hole {""} {range 0 0} {[]} {[]})∷ a)
  (resultTypeNewFunc ∷ []) <- liftScopeState $ liftIO $ getTypes
                              programWithNewHole h
                                (extractedExp ∷ []) filename
            where _ -> fail "Something happened in InteractWithAgda"
  environment <- liftScopeState $ liftIO $ getEnvironment programWithNewHole h filename
  newFuncName <- liftScopeState $ getUniqueIdentifier
  newFuncEnv <- filterEnvironment resultTypeNewFunc environment extractedExp
  (newFuncSignParts , newFuncArgNames) <- signatureToType resultTypeNewFunc newFuncEnv
  newFuncType <- makeTypeFromTypes $ newFuncSignParts
  let newFuncSignature = signature (typeSignature newFuncName newFuncType) (range 0 0)
  let newFuncDefinition = functionDefinition newFuncName newFuncArgNames extractedExp (range 0 0)
  replacingExpr <- makeExprFromExprs $ reverse $ ident newFuncName ∷ newFuncArgNames
  let oldFunction = functionBuilder $ expBuilder $ replacingExpr
  let placeBelowTypeSignature = isIdInExpr oldFunctionName extractedExp
  let completeCode = placeInRightPlace oldFunctionName (not placeBelowTypeSignature) newFuncSignature newFuncDefinition b ++
        (oldFunction ∷ a)
  scopeCompleted <- liftScopeState $ scopeParseTreeList completeCode
  identifier _ _ _ d <- liftScopeState $ getIDForModule scopeCompleted
  liftScopeState $ replaceID d name
  liftScopeState $ matchUpNames scopeCompleted

extract : List ParseTree -> ℕ -> ℕ -> String -> ScopeState (List ParseTree)
extract p s e f = runExtractionState (doExtraction p s e f) $ extEnv [] [] nothing nothing 0 nothing nothing


text:
-- Andreas, James, 2011-11-24
-- trigger error message 'NeedOptionCopatterns'
module NeedOptionCopatterns where

record Bla : Set2 where
  field
    bla : Set1
open Bla

f : Bla
bla f = Set
-- should request option --copatterns

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Data.Int where

open import Algebra.Group
open import Classes
open import Core
open import Data.Int.Core
open import Data.Int.Core public
  using (ℤ; ℤ-Negative; ℤ-Number; negsuc; pos)

ℤ,+ : Group
ℤ,+ =
  record {
    semigroup = record {
      A = ℤ;
      Eq = PropEq ℤ;
      semigroupOver = record {
        _⋄_ = _+_;
        ⋄-cong = cong2 _+_;
        assoc = Props.+-assoc
      }
    };
    isGroup = record {
      isMonoid = record {
        id = 0;
        left-id = Props.+-left-id;
        right-id = Props.+-right-id
      };
      iso = λ x → record {
        inv = neg x;
        left-inv = Props.+-left-inv x;
        right-inv = Props.+-right-inv x
      };
      inv-cong = cong neg
    }
  }

ℤ,* : Monoid
ℤ,* =
  record {
    semigroup = record {
      A = ℤ;
      Eq = PropEq ℤ;
      semigroupOver = record {
        _⋄_ = _*_;
        ⋄-cong = cong2 _*_;
        assoc = Props.*-assoc
      }
    };
    isMonoid = record {
      id = 1;
      left-id = Props.*-left-id;
      right-id = Props.*-right-id
    }
  }

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


text:
module Luau.Syntax.ToString where

open import Agda.Builtin.Float using (primShowFloat)
open import Luau.Syntax using (Block; Stat; Expr; VarDec; FunDec; nil; var; var_∈_; addr; _$_; function_is_end; return; local_←_; _∙_; done; block_is_end; _⟨_⟩; _⟨_⟩∈_; number; BinaryOperator; +; -; *; /; binexp)
open import FFI.Data.String using (String; _++_)
open import Luau.Addr.ToString using (addrToString)
open import Luau.Type.ToString using (typeToString)
open import Luau.Var.ToString using (varToString)

varDecToString : ∀ {a} → VarDec a → String
varDecToString (var x) = varToString x
varDecToString (var x ∈ T) =  varToString x ++ " : " ++ typeToString T

funDecToString : ∀ {a} → FunDec a → String
funDecToString ("" ⟨ x ⟩∈ T) = "function(" ++ varDecToString x ++ "): " ++ typeToString T
funDecToString ("" ⟨ x ⟩) = "function(" ++ varDecToString x ++ ")"
funDecToString (f ⟨ x ⟩∈ T) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ "): " ++ typeToString T
funDecToString (f ⟨ x ⟩) = "function " ++ varToString f ++ "(" ++ varDecToString x ++ ")"

binOpToString : BinaryOperator → String
binOpToString + = "+"
binOpToString - = "-"
binOpToString * = "*"
binOpToString / = "/"

exprToString′ : ∀ {a} → String → Expr a → String
statToString′ : ∀ {a} → String → Stat a → String
blockToString′ : ∀ {a} → String → Block a → String

exprToString′ lb nil =
  "nil"
exprToString′ lb (addr a) =
  addrToString(a)
exprToString′ lb (var x) =
  varToString(x)
exprToString′ lb (M $ N) =
  (exprToString′ lb M) ++ "(" ++ (exprToString′ lb N) ++ ")"
exprToString′ lb (function F is B end) =
  funDecToString F ++ lb ++
  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
  "end"
exprToString′ lb (block b is B end) =
  "(" ++ b ++ "()" ++ lb ++
  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
  "end)()"
exprToString′ lb (number x) = primShowFloat x
exprToString′ lb (binexp x op y) = exprToString′ lb x ++ " " ++ binOpToString op ++ " " ++ exprToString′ lb y

statToString′ lb (function F is B end) =
  "local " ++ funDecToString F ++ lb ++
  "  " ++ (blockToString′ (lb ++ "  ") B) ++ lb ++
  "end"
statToString′ lb (local x ← M) =
  "local " ++ varDecToString x ++ " = " ++ (exprToString′ lb M)
statToString′ lb (return M) =
  "return " ++ (exprToString′ lb M)

blockToString′ lb (S ∙ done) = statToString′ lb S
blockToString′ lb (S ∙ B) = statToString′ lb S ++ lb ++ blockToString′ lb B
blockToString′ lb (done) = ""

exprToString : ∀ {a} → Expr a → String
exprToString = exprToString′ "\n"

statToString : ∀ {a} → Stat a → String
statToString = statToString′ "\n"

blockToString : ∀ {a} → Block a → String
blockToString = blockToString′ "\n"


text:
module MJ.Examples.DynDispatch where

open import Prelude
import Data.Vec.All as Vec∀
open import Data.Star
open import Data.Bool
open import Data.List
open import Data.List.Any
open import Data.List.Membership.Propositional
open import Data.List.All hiding (lookup)
open import Data.Product hiding (Σ)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable
open import Data.String

open import MJ.Types

open import MJ.Classtable.Core 2

{-

  // We test field inheritance and
  // method call dispatching combining super calls and dynamic dispatch.
  // The Agda test is equivalent to the following Java code

  class Int {

      int x;

      public Int(int i) {
          this.x = i;
          return;
      }

      public int get() {
          System.out.println("never");
          return x;
      }

      public int set (Int y) {
          x = y.x;

          // in the test main this should dispatch to
          // the implementation of the child Int2
          return this.get();
      }
  }

  class Int2 extends Int {

      public Int2(int i) {
          super(i);
      }

      public int get() {
          return x + 1;
      }

      public int set (Int y) {
          // test super dispatch
          return super.set(new Int(y.x + 1));
      }
  }

  class Main {
      public static void main(String[] args) {
          Int y = new Int(18);
          Int2 x = new Int2(0);

          // should print 20
          // because we use the set(..) and get() of Int2
          // which both increment with one
          System.out.println(x.set(y));
      }
  }

-}

INT : Cid 2
INT = (cls (# 0))

INT+ : Cid 2
INT+ = (cls (# 1))

decls : (ns : NS) → List (String × typing ns)
decls METHOD =
    ("get" , ([] , int))
  ∷ ("set" , (ref INT ∷ [] , int))
  ∷ []
decls FIELD =
    ("x" , int)
  ∷ []

-- override methods; no extra fields
decls+ : (ns : NS) → List (String × typing ns)
decls+ METHOD =
    ("get" , ([] , int))
  ∷ ("set" , (ref INT ∷ [] , int))
  ∷ []
decls+ FIELD = []

IntegerSig = (class Object (int ∷ []) decls)
Integer+Sig = (class INT (int ∷ []) decls+)

-- class table signature
Σ : Classtable
Σ = record {
  Σ = λ{
    (cls zero) → IntegerSig ;
    (cls (suc zero)) → Integer+Sig ;
    (cls (suc (suc ()))) ;
    Object → ObjectClass} ;
  founded = refl ;
  rooted = λ{
    (cls zero) → super ◅ ε ;
    (cls (suc zero)) → super ◅ super ◅ ε ;
    (cls (suc (suc ()))) ;
    Object → ε };
  Σ-Object = refl }

open import MJ.Classtable.Code Σ
open import MJ.Syntax Σ
open import MJ.Syntax.Program Σ

-- Integer class body
IntegerImpl : Implementation INT
IntegerImpl = implementation
    (body (body
      (set
        (var (here refl))
        "x"
        (var (there (here refl))) ◅ ε)
      unit))

    -- methods
    (
      -- get
      body (body ε (get (var (here refl)) "x"))

      -- set
      ∷ (body (body
          (set
            (var (here refl))
            "x"
            {int}
            (get (var (there (here refl))) "x") ◅ ε)
          (call (var (here refl)) "get" [])))

      ∷ []
    )

-- Integer+ class body
Integer+Impl : Implementation INT+
Integer+Impl = implementation
    (body (body
      (
        set (var (here refl)) "x" (var (there (here refl)))
        ◅ ε)
      unit))

    -- methods
    (
      -- override get
      (body (body ε (iop (λ l r → l + r) (get (var (here refl)) "x") (num 1))))

      -- set
      ∷ (super _ ⟨ new INT (iop (λ l r → l + r) (get (var (there (here refl))) "x") (num 1) ∷ []) ∷ [] ⟩then
        body
          ε
          (var (here refl)))

      ∷ []
    )

-- Implementation of the class table
Lib : Code
Lib (cls zero) = IntegerImpl
Lib (cls (suc zero)) = Integer+Impl
Lib (cls (suc (suc ())))
Lib Object = implementation (body (body ε unit)) []

open import MJ.Semantics Σ Lib
open import MJ.Semantics.Values Σ

-- a simple program
p₀ : Prog int
p₀ = Lib ,
  let
    x = (here refl)
    y = (there (here refl))
  in body
    (
        loc (ref INT) -- y
      ◅ loc (ref INT+) -- x
      ◅ asgn x (new INT+ ((num 0) ∷ []))
      ◅ asgn y (new INT ((num 18) ∷ []))
      ◅ ε
    )
    (call (var x) "set" (var y ∷ []))

test0 : p₀ ⇓⟨ 100 ⟩ (λ {W} (v : Val W int) → v ≡ num 20)
test0 = refl


text:
-- Andreas, 2017-09-09
-- Don't allow pattern synonyms where builtin constructor is expected

data Bool : Set where
  true  : Bool
  false : Bool

pattern You = false

{-# BUILTIN BOOL  Bool #-}
{-# BUILTIN TRUE  true #-}
{-# BUILTIN FALSE You  #-}  -- This should be rejected.

-- Expected error: ;-)
-- You must be a constructor in the binding to builtin FALSE
-- when checking the pragma BUILTIN FALSE You

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda