text:
{-# OPTIONS --no-universe-polymorphism #-}
open import Data.Product hiding (map)
open import Relation.Binary.Core
open import Function
open import Data.List
open import Data.Unit using (⊤)
open import Data.Empty

open import Equivalence

module BagEquality where

infixr 5 _⊕_

data _⊕_ (A B : Set) : Set where
             inj₁ : A → A ⊕ B
             inj₂ : B → A ⊕ B

uninhabited : {A : Set} → (A → ⊥) → A ↔ ⊥
uninhabited pf = record {to = pf;
                         from = ⊥-elim;
                         from-to = λ a → ⊥-elim (pf a);
                         to-from = λ false → ⊥-elim false}

Any : {A : Set} → (A → Set) → List A → Set
Any P []       = ⊥
Any P (x ∷ xs) = P x ⊕ Any P xs

infix 6 _∈_
_∈_ : {A : Set} → A → List A → Set
z ∈ xs = Any (λ y → z ≡ y) xs

infixr 4 _≈_

_≈_ : {A : Set} → List A → List A → Set
xs ≈ ys = ∀ z → z ∈ xs ↔ z ∈ ys

infix 10 _>>=_

_>>=_ : {A B : Set} → List A → (A → List B) → List B
xs >>= f = concat (map f xs)

⊕-left-identity : {A : Set} → ⊥ ⊕ A ↔ A
⊕-left-identity {A} = record { to      = to'        ;
                               from    = inj₂       ;
                               from-to = from-to'   ;
                               to-from = λ a → refl } where
                                    to' : ⊥ ⊕ A → A
                                    to' (inj₁ b) = ⊥-elim b
                                    to' (inj₂ a) = a
                                    from-to' : (s : ⊥ ⊕ A) → inj₂ (to' s) ≡ s
                                    from-to' (inj₁ b) = ⊥-elim b
                                    from-to' (inj₂ a) = refl

⊕-assoc : {A B C : Set} → A ⊕ (B ⊕ C) ↔ (A ⊕ B) ⊕ C
⊕-assoc {A} {B} {C} = record {to      = to'      ;
                              from    = from'    ;
                              from-to = from-to' ;
                              to-from = to-from' } where
                                  to' : A ⊕ (B ⊕ C) → (A ⊕ B) ⊕ C
                                  to' (inj₁ a)        = inj₁ (inj₁ a)
                                  to' (inj₂ (inj₁ b)) = inj₁ (inj₂ b)
                                  to' (inj₂ (inj₂ c)) = inj₂ c
                                  from' : (A ⊕ B) ⊕ C → A ⊕ (B ⊕ C)
                                  from' (inj₁ (inj₁ a)) = inj₁ a
                                  from' (inj₁ (inj₂ b)) = inj₂ (inj₁ b)
                                  from' (inj₂ c)        = inj₂ (inj₂ c)
                                  from-to' : (x : A ⊕ (B ⊕ C)) → from' (to' x) ≡ x
                                  from-to' (inj₁ _)        = refl
                                  from-to' (inj₂ (inj₁ _)) = refl
                                  from-to' (inj₂ (inj₂ _)) = refl
                                  to-from' : (y : (A ⊕ B) ⊕ C) → to' (from' y) ≡ y
                                  to-from' (inj₁ (inj₁ _)) = refl
                                  to-from' (inj₁ (inj₂ _)) = refl
                                  to-from' (inj₂ _)        = refl

⊕-comm : {A B : Set} → A ⊕ B ↔ B ⊕ A
⊕-comm {A} {B} = record {to      = to'      ;
                         from    = from'    ;
                         from-to = from-to' ;
                         to-from = to-from' } where
                               to' : A ⊕ B → B ⊕ A
                               to' (inj₁ a) = inj₂ a
                               to' (inj₂ b) = inj₁ b
                               from' : B ⊕ A → A ⊕ B
                               from' (inj₁ b) = inj₂ b
                               from' (inj₂ a) = inj₁ a
                               from-to' : (x : A ⊕ B) → from' (to' x) ≡ x
                               from-to' (inj₁ _) = refl
                               from-to' (inj₂ _) = refl
                               to-from' : (x : B ⊕ A) → to' (from' x) ≡ x
                               to-from' (inj₁ _) = refl
                               to-from' (inj₂ _) = refl

⊕-cong : {A₁ A₂ B₁ B₂ : Set} → A₁ ↔ A₂ → B₁ ↔ B₂ → A₁ ⊕ B₁ ↔ A₂ ⊕ B₂
⊕-cong {A₁} {A₂} {B₁} {B₂} A↔ B↔ = record { to = to';
                                            from = from';
                                            from-to = from-to';
                                            to-from = to-from' } where
                                               to' :  A₁ ⊕ B₁ → A₂ ⊕ B₂
                                               to' (inj₁ a) = inj₁ (_↔_.to A↔ a)
                                               to' (inj₂ b) = inj₂ (_↔_.to B↔ b)
                                               from' :  A₂ ⊕ B₂ → A₁ ⊕ B₁
                                               from' (inj₁ a) = inj₁ (_↔_.from A↔ a)
                                               from' (inj₂ b) = inj₂ (_↔_.from B↔ b)
                                               from-to' : (x : A₁ ⊕ B₁) → from' (to' x) ≡ x
                                               from-to' (inj₁ a) = _↔_.from-to A↔ a under inj₁
                                               from-to' (inj₂ b) = _↔_.from-to B↔ b under inj₂
                                               to-from' : (x : A₂ ⊕ B₂) → to' (from' x) ≡ x
                                               to-from' (inj₁ a) = _↔_.to-from A↔ a under inj₁
                                               to-from' (inj₂ b) = _↔_.to-from B↔ b under inj₂

×-cong : {A₁ A₂ B₁ B₂ : Set} → A₁ ↔ A₂ → B₁ ↔ B₂ → (A₁ × B₁) ↔ (A₂ × B₂)
×-cong {A₁} {A₂} {B₁} {B₂} A↔ B↔ = record { to      = to';
                                            from    = from';
                                            from-to = from-to';
                                            to-from = to-from' } where
                                               to'    :  A₁ × B₁ → A₂ × B₂
                                               to'   (a , b) = (_↔_.to A↔ a , _↔_.to B↔ b)
                                               from'  :  A₂ × B₂ → A₁ × B₁
                                               from' (a , b) = (_↔_.from A↔ a , _↔_.from B↔ b)
                                               pairEq : {A B : Set} {x y : A} {u v : B} → x ≡ y → u ≡ v → (x , u) ≡ (y , v)
                                               pairEq refl refl = refl
                                               from-to' : (x : A₁ × B₁) → from' (to' x) ≡ x
                                               from-to' (a , b) = pairEq (_↔_.from-to A↔ a) (_↔_.from-to B↔ b)
                                               to-from' : (y : A₂ × B₂) → to' (from' y) ≡ y
                                               to-from' (a , b) = pairEq (_↔_.to-from A↔ a) (_↔_.to-from B↔ b)

Any-++ : {A : Set} (P : A → Set) (xs ys : List A) → Any P (xs ++ ys) ↔ Any P xs ⊕ Any P ys

Any-++ P [] ys       = Any P ys ↔⟨ ↔sym ⊕-left-identity ⟩
                       ⊥ ⊕ Any P ys □↔

Any-++ P (x ∷ xs) ys = P x ⊕ Any P (xs ++ ys)        ↔⟨ ⊕-cong (P x □↔) (Any-++ P xs ys) ⟩
                       P x ⊕ (Any P xs ⊕ Any P ys)   ↔⟨ ⊕-assoc ⟩
                       (P x ⊕ Any P xs) ⊕ Any P ys   □↔

-- ++-assoc : {A : Set} (xs ys zs : List A) → ((xs ++ ys) ++ zs) ≡ (xs ++ (ys ++ zs))

++-comm : {A : Set} (xs ys : List A) → xs ++ ys ≈ ys ++ xs
++-comm xs ys z = z ∈ (xs ++ ys)      ↔⟨ Any-++ (z ≡_ )  xs ys ⟩
                  z ∈ xs ⊕ z ∈ ys     ↔⟨ ⊕-comm ⟩
                  z ∈ ys ⊕ z ∈ xs     ↔⟨ ↔sym (Any-++ (z ≡_ ) ys xs ) ⟩
                  z ∈ (ys ++ xs)      □↔

Any-concat : {A : Set} (P : A → Set) → (xss : List (List A)) → Any P (concat xss) ↔ Any (Any P) xss
Any-concat P []         = ⊥ □↔
Any-concat P (xs ∷ xss) = Any P (xs ++ concat xss)         ↔⟨ Any-++ P xs (concat xss) ⟩
                          Any P xs ⊕ Any P (concat xss)    ↔⟨ ⊕-cong (Any P xs □↔) (Any-concat P xss) ⟩
                          Any P xs ⊕ Any (Any P) xss       □↔

Any-map : {A B : Set} (P : B → Set) → (f : A → B) → (xs : List A) → Any P (map f xs) ↔ Any (P ∘ f) xs
Any-map P f []       = ⊥ □↔
Any-map P f (x ∷ xs) = P (f x) ⊕ Any P (map f xs) ↔⟨ ⊕-cong (P (f x) □↔) (Any-map P f xs) ⟩
                      (P ∘ f) x ⊕ Any (P ∘ f) xs □↔

Any->>= : {A B : Set} (P : B → Set) → (xs : List A) → (f : A → List B) → Any P (xs >>= f) ↔ Any (Any P ∘ f) xs
Any->>= P xs f = Any P (concat (map f xs))  ↔⟨ Any-concat P (map f xs) ⟩
                 Any (Any P) (map f xs)     ↔⟨ Any-map (Any P) f xs ⟩
                 Any (Any P ∘ f) xs         □↔

Any-∈ : {A : Set} {P : A → Set} {xs : List A} → Any P xs ↔ (∃ λ z → P z × z ∈ xs)
Any-∈ {A} {P} {[]}     = ⊥ ↔⟨ (↔sym ∘ uninhabited) (⊥-elim ∘ proj₂ ∘ proj₂) ⟩
                         (∃ λ z → P z × z ∈ []) □↔
Any-∈ {A} {P} {x ∷ xs} = record {to      = to'      ;
                                   from    = from'    ;
                                   from-to = from-to' ;
                                   to-from = to-from' } where
                                    to' : P x ⊕ Any P xs → ∃ (λ z → P z × z ∈ (x ∷ xs))
                                    to' (inj₁ px)  = x , (px , (inj₁ refl))
                                    to' (inj₂ any) = (proj₁ recEx) , ( (proj₁ ∘ proj₂) recEx , (inj₂ (proj₂ (proj₂ recEx))) ) where
                                           recEx = _↔_.to Any-∈ any
                                    from' : ∃ (λ z → P z × z ∈ (x ∷ xs)) → P x ⊕ Any P xs
                                    from' ex = from'' (proj₁ ex) (proj₁ (proj₂ ex)) (proj₂ (proj₂ ex)) where
                                           from'' : (z : A) → P z → z ∈ (x ∷ xs) → P x ⊕ Any P xs
                                           from'' .x px (inj₁ refl) = inj₁ px
                                           from''  z pz (inj₂ z∈xs) = inj₂ recAny where
                                                recAny = _↔_.from (Any-∈ {P = P}) (z , (pz , z∈xs))
                                    from-to' : (pf : P x ⊕ Any P xs) → from' (to' pf) ≡ pf
                                    from-to' (inj₁ px)  = refl
                                    from-to' (inj₂ any) = _↔_.from-to Any-∈ any under inj₂
                                    to-from' : (ex : ∃ (λ z → P z × z ∈ (x ∷ xs))) → to' (from' ex) ≡ ex
                                    to-from' ex = to-from'' (proj₁ ex) (proj₁ (proj₂ ex)) (proj₂ (proj₂ ex)) where
                                              to-from'' : (z : A) → (pz : P z) → (z∈xxs : z ∈ (x ∷ xs)) →
                                                             to' (from' ( z , ( pz , z∈xxs ))) ≡ ( z , ( pz , z∈xxs ))
                                              to-from'' .x px (inj₁ refl) = refl
                                              to-from''  z pz (inj₂ z∈xs) = _↔_.to-from (Any-∈ {P = P}) (z , ( pz , z∈xs ) )
                                                   under (λ ex → ((proj₁ ex) , ( (proj₁ ∘ proj₂) ex , (inj₂ (proj₂ (proj₂ ex))))))

∃-cong : {A : Set} {P Q : A → Set} → (∀ x → P x ↔ Q x) → (∃ λ x → P x) ↔ (∃ λ x → Q x)
∃-cong p = record {to     = λ ex → proj₁ ex ,  _↔_.to (p (proj₁ ex)) (proj₂ ex);
                   from    = λ ex → proj₁ ex ,  _↔_.from (p (proj₁ ex)) (proj₂ ex);
                   from-to = λ ex → _↔_.from-to (p (proj₁ ex)) (proj₂ ex) under λ pf → (proj₁ ex) , pf;
                   to-from = λ ex → _↔_.to-from (p (proj₁ ex)) (proj₂ ex) under λ pf → (proj₁ ex) , pf }

Any-cong : {A : Set} (P Q : A → Set) → (xs ys : List A) → (∀ x → P x ↔ Q x) → xs ≈ ys → Any P xs ↔ Any Q ys
Any-cong P Q xs ys p eq = Any P xs                   ↔⟨ Any-∈ ⟩
                          (∃ λ z → P z × z ∈ xs)  ↔⟨ ∃-cong (λ x → ×-cong (p x) (eq x)) ⟩
                          (∃ λ z → Q z × z ∈ ys)  ↔⟨ ↔sym Any-∈ ⟩
                          Any Q ys                  □↔

All-cong : {A : Set} {P Q : A → Set} → {xs ys : List A} → (∀ x → P x ↔ Q x) → xs ≈ ys →
                                                   (∀ x → x ∈ xs → P x) ⇔ (∀ y → y ∈ ys → Q y)
All-cong {P} {Q} {xs} {ys} p eq = record {to = λ P∀x y y∈ys → _↔_.to (p y) (P∀x y (_↔_.from (eq y) y∈ys));
                                          from = λ Q∀y x x∈xs → _↔_.from (p x) (Q∀y x (_↔_.to (eq x) x∈xs))}

max_stars_repo_name: NAMEhzj/Divide-and-Conquer-in-Agda

max_issues_repo_name: NAMEhzj/Divide-and-Conquer-in-Agda

max_forks_repo_name: NAMEhzj/Divide-and-Conquer-in-Agda


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

module lib.groupoids.Groupoids where

open import lib.groupoids.FundamentalPreGroupoid public

ext: agda

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Luau.Syntax where

open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Bool using (Bool; true; false)
open import Agda.Builtin.Float using (Float)
open import Agda.Builtin.String using (String)
open import Luau.Var using (Var)
open import Luau.Addr using (Addr)
open import Luau.Type using (Type)
open import FFI.Data.Maybe using (Maybe; just; nothing)

infixr 5 _∙_

data Annotated : Set where
  maybe : Annotated
  yes : Annotated

data VarDec : Annotated → Set where
  var : Var → VarDec maybe
  var_∈_ : ∀ {a} → Var → Type → VarDec a

name : ∀ {a} → VarDec a → Var
name (var x) = x
name (var x ∈ T) = x

data FunDec : Annotated → Set where
  _⟨_⟩∈_ : ∀ {a} → Var → VarDec a → Type → FunDec a
  _⟨_⟩ : Var → VarDec maybe → FunDec maybe

fun : ∀ {a} → FunDec a → VarDec a
fun (f ⟨ x ⟩∈ T) = (var f ∈ T)
fun (f ⟨ x ⟩) = (var f)

arg : ∀ {a} → FunDec a → VarDec a
arg (f ⟨ x ⟩∈ T) = x
arg (f ⟨ x ⟩) = x

data BinaryOperator : Set where
  + : BinaryOperator
  - : BinaryOperator
  * : BinaryOperator
  / : BinaryOperator
  < : BinaryOperator
  > : BinaryOperator
  == : BinaryOperator
  ~= : BinaryOperator
  <= : BinaryOperator
  >= : BinaryOperator
  ·· : BinaryOperator

data Value : Set where
  nil : Value
  addr : Addr → Value
  number : Float → Value
  bool : Bool → Value
  string : String → Value

data Block (a : Annotated) : Set
data Stat (a : Annotated) : Set
data Expr (a : Annotated) : Set

data Block a where
  _∙_ : Stat a → Block a → Block a
  done : Block a

data Stat a where
  function_is_end : FunDec a → Block a → Stat a
  local_←_ : VarDec a → Expr a → Stat a
  return : Expr a → Stat a

data Expr a where
  var : Var → Expr a
  val : Value → Expr a
  _$_ : Expr a → Expr a → Expr a
  function_is_end : FunDec a → Block a → Expr a
  block_is_end : VarDec a → Block a → Expr a
  binexp : Expr a → BinaryOperator → Expr a → Expr a

isAnnotatedᴱ : ∀ {a} → Expr a → Maybe (Expr yes)
isAnnotatedᴮ : ∀ {a} → Block a → Maybe (Block yes)

isAnnotatedᴱ (var x) = just (var x)
isAnnotatedᴱ (val v) = just (val v)
isAnnotatedᴱ (M $ N) with isAnnotatedᴱ M | isAnnotatedᴱ N
isAnnotatedᴱ (M $ N) | just M′ | just N′ = just (M′ $ N′)
isAnnotatedᴱ (M $ N) | _ | _ = nothing
isAnnotatedᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) with isAnnotatedᴮ B
isAnnotatedᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) | just B′ = just (function f ⟨ var x ∈ T ⟩∈ U is B′ end)
isAnnotatedᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) | _ = nothing
isAnnotatedᴱ (function _ is B end) = nothing
isAnnotatedᴱ (block var b ∈ T is B end) with isAnnotatedᴮ B
isAnnotatedᴱ (block var b ∈ T is B end) | just B′ = just (block var b ∈ T is B′ end)
isAnnotatedᴱ (block var b ∈ T is B end) | _ = nothing
isAnnotatedᴱ (block _ is B end) = nothing
isAnnotatedᴱ (binexp M op N) with isAnnotatedᴱ M | isAnnotatedᴱ N
isAnnotatedᴱ (binexp M op N) | just M′ | just N′ = just (binexp M′ op N′)
isAnnotatedᴱ (binexp M op N) | _ | _ = nothing

isAnnotatedᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) with isAnnotatedᴮ B | isAnnotatedᴮ C
isAnnotatedᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) | just B′ | just C′ = just (function f ⟨ var x ∈ T ⟩∈ U is C′ end ∙ B′)
isAnnotatedᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) | _ | _ = nothing
isAnnotatedᴮ (function _ is C end ∙ B) = nothing
isAnnotatedᴮ (local var x ∈ T ← M ∙ B) with isAnnotatedᴱ M | isAnnotatedᴮ B
isAnnotatedᴮ (local var x ∈ T ← M ∙ B) | just M′ | just B′ = just (local var x ∈ T ← M′ ∙ B′)
isAnnotatedᴮ (local var x ∈ T ← M ∙ B) | _ | _ = nothing
isAnnotatedᴮ (local _ ← M ∙ B) = nothing
isAnnotatedᴮ (return M ∙ B) with isAnnotatedᴱ M | isAnnotatedᴮ B
isAnnotatedᴮ (return M ∙ B) | just M′ | just B′ = just (return M′ ∙ B′)
isAnnotatedᴮ (return M ∙ B) | _ | _ = nothing
isAnnotatedᴮ done = just done

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
------------------------------------------------------------------------------
-- All the common modules
------------------------------------------------------------------------------

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

module Common.Everything where

open import Common.DefinitionsATP
open import Common.DefinitionsI

open import Common.FOL.FOL
open import Common.FOL.FOL-Eq
open import Common.FOL.Relation.Binary.EqReasoning
open import Common.FOL.Relation.Binary.PropositionalEquality

open import Common.Relation.Binary.PreorderReasoning
open import Common.Relation.Unary

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Structure.Category.Monoidal where

import      Lvl
open import Data.Tuple as Tuple using (_,_ ; _⨯_)
open import Data.Tuple.Category
open import Data.Tuple.Equivalence
import      Functional as Fn
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Category
open import Structure.Category.Functor
import      Structure.Category.Functor.Functors as Functors
open import Structure.Category.NaturalTransformation
open import Syntax.Function
open import Type

private variable ℓ ℓₒ ℓₘ ℓₑ ℓₒ₁ ℓₘ₁ ℓₑ₁ ℓₒ₂ ℓₘ₂ ℓₑ₂ : Lvl.Level
private variable Obj : Type{ℓ}
private variable Morphism : Obj → Obj → Type{ℓ}

open Functors.Wrapped

module _
  {C : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}}
  (product@([∃]-intro _) : (C ⨯ᶜᵃᵗ C) →ᶠᵘⁿᶜᵗᵒʳ C)
  (𝟏 : CategoryObject.Object(C))
  where

  open CategoryObject(C)
  open Category.ArrowNotation(category)
  open Category(category)
  open Functor

  record MonoidalCategory : Type{Lvl.of(Type.of C)} where
    constructor intro

    field
      associator : (((product ∘ᶠᵘⁿᶜᵗᵒʳ (Tupleᶜᵃᵗ.mapLeft product))) ∘ᶠᵘⁿᶜᵗᵒʳ Tupleᶜᵃᵗ.associateLeft) ↔ᴺᵀ (product ∘ᶠᵘⁿᶜᵗᵒʳ (Tupleᶜᵃᵗ.mapRight product))
      unitorₗ : (product ∘ᶠᵘⁿᶜᵗᵒʳ Tupleᶜᵃᵗ.constₗ 𝟏) ↔ᴺᵀ idᶠᵘⁿᶜᵗᵒʳ
      unitorᵣ : (product ∘ᶠᵘⁿᶜᵗᵒʳ Tupleᶜᵃᵗ.constᵣ 𝟏) ↔ᴺᵀ idᶠᵘⁿᶜᵗᵒʳ

    _⊗_ : Object → Object → Object
    _⊗_ = Tuple.curry([∃]-witness product)

    _<⊗>_ : ∀{x₁ x₂ y₁ y₂} → (x₁ ⟶ x₂) → (y₁ ⟶ y₂) → ((x₁ ⊗ y₁) ⟶ (x₂ ⊗ y₂))
    _<⊗>_ = Tuple.curry(map([∃]-proof product))

    α : ∀(x)(y)(z) → (((x ⊗ y) ⊗ z) ⟶ (x ⊗ (y ⊗ z)))
    α x y z = [∃]-witness associator (x , (y , z))

    υₗ : ∀(x) → ((𝟏 ⊗ x) ⟶ x)
    υₗ = [∃]-witness unitorₗ

    υᵣ : ∀(x) → ((x ⊗ 𝟏) ⟶ x)
    υᵣ = [∃]-witness unitorᵣ

    α⁻¹ : ∀(x)(y)(z) → ((x ⊗ (y ⊗ z)) ⟶ ((x ⊗ y) ⊗ z))
    α⁻¹ x y z = [∃]-witness (invᴺᵀ associator) (x , (y , z))

    υₗ⁻¹ : ∀(x) → (x ⟶ (𝟏 ⊗ x))
    υₗ⁻¹ = [∃]-witness (invᴺᵀ unitorₗ)

    υᵣ⁻¹ : ∀(x) → (x ⟶ (x ⊗ 𝟏))
    υᵣ⁻¹ = [∃]-witness (invᴺᵀ unitorᵣ)

    α-natural : ∀{(x₁ , (x₂ , x₃)) (y₁ , (y₂ , y₃)) : Object ⨯ (Object ⨯ Object)}
                 {(f₁ , f₂ , f₃) : ((x₁ ⟶ y₁) ⨯ ((x₂ ⟶ y₂) ⨯ (x₃ ⟶ y₃)))} →
                 ((α y₁ y₂ y₃) ∘ ((f₁ <⊗> f₂) <⊗> f₃) ≡ (f₁ <⊗> (f₂ <⊗> f₃)) ∘ (α x₁ x₂ x₃))
    α-natural = NaturalTransformation.natural(NaturalIsomorphism.naturalTransformation([∃]-proof associator))

    υₗ-natural : ∀{x y}{f : x ⟶ y} → (υₗ(y) ∘ (id <⊗> f) ≡ f ∘ υₗ(x))
    υₗ-natural = NaturalTransformation.natural(NaturalIsomorphism.naturalTransformation([∃]-proof unitorₗ))

    υᵣ-natural : ∀{x y}{f : x ⟶ y} → (υᵣ(y) ∘ (f <⊗> id) ≡ f ∘ υᵣ(x))
    υᵣ-natural = NaturalTransformation.natural(NaturalIsomorphism.naturalTransformation([∃]-proof unitorᵣ))

    α⁻¹-natural : ∀{((x₁ , x₂) , x₃) ((y₁ , y₂) , y₃) : (Object ⨯ Object) ⨯ Object}
                   {(f₁ , f₂ , f₃) : ((x₁ ⟶ y₁) ⨯ ((x₂ ⟶ y₂) ⨯ (x₃ ⟶ y₃)))} →
                   ((α⁻¹ y₁ y₂ y₃) ∘ (f₁ <⊗> (f₂ <⊗> f₃)) ≡ ((f₁ <⊗> f₂) <⊗> f₃) ∘ (α⁻¹ x₁ x₂ x₃))
    α⁻¹-natural = NaturalTransformation.natural(NaturalIsomorphism.naturalTransformation([∃]-proof (invᴺᵀ associator)))

    υₗ⁻¹-natural : ∀{x y}{f : x ⟶ y} → (υₗ⁻¹(y) ∘ f ≡ (id <⊗> f) ∘ υₗ⁻¹(x))
    υₗ⁻¹-natural = NaturalTransformation.natural(NaturalIsomorphism.naturalTransformation([∃]-proof (invᴺᵀ unitorₗ)))

    υᵣ⁻¹-natural : ∀{x y}{f : x ⟶ y} → (υᵣ⁻¹(y) ∘ f ≡ (f <⊗> id) ∘ υᵣ⁻¹(x))
    υᵣ⁻¹-natural = NaturalTransformation.natural(NaturalIsomorphism.naturalTransformation([∃]-proof (invᴺᵀ unitorᵣ)))

    -- TODO: And the coherence conditions?

record Monoidalᶜᵃᵗ{ℓₒ}{ℓₘ}{ℓₑ} (C : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}) : Type{Lvl.𝐒(ℓₒ Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ)} where
  constructor intro
  field
    productFunctor : (C ⨯ᶜᵃᵗ C) →ᶠᵘⁿᶜᵗᵒʳ C
    unitObject : CategoryObject.Object(C)
    ⦃ monoidalCategory ⦄ : MonoidalCategory(productFunctor)(unitObject)

module _
  {C₁ : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}} ⦃ (intro product₁ 𝟏₁) : Monoidalᶜᵃᵗ(C₁) ⦄
  {C₂ : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}} ⦃ (intro product₂ 𝟏₂) : Monoidalᶜᵃᵗ(C₂) ⦄
  (functor@([∃]-intro F) : (C₁ →ᶠᵘⁿᶜᵗᵒʳ C₂))
  where

  instance _ = C₁
  instance _ = C₂

  open CategoryObject ⦃ … ⦄
  open Category ⦃ … ⦄
  open Category.ArrowNotation ⦃ … ⦄
  open Functor ⦃ … ⦄
  open MonoidalCategory ⦃ … ⦄

  -- Also called: Lax monoidal functor, applicative functor, idiom.
  record MonoidalFunctor : Type{Lvl.of(Type.of C₁)} where
    constructor intro
    field
      ε : 𝟏₂ ⟶ F(𝟏₁)
      Μ : (product₂ ∘ᶠᵘⁿᶜᵗᵒʳ Tupleᶜᵃᵗ.map functor functor) →ᴺᵀ (functor ∘ᶠᵘⁿᶜᵗᵒʳ product₁)

    μ : ∀{x y} → ((F(x) ⊗ F(y)) ⟶ F(x ⊗ y))
    μ{x}{y} = [∃]-witness Μ (x , y)

    μ-natural : ∀{(x₁ , x₂) (y₁ , y₂) : Object ⦃ C₁ ⦄ ⨯ Object ⦃ C₁ ⦄}
                 {(f₁ , f₂) : ((x₁ ⟶ y₁) ⨯ (x₂ ⟶ y₂))} →
                 (μ ∘ (map(f₁) <⊗> map(f₂)) ≡ map(f₁ <⊗> f₂) ∘ μ)
    μ-natural = NaturalTransformation.natural([∃]-proof Μ)

    -- TODO: Coherence conditions

module _
  {C : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}} ⦃ (intro product 𝟏) : Monoidalᶜᵃᵗ(C) ⦄
  (functor@([∃]-intro F) : (⟲ᶠᵘⁿᶜᵗᵒʳ C))
  where

  instance _ = C

  open CategoryObject ⦃ … ⦄
  open Category ⦃ … ⦄
  open Category.ArrowNotation ⦃ … ⦄
  open Functor ⦃ … ⦄
  open MonoidalCategory ⦃ … ⦄

  record TensorialStrength : Type{Lvl.of(Type.of C)} where
    constructor intro
    field
      Β : (product ∘ᶠᵘⁿᶜᵗᵒʳ Tupleᶜᵃᵗ.mapRight functor) →ᴺᵀ (functor ∘ᶠᵘⁿᶜᵗᵒʳ product)

    β : ∀{x y} → ((x ⊗ F(y)) ⟶ F(x ⊗ y))
    β{x}{y} = [∃]-witness Β (x , y)

    β-natural : ∀{(x₁ , x₂) (y₁ , y₂) : Object ⦃ C ⦄ ⨯ Object ⦃ C ⦄}
                 {(f₁ , f₂) : ((x₁ ⟶ y₁) ⨯ (x₂ ⟶ y₂))} →
                 (β ∘ (f₁ <⊗> map(f₂)) ≡ map(f₁ <⊗> f₂) ∘ β)
    β-natural = NaturalTransformation.natural([∃]-proof Β)

  module TensorialStrengthenedMonoidalEndofunctor ⦃ monoidal : MonoidalFunctor(functor) ⦄ ⦃ strength : TensorialStrength ⦄ where
    open MonoidalFunctor(monoidal)
    open TensorialStrength(strength)

    Ι : idᶠᵘⁿᶜᵗᵒʳ →ᴺᵀ functor
    ∃.witness Ι x = {!!} ∘ μ{x}{𝟏} ∘ {!!}
    ∃.proof Ι = {!!}

    ι : ∀{x} → (x ⟶ F(x))
    ι{x} = [∃]-witness Ι x

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Adjunction where

open import Level

open import Relation.Binary using (Rel; IsEquivalence)
open import Data.Sum
open import Data.Product
open import Function using (flip)

open import Categories.Category
open import Categories.Functor hiding (equiv; assoc; identityˡ; identityʳ; ∘-resp-≡) renaming (id to idF; _≡_ to _≡F_; _∘_ to _∘F_)
open import Categories.NaturalTransformation hiding (equiv; setoid) renaming (id to idT; _≡_ to _≡T_)
open import Categories.Monad
open import Categories.Support.Equivalence

record Adjunction {o ℓ e} {o₁ ℓ₁ e₁} {C : Category o ℓ e} {D : Category o₁ ℓ₁ e₁} (F : Functor D C) (G : Functor C D) : Set (o ⊔ ℓ ⊔ e ⊔ o₁ ⊔ ℓ₁ ⊔ e₁) where
  field
    unit   : NaturalTransformation idF (G ∘F F)
    counit : NaturalTransformation (F ∘F G) idF

    .zig : idT ≡T (counit ∘ʳ F) ∘₁ (F ∘ˡ unit)
    .zag : idT ≡T (G ∘ˡ counit) ∘₁ (unit ∘ʳ G)

  private module C = Category C
  private module D = Category D

  private module F = Functor F
  private module G = Functor G renaming (F₀ to G₀; F₁ to G₁; F-resp-≡ to G-resp-≡)
  open F hiding (op)
  open G hiding (op)

  private module unit   = NaturalTransformation unit
  private module counit = NaturalTransformation counit

  monad : Monad D
  monad = record
    { F = G ∘F F
    ; η = unit
    ; μ = G ∘ˡ (counit ∘ʳ F)
    ; assoc = assoc′
    ; identityˡ = identityˡ′
    ; identityʳ = identityʳ′
    }
    where

    .assoc′ : ∀ {x}
           → G₁ (counit.η (F₀ x)) D.∘ G₁ (F₁ (G₁ (counit.η (F₀ x)))) D.≡ G₁ (counit.η (F₀ x)) D.∘ G₁ (counit.η (F₀ (G₀ (F₀ x))))
    assoc′ {x} =
        begin
          G₁ (counit.η (F₀ x)) D.∘ G₁ (F₁ (G₁ (counit.η (F₀ x))))
        ↑⟨ G.homomorphism ⟩
          G₁ ((counit.η (F₀ x)) C.∘ (F₁ (G₁ (counit.η (F₀ x)))))
        ↓⟨ G-resp-≡ (NaturalTransformation.commute counit (counit.η (F₀ x))) ⟩
          G₁ (counit.η (F₀ x) C.∘ counit.η (F₀ (G₀ (F₀ x))))
        ↓⟨ G.homomorphism ⟩
          G₁ (counit.η (F₀ x)) D.∘ G₁ (counit.η (F₀ (G₀ (F₀ x))))
        ∎
      where
      open D.HomReasoning

    .identityˡ′ : ∀ {x} → G₁ (counit.η (F₀ x)) D.∘ G₁ (F₁ (unit.η x)) D.≡ D.id
    identityˡ′ {x} =
        begin
          G₁ (counit.η (F₀ x)) D.∘ G₁ (F₁ (unit.η x))
        ↑⟨ G.homomorphism ⟩
          G₁ ((counit.η (F₀ x)) C.∘ (F₁ (unit.η x)))
        ↑⟨ G-resp-≡ zig ⟩
          G₁ C.id
        ↓⟨ G.identity ⟩
          D.id
        ∎
      where
      open D.HomReasoning

    .identityʳ′ : ∀ {x} → G₁ (counit.η (F₀ x)) D.∘ unit.η (G₀ (F₀ x)) D.≡ D.id
    identityʳ′ = D.Equiv.sym zag

  op : Adjunction {C = D.op} {D = C.op} G.op F.op
  op = record { unit = counit.op; counit = unit.op; zig = zag; zag = zig }

infixr 5 _⊣_
_⊣_ = Adjunction

id : ∀ {o ℓ e} {C : Category o ℓ e} → Adjunction (idF {C = C}) (idF {C = C})
id {C = C} = record
   { unit = idT
   ; counit = idT
   ; zig = Equiv.sym C.identityˡ
   ; zag = Equiv.sym C.identityˡ
   }
  where
    module C = Category C
    open C

infix  4 _≡_

_≡_ : ∀ {o ℓ e} {o₁ ℓ₁ e₁} {C : Category o ℓ e} {D : Category o₁ ℓ₁ e₁} {F : Functor D C} {G : Functor C D} →  Rel (F ⊣ G) (o ⊔ e ⊔ o₁ ⊔ e₁)
_≡_ {C = C} {D} {F} {G} X Y = Adjunction.unit X ≡T Adjunction.unit Y ×
                                Adjunction.counit X ≡T Adjunction.counit Y

.equiv : ∀ {o ℓ e} {o₁ ℓ₁ e₁} {C : Category o ℓ e} {D : Category o₁ ℓ₁ e₁} {F : Functor D C} {G : Functor C D} → IsEquivalence (_≡_ {F = F} {G})
equiv {C = C} {D} {F} {G} = record
         { refl = (D.Equiv.refl), (C.Equiv.refl)
         ; sym = λ {T U : F ⊣ G} → sym' {T = T} {U = U}
         ; trans = λ {T U V : F ⊣ G} → trans' {T = T} {U = U} {V = V}
         }
      where
        module C = Category C
        module D = Category D

        sym' : {T U : F ⊣ G} → (H : T ≡ U) → flip _≡_ T U
        sym' {T} {U} (H₁ , H₂) = (λ {x} → D.Equiv.sym H₁) , (λ {x} → C.Equiv.sym H₂)

        trans' : {T U V : F ⊣ G} → T ≡ U → U ≡ V → T ≡ V
        trans' {T} {U} {V} (H₁ , H₂) (H₃ , H₄) = (λ {x} → D.Equiv.trans H₁ H₃) , (C.Equiv.trans H₂ H₄)

setoid : ∀ {o ℓ e} {o₁ ℓ₁ e₁} {C : Category o ℓ e} {D : Category o₁ ℓ₁ e₁} {F : Functor D C} {G : Functor C D}
         → Setoid (o ⊔ ℓ ⊔ e ⊔ o₁ ⊔ ℓ₁ ⊔ e₁) (o ⊔ e ⊔ o₁ ⊔ e₁)
setoid {C = C} {D} {F} {G} = record
       { Carrier = Adjunction F G
       ; _≈_ = _≡_
       ; isEquivalence = equiv {F = F} {G = G}
       }

max_stars_repo_name: p-pavel/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --safe --warning=error --without-K --guardedness #-}

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Setoids.Setoids
open import Rings.Definition
open import Rings.Lemmas
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Groups.Definition
open import Groups.Lemmas
open import Fields.Fields
open import Sets.EquivalenceRelations
open import Sequences
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Semirings.Definition

module Fields.CauchyCompletion.Setoid {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

open Setoid S
open SetoidTotalOrder (TotallyOrderedRing.total order)
open SetoidPartialOrder pOrder
open Equivalence eq
open PartiallyOrderedRing pRing
open Ring R
open Group additiveGroup
open Field F

open import Fields.Lemmas F
open import Fields.CauchyCompletion.Definition order F
open import Fields.CauchyCompletion.Addition order F
open import Rings.Orders.Partial.Lemmas pRing
open import Rings.Orders.Total.Lemmas order
open import Rings.Orders.Total.AbsoluteValue order
open import Rings.InitialRing R
open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order })

isZero : CauchyCompletion → Set (m ⊔ o)
isZero record { elts = elts ; converges = converges } = ∀ ε → 0R < ε → Sg ℕ (λ N → ∀ {m : ℕ} → (N <N m) → (abs (index elts m)) < ε)

private
  transitiveLemma : {a b c e/2 : A} → abs (a + inverse b) < e/2 → abs (b + inverse c) < e/2 → (abs (a + inverse c)) < (e/2 + e/2)
  transitiveLemma {a} {b} {c} {e/2} a-b<e/2 b-c<e/2 with triangleInequality (a + inverse b) (b + inverse c)
  transitiveLemma {a} {b} {c} {e/2} a-b<e/2 b-c<e/2 | inl x = SetoidPartialOrder.<Transitive pOrder (<WellDefined (absWellDefined _ _ (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq +Associative (Equivalence.transitive eq (+WellDefined invLeft (Equivalence.reflexive eq)) identLeft))))) (Equivalence.reflexive eq) x) (ringAddInequalities a-b<e/2 b-c<e/2)
  transitiveLemma {a} {b} {c} {e/2} a-b<e/2 b-c<e/2 | inr x = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (absWellDefined _ _ (Equivalence.symmetric eq ((Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq +Associative (Equivalence.transitive eq (+WellDefined invLeft (Equivalence.reflexive eq)) identLeft))))))) x)) (Equivalence.reflexive eq) (ringAddInequalities a-b<e/2 b-c<e/2)

cauchyCompletionSetoid : Setoid CauchyCompletion
(cauchyCompletionSetoid Setoid.∼ a) b = isZero (a +C (-C b))
Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {x} ε 0<e = 0 , t
  where
    t : {m : ℕ} → (0 <N m) → abs (index (apply _+_ (CauchyCompletion.elts x) (map inverse (CauchyCompletion.elts x))) m) < ε
    t {m} 0<m rewrite indexAndApply (CauchyCompletion.elts x) (map inverse (CauchyCompletion.elts x)) _+_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts x) inverse m) = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (absWellDefined _ _ invRight) (identityOfIndiscernablesRight _∼_ (Equivalence.reflexive eq) absZero))) (Equivalence.reflexive eq) 0<e
Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {x} {y} x=y ε 0<e with x=y ε 0<e
Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {x} {y} x=y ε 0<e | N , pr = N , t
  where
    t : {m : ℕ} → N <N m → abs (index (apply _+_ (CauchyCompletion.elts y) (map inverse (CauchyCompletion.elts x))) m) < ε
    t {m} N<m = <WellDefined (Equivalence.transitive eq (absNegation _) (absWellDefined _ _ (identityOfIndiscernablesRight _∼_ (identityOfIndiscernablesLeft _∼_ (identityOfIndiscernablesLeft _∼_ (Equivalence.transitive eq (inverseDistributes) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.transitive eq (inverseWellDefined additiveGroup (identityOfIndiscernablesLeft _∼_ (Equivalence.reflexive eq) (mapAndIndex _ inverse m))) (invTwice additiveGroup (index (CauchyCompletion.elts y) m))) (identityOfIndiscernablesLeft _∼_ (Equivalence.reflexive eq) (equalityCommutative (mapAndIndex (CauchyCompletion.elts x) inverse m)))))) (equalityCommutative (mapAndApply (CauchyCompletion.elts x) (map inverse (CauchyCompletion.elts y)) _+_ inverse m))) (equalityCommutative (mapAndIndex _ inverse m))) (equalityCommutative (indexAndApply (CauchyCompletion.elts y) (map inverse (CauchyCompletion.elts x)) _+_ {m}))))) (Equivalence.reflexive eq) (pr N<m)
Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {x} {y} {z} x=y y=z ε 0<e with halve charNot2 ε
... | e/2 , prHalf with x=y e/2 (halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prHalf) 0<e))
... | Nx , prX with y=z e/2 (halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prHalf) 0<e))
... | Ny , prY = (Nx +N Ny) , t
  where
    t : {m : ℕ} → (Nx +N Ny <N m) → abs (index (apply _+_ (CauchyCompletion.elts x) (map inverse (CauchyCompletion.elts z))) m) < ε
    t {m} nsPr with prX {m} (le (_<N_.x nsPr +N Ny) (transitivity (applyEquality succ (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring _ Ny Nx)) (applyEquality ( λ i → (_<N_.x nsPr) +N i) (Semiring.commutative ℕSemiring Ny Nx)))) (_<N_.proof nsPr)))
    ... | x-y<e/2 with prY {m} (le (_<N_.x nsPr +N Nx) (transitivity (applyEquality succ (equalityCommutative (Semiring.+Associative ℕSemiring _ Nx Ny))) (_<N_.proof nsPr)))
    ... | y-z<e/2 rewrite indexAndApply (CauchyCompletion.elts x) (map inverse (CauchyCompletion.elts z)) _+_ {m} | indexAndApply (CauchyCompletion.elts x) (map inverse (CauchyCompletion.elts y)) _+_ {m} | indexAndApply (CauchyCompletion.elts y) (map inverse (CauchyCompletion.elts z)) _+_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts z) inverse m) | equalityCommutative (mapAndIndex (CauchyCompletion.elts y) inverse m) = <WellDefined (Equivalence.reflexive eq) prHalf (transitiveLemma x-y<e/2 y-z<e/2)

injectionPreservesSetoid : (a b : A) → (a ∼ b) → Setoid._∼_ cauchyCompletionSetoid (injection a) (injection b)
injectionPreservesSetoid a b a=b ε 0<e = 0 , t
  where
    t : {m : ℕ} → 0 <N m → abs (index (apply _+_ (constSequence a) (map inverse (constSequence b))) m) < ε
    t {m} 0<m = <WellDefined (identityOfIndiscernablesLeft _∼_ (absWellDefined 0G _ (identityOfIndiscernablesRight _∼_ (Equivalence.transitive eq (Equivalence.symmetric eq (transferToRight'' additiveGroup a=b)) (+WellDefined (identityOfIndiscernablesLeft _∼_ (Equivalence.reflexive eq) (indexAndConst a m)) (identityOfIndiscernablesRight _∼_ (Equivalence.reflexive eq) (transitivity (applyEquality inverse (equalityCommutative (indexAndConst _ m))) (mapAndIndex _ inverse m))))) (equalityCommutative (indexAndApply (constSequence a) _ _+_ {m})))) absZero) (Equivalence.reflexive eq) 0<e

infinitesimalImplies0 : (a : A) → ({ε : A} → (0R < ε) → a < ε) → (a ∼ 0R) || (a < 0R)
infinitesimalImplies0 a pr with totality 0R a
infinitesimalImplies0 a pr | inl (inl 0<a) with halve charNot2 a
infinitesimalImplies0 a pr | inl (inl 0<a) | a/2 , prA/2 with pr {a/2} (halvePositive a/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prA/2) 0<a))
... | bl with halvePositive a/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prA/2) 0<a)
... | 0<a/2 = exFalso (irreflexive {a} (<WellDefined identLeft prA/2 (ringAddInequalities 0<a/2 bl)))
infinitesimalImplies0 a pr | inl (inr a<0) = inr a<0
infinitesimalImplies0 a pr | inr 0=a = inl (Equivalence.symmetric eq 0=a)

injectionPreservesSetoid' : (a b : A) → Setoid._∼_ cauchyCompletionSetoid (injection a) (injection b) → a ∼ b
injectionPreservesSetoid' a b a=b = transferToRight additiveGroup (absZeroImpliesZero ans)
  where
    infinitesimal : {ε : A} → 0G < ε → abs (a + inverse b) < ε
    infinitesimal {ε} 0<e with a=b ε 0<e
    ... | N , pr with pr {succ N} (le 0 refl)
    ... | bl rewrite indexAndApply (constSequence a) (map inverse (constSequence b)) _+_ {N} | indexAndConst a N | equalityCommutative (mapAndIndex (constSequence b) inverse N) | indexAndConst b N = bl
    ans : (abs (a + inverse b)) ∼ 0G
    ans with infinitesimalImplies0 _ infinitesimal
    ... | inl x = x
    ... | inr x = exFalso (absNonnegative x)

CInjection : SetoidInjection S cauchyCompletionSetoid injection
SetoidInjection.wellDefined CInjection {x} {y} x=y = injectionPreservesSetoid x y x=y
SetoidInjection.injective CInjection {x} {y} x=y = injectionPreservesSetoid' x y x=y

trivialIfInputTrivial : (0R ∼ 1R) → (a : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid (injection 0R) a
trivialIfInputTrivial 0=1 a ε 0<e = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (oneZeroImpliesAllZero R 0=1) 0<e))


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Functions.Definition
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Order
open import Sets.FinSet.Definition
open import Sets.FinSet.Lemmas
open import Setoids.Setoids
open import Setoids.Cardinality.Infinite.Definition
open import Sets.Cardinality.Infinite.Lemmas
open import Setoids.Subset
open import Sets.EquivalenceRelations

module Setoids.Cardinality.Infinite.Lemmas where

finsetNotInfiniteSetoid : {n : ℕ} → InfiniteSetoid (reflSetoid (FinSet n)) → False
finsetNotInfiniteSetoid {n} isInfinite = isInfinite n id (record { inj = record { wellDefined = id ; injective = id } ; surj = record { wellDefined = id ; surjective = λ {x} → x , refl } })

dedekindInfiniteImpliesInfiniteSetoid : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → DedekindInfiniteSetoid S → InfiniteSetoid S
dedekindInfiniteImpliesInfiniteSetoid S record { inj = inj ; isInjection = isInj } zero f isBij with SetoidInvertible.inverse (setoidBijectiveImpliesInvertible isBij) (inj 0)
... | ()
dedekindInfiniteImpliesInfiniteSetoid {A = A} S record { inj = inj ; isInjection = isInj } (succ n) f isBij = noInjectionNToFinite {f = t} tInjective
  where
    t : ℕ → FinSet (succ n)
    t n = SetoidInvertible.inverse (setoidBijectiveImpliesInvertible isBij) (inj n)
    tInjective : Injection t
    tInjective pr = SetoidInjection.injective isInj (SetoidInjection.injective (SetoidBijection.inj (setoidInvertibleImpliesBijective (inverseInvertible (setoidBijectiveImpliesInvertible isBij)))) pr)


text:
module SystemF.BigStep.Extrinsic.Semantics where

open import Prelude hiding (⊥; id)
open import Function as Fun using ()
open import Data.List hiding ([_]; monad)
open import Data.List.Properties as ListProp using ()
open import Data.Fin.Substitution
open import Extensions.List

open import SystemF.BigStep.Types
open import SystemF.BigStep.Extrinsic.Terms
open import SystemF.BigStep.Extrinsic.Welltyped

-- environments
mutual
  Env : Set
  Env = List Val

  data Val : Set where
    unit : Val
    clos : Env → (t : Term) → Val
    tclos : Env → (t : Term) → Val

open import Relation.Binary.List.Pointwise hiding (refl; map)
mutual

  -- welltypedness relations between typing contexts and environmets
  -- is just the pointwise extension of value-welltypedness
  _⊢_ : ∀ {n} → Ctx n → Env → Set
  Γ ⊢ E = Rel (λ{ a v → ⊢̬ v ∶ a}) Γ E

  data ⊢̬_∶_ {n} : Val → Type n → Set where

    unit : -------------------
          ⊢̬ unit ∶ Unit

    clos : ∀ {b t}{Γ : Ctx n}{E a} →
            (a ∷ Γ) ⊢ t ∶ b →
            Γ ⊢ E →
            -------------------
            ⊢̬ clos E t ∶ (a ⇒ b)

    tclos : ∀ {a t}{Γ : Ctx n}{E} →
            (Γ ctx/ wk) ⊢ t ∶ a →
            Γ ⊢ E →
            ---------------------
            ⊢̬ tclos E t ∶ ∀' a

module UglyBits where

  _wt/_ : ∀ {n m}{Γ : Ctx n}{t a} → Γ ⊢ t ∶ a → (ρ : Sub Type n m) → (Γ ctx/ ρ) ⊢ t ∶ (a / ρ)
  unit wt/ ρ = unit
  ƛ a t wt/ ρ = ƛ (a / ρ) (t wt/ ρ)
  var x wt/ ρ = var ([]=-map x)
  (f · e) wt/ ρ = (f wt/ ρ) · (e wt/ ρ)
  Λ t wt/ ρ = Λ (subst (λ Γ → Γ ⊢ _ ∶ _) (sym $ CtxLemmas.ctx/-wk-comm _ ρ) (t wt/ (ρ ↑)))
  (_[_] {a = a} t b) wt/ ρ =
    subst (λ a → _ ⊢ _ ∶ a) (sym $ Lemmas.sub-commutes a) ((t wt/ ρ) [ (b / ρ) ])

module StepIndexed where

  open UglyBits
  open import Level as Lev using ()
  open import Data.Maybe
  open import Category.Monad
  open RawMonad (monad {f = Lev.zero})

  -- quadratic return through the layered monad
  pattern just² x = just (just x)

  -- substitution-free semantics in double-layered maybe monad;
  -- distinguishing semantic errors from timeouts
  _⊢_⇓_ : ∀ (μ : Env) → Term → ℕ → Maybe (Maybe Val)
  μ ⊢ x ⇓ zero = nothing
  μ ⊢ unit ⇓ (suc n) = just² unit
  μ ⊢ ƛ t ⇓ (suc n) = just² (clos μ t)
  μ ⊢ Λ t ⇓ (suc n) = just² (tclos μ t )
  μ ⊢ f · e ⇓ (suc n) with (μ ⊢ f ⇓ n) | μ ⊢ e ⇓ n
  -- timeout
  ... | nothing | _ = nothing
  ... | _ | nothing = nothing
  -- success
  ... | just² (clos μ' t) | just² v = (v ∷ μ') ⊢ t ⇓ n
  -- semantic errors & semantic error propagation
  ... | _ | _ = just nothing
  μ ⊢ t [-] ⇓ (suc n) with (μ ⊢ t ⇓ n)
  -- timeout
  ... | nothing = nothing
  -- success
  ... | just² (tclos μ' t') = μ' ⊢ t' ⇓ n
  -- semantic error (propagation)
  ... | _ = just nothing
  μ ⊢ var x ⇓ (suc n) = just (maybe-lookup x μ)

  -- extrinsic safety
  _⊢_⇓_ok : ∀ {n}{Γ : Ctx n}{μ : Env}{t a} →
            Γ ⊢ μ → Γ ⊢ t ∶ a → ∀ n → All (Any (λ v → ⊢̬ v ∶ a)) (μ ⊢ t ⇓ n)

  μ ⊢ x ⇓ zero ok = nothing

  μ ⊢ unit ⇓ suc n ok = just² unit

  μ ⊢ ƛ a x ⇓ suc n ok = just² (clos x μ)

  μ ⊢ Λ x ⇓ suc n ok = just² (tclos x μ)

  _⊢_⇓_ok {μ = E} μ (_·_ {f = f}{e = e} wtf wte) (suc n) with
    E ⊢ f ⇓ n | E ⊢ e ⇓ n | μ ⊢ wtf ⇓ n ok | μ ⊢ wte ⇓ n ok
  -- timeout
  ... | nothing | _ | _ | _ = nothing
  ... | just _ | nothing | _ | _ = nothing

  -- success
  ... | just² (clos μ' t) | just² v | just² (clos wtt wtμ') | just² px = (px ∷ wtμ') ⊢ wtt ⇓ n ok

  -- semantic error propagation
  ... | just nothing | _ | (just ()) | _
  ... | _ | just nothing | _ | (just ())

  -- semantic errors
  ... | just² (tclos _ _) | _ | just² () | _
  ... | just² unit | _ | just² () | _

  _⊢_⇓_ok {μ = E} μ (_[_] {f = f} wtf b) (suc n) with E ⊢ f ⇓ n | μ ⊢ wtf ⇓ n ok
  -- timeout
  ... | nothing | _ = nothing
  -- semantic errors
  ... | just nothing | (just ())
  ... | just² unit | just² ()
  ... | just² (clos x t) | just² ()
  -- success
  ... | just² (tclos μ' t) | just² (tclos tok μ'ok) =
    μ'ok ⊢ subst (λ Γ → Γ ⊢ _ ∶ _) (CtxLemmas.ctx/-wk-sub≡id _ b) (tok wt/ (sub b)) ⇓ n ok

  μ ⊢ var x ⇓ suc n ok with pointwise-maybe-lookup μ x
  μ ⊢ var x ⇓ suc n ok | _ , is-just , p rewrite is-just = just² p

module DelayMonad where

  open import Coinduction
  open import Category.Monad.Partiality
  open import Data.Maybe

  module _ where
    open Workaround

    _⊢lookup_ : Env → ℕ → Maybe Val
    [] ⊢lookup n = nothing
    (x ∷ μ) ⊢lookup zero = just x
    (x ∷ μ) ⊢lookup suc n = μ ⊢lookup n

    ret : ∀ {a} {A : Set a} → A → (Maybe A) ⊥P
    ret x = now (just x)

    -- substitution free semantics for SystemF
    _⊢_⇓P : ∀ (μ : Env) → Term → (Maybe Val) ⊥P
    μ ⊢ unit ⇓P = ret unit
    μ ⊢ ƛ t ⇓P = ret (clos μ t)
    μ ⊢ Λ t ⇓P = ret (tclos μ t )
    μ ⊢ f · e ⇓P = μ ⊢ f ⇓P >>= λ{
        (just (clos μ' t)) → μ ⊢ e ⇓P >>= (λ{
          (just v) → later (♯ ((v ∷ μ') ⊢ t ⇓P))
          ; nothing → now nothing
        }) ;
        _ → now nothing
      }
    μ ⊢ t [-] ⇓P = μ ⊢ t ⇓P >>= λ{
        (just (tclos μ' t')) →  later (♯ (μ' ⊢ t' ⇓P)) ;
        _ → now nothing
      }
    μ ⊢ var x ⇓P = now (μ ⊢lookup x)

    _⊢_⇓ : ∀ (μ : Env) → Term → (Maybe Val) ⊥
    μ ⊢ t ⇓ = ⟦ μ ⊢ t ⇓P ⟧P

{-}
  open import Category.Monad.Partiality.All
  open Alternative

  {-}
  module Compositional where
    private
      module Eq = Equality (_≡_)

    open import Level as Level
    open import Category.Monad
    open Eq hiding (_⇓)
    open RawMonad (monad {f = Level.zero})

    _·⇓_ : ∀ (f e : Val ⊥) → Val ⊥
    f ·⇓ e = f >>= λ{ (clos x t) → {!!} ; _ → now error }

    ·-comp : ∀ {μ f e} → (μ ⊢ f · e ⇓) ≅ ((μ ⊢ f ⇓) ·⇓ (μ ⊢ e ⇓))
    ·-comp = {!!}
  -}

  module Safety where

    _⊢_⇓okP : ∀ {n}{Γ : Ctx n}{μ : Env}{t a} → Γ ⊢ μ → Γ ⊢ t ∶ a → AllP (λ v → ⊢̬ v ∶ a) (μ ⊢ t ⇓)
    μ ⊢ unit ⇓okP = now unit
    μ ⊢ ƛ a t₁ ⇓okP = now (clos t₁ μ)
    μ ⊢ var x ⇓okP = now {!!}
    μ ⊢ f · e ⇓okP = {!μ ⊢ f ⇓okP!}
    μ ⊢ Λ t₁ ⇓okP = {!!}
    μ ⊢ t [ b ] ⇓okP = {!!}
-}


text:
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Ordinals
module ODUtil {n : Level } (O : Ordinals {n} ) where

open import zf
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Data.Nat.Properties
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary hiding ( _⇔_ )

open import logic
open import nat

open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
import OrdUtil
open OrdUtil O

import OD
open OD O
open OD.OD
open ODAxiom odAxiom

open HOD
open _⊆_
open _∧_
open _==_

cseq :  HOD  →  HOD
cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
    lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
    lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc )

pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) )
pair-xx<xy {x} {y} = ⊆→o≤  lemma where
   lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z
   lemma {z} (case1 refl) = case1 refl
   lemma {z} (case2 refl) = case1 refl

pair-<xy : {x y : HOD} → {n : Ordinal}  → & x o< next n →  & y o< next n  → & (x , y) o< next n
pair-<xy {x} {y} {o} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y)
... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho<
... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho<
... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho<

--  another form of infinite
-- pair-ord< :  {x : Ordinal } → Set n
pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x)
pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1  where
       lemmab0 : next (odmax (x , x)) ≡ next (& x)
       lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡)
       lemmab1 : & (x , x) o< next ( odmax (x , x))
       lemmab1 = ho<

trans-⊆ :  { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }

refl-⊆ : {A : HOD} → A ⊆ A
refl-⊆ {A} = record { incl = λ x → x }

od⊆→o≤  : {x y : HOD } → x ⊆ y → & x o< osuc (& y)
od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) &iso (incl lt (d→∋ x x>z)))

subset-lemma : {A x : HOD  } → ( {y : HOD } →  x ∋ y → (A ∩ x ) ∋  y ) ⇔  ( x ⊆ A  )
subset-lemma  {A} {x} = record {
      proj1 = λ lt  → record { incl = λ x∋z → proj1 (lt x∋z)  }
    ; proj2 = λ x⊆A lt → ⟪ incl x⊆A lt , lt ⟫
   }

ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
ω<next-o∅ {y} lt = <odmax infinite lt

nat→ω : Nat → HOD
nat→ω Zero = od∅
nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y))

ω→nato : {y : Ordinal} → infinite-d y → Nat
ω→nato iφ = Zero
ω→nato (isuc lt) = Suc (ω→nato lt)

ω→nat : (n : HOD) → infinite ∋ n → Nat
ω→nat n = ω→nato

ω∋nat→ω : {n : Nat} → def (od infinite) (& (nat→ω n))
ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) (sym ord-od∅) iφ
ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) lemma (isuc ( ω∋nat→ω {n})) where
    lemma :  & (Union (* (& (nat→ω n)) , (* (& (nat→ω n)) , * (& (nat→ω n))))) ≡ & (nat→ω (Suc n))
    lemma = subst (λ k → & (Union (k , ( k , k ))) ≡ & (nat→ω (Suc n))) (sym *iso) refl

pair1 : { x y  : HOD  } →  (x , y ) ∋ x
pair1 = case1 refl

pair2 : { x y  : HOD  } →  (x , y ) ∋ y
pair2 = case2 refl

single : {x y : HOD } → (x , x ) ∋ y → x ≡ y
single (case1 eq) = ==→o≡ ( ord→== (sym eq) )
single (case2 eq) = ==→o≡ ( ord→== (sym eq) )

open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
-- postulate f-extensionality : { n m : Level}  → HE.Extensionality n m

ω-prev-eq1 : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → ¬ (x o< y)
ω-prev-eq1 {x} {y} eq x<y = eq→ (ord→== eq) {& (* y)} (λ not2 → not2 (& (* y , * y))
      ⟪ case2 refl , subst (λ k → odef k (& (* y))) (sym *iso) (case1 refl)⟫ ) (λ u → lemma u ) where
   lemma : (u : Ordinal) → ¬ def (od (* x , (* x , * x))) u ∧ def (od (* u)) (& (* y))
   lemma u t with proj1 t
   lemma u t | case1 u=x = o<> (c<→o< {* y} {* u} (proj2 t)) (subst₂ (λ j k → j o< k )
        (trans (sym &iso) (trans (sym u=x) (sym &iso)) ) (sym &iso) x<y ) -- x ≡ & (* u)
   lemma u t | case2 u=xx = o<¬≡ (lemma1 (subst (λ k → odef k (& (* y)) ) (trans (cong (λ k → * k ) u=xx) *iso )  (proj2 t))) x<y where
       lemma1 : {x y : Ordinal } → (* x , * x ) ∋ * y → x ≡ y    --  y = x ∈ ( x , x ) = u
       lemma1 (case1 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq)
       lemma1 (case2 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq)

ω-prev-eq : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → x ≡ y
ω-prev-eq {x} {y} eq with trio< x y
ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a)
ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b
ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c)

ω-∈s : (x : HOD) →  Union ( x , (x , x)) ∋ x
ω-∈s x not = not (& (x , x)) ⟪ case2 refl , subst (λ k → odef k (& x) ) (sym *iso) (case1 refl) ⟫

ωs≠0 : (x : HOD) →  ¬ ( Union ( x , (x , x)) ≡ od∅ )
ωs≠0 y eq =  ⊥-elim ( ¬x<0 (subst (λ k → & y  o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) )

nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
nat→ω-iso {i} = ε-induction {λ i →  (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i  } ind i where
     ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
                                            (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x
     ind {x} prev lt = ind1 lt *iso where
         ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → * ox ≡ x → nat→ω (ω→nato ltd) ≡ x
         ind1 {o∅} iφ refl = sym o∅≡od∅
         ind1 (isuc {x₁} ltd) ox=x = begin
              nat→ω (ω→nato (isuc ltd) )
           ≡⟨⟩
              Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd)))
           ≡⟨ cong (λ k → Union (k , (k , k ))) lemma  ⟩
              Union (* x₁ , (* x₁ , * x₁))
           ≡⟨ trans ( sym *iso) ox=x ⟩
              x
           ∎ where
               open ≡-Reasoning
               lemma0 :  x ∋ * x₁
               lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x) (λ not → not
                  (& (* x₁ , * x₁))  ⟪ pair2 , subst (λ k → odef k (& (* x₁))) (sym *iso) pair1 ⟫ )
               lemma1 : infinite ∋ * x₁
               lemma1 = subst (λ k → odef infinite k) (sym &iso) ltd
               lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
               lemma3 iφ iφ refl = HE.refl
               lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) )))
               lemma3 (isuc {y} ltd)  iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso (sym eq) (c<→o< (ω-∈s (* y)) )))
               lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq))
               ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅  (ω-prev-eq eq)) t
               lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1
               lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq)  where
                   lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1
                   lemma6 refl HE.refl = refl
               lemma :  nat→ω (ω→nato ltd) ≡ * x₁
               lemma = trans  (cong (λ k →  nat→ω  k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym &iso) ltd)  &iso ) ) ( prev {* x₁} lemma0 lemma1 )

ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i
ω→nat-iso {i} = lemma i (ω∋nat→ω {i}) *iso where
   lemma : {x : Ordinal } → ( i : Nat ) → (ltd : infinite-d x ) → * x ≡  nat→ω i → ω→nato ltd ≡ i
   lemma {x} Zero iφ eq = refl
   lemma {x} (Suc i) iφ eq = ⊥-elim ( ωs≠0 (nat→ω i) (trans (sym eq) o∅≡od∅ )) -- Union (nat→ω i , (nat→ω i , nat→ω i)) ≡ od∅
   lemma Zero (isuc {x} ltd) eq = ⊥-elim ( ωs≠0 (* x) (subst (λ k → k ≡ od∅  ) *iso eq ))
   lemma (Suc i) (isuc {x} ltd) eq = cong (λ k → Suc k ) (lemma i ltd (lemma1 eq) )  where -- * x ≡ nat→ω i
           lemma1 :  * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i
           lemma1 eq = subst (λ k → * x ≡ k ) *iso (cong (λ k → * k)
                ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym
                    (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq ))))))

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
{-# OPTIONS --sized-types #-}
module SNat.Order.Properties where

open import Data.Sum renaming (_⊎_ to _∨_)
open import Relation.Binary.PropositionalEquality
open import Size
open import SNat
open import SNat.Order

tot≤ : {ι ι' : Size} → (m : SNat {ι}) → (n : SNat {ι'}) → m ≤ n ∨ n ≤ m
tot≤ zero n = inj₁ (z≤n n)
tot≤ m zero = inj₂ (z≤n m)
tot≤ (succ m) (succ n)
   with tot≤ m n
...| inj₁ m≤n = inj₁ (s≤s m≤n)
...| inj₂ n≤m = inj₂ (s≤s n≤m)

refl≤ : {n : SNat} → n ≤ n
refl≤ {n}
    with tot≤ n n
... | inj₁ n≤n = n≤n
... | inj₂ n≤n = n≤n

trans≤ :  {ι ι' ι'' : Size}{n : SNat {ι}}{n' : SNat {ι'}}{n'' : SNat {ι''}} → n ≤ n' → n' ≤ n'' → n ≤ n''
trans≤ {n'' = n''} (z≤n n') _ = z≤n n''
trans≤ (s≤s n≤n') (s≤s n'≤n'') = s≤s (trans≤ n≤n' n'≤n'')

refl≅ : {n : SNat} → n ≅ n
refl≅ {zero} = z≅z
refl≅ {succ _} = s≅s refl≅

trans≅ :  {ι ι' ι'' : Size}{n : SNat {ι}}{n' : SNat {ι'}}{n'' : SNat {ι''}} → n ≅ n' → n' ≅ n'' → n ≅ n''
trans≅ z≅z z≅z = z≅z
trans≅ (s≅s n≅n') (s≅s n'≅n'') = s≅s (trans≅ n≅n' n'≅n'')

lemma-z≤′n : {ι ι' : Size}(n : SNat {ι}) → zero {ι'} ≤′ n
lemma-z≤′n zero = ≤′-eq z≅z
lemma-z≤′n (succ n) = ≤′-step (lemma-z≤′n n)

lemma-s≤′s : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}} → m ≤′ n → succ m ≤′ succ n
lemma-s≤′s (≤′-eq m≅n) = ≤′-eq (s≅s m≅n)
lemma-s≤′s (≤′-step m≤′n) = ≤′-step (lemma-s≤′s m≤′n)

lemma-≤-≤′ : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}} → m ≤ n → m ≤′ n
lemma-≤-≤′ (z≤n n) = lemma-z≤′n n
lemma-≤-≤′ (s≤s m≤n) = lemma-s≤′s (lemma-≤-≤′ m≤n)

lemma-≅-≤ : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}} → m ≅ n → m ≤ n
lemma-≅-≤ z≅z = z≤n zero
lemma-≅-≤ (s≅s m≅n) = s≤s (lemma-≅-≤ m≅n)

lemma-≡-≤′ : {a b c : SNat} → b ≡ a → a ≤′ c → b ≤′ c
lemma-≡-≤′ b≡a a≤′c rewrite b≡a = a≤′c

lemma-n≤sn : {ι : Size}(n : SNat {ι}) → n ≤ succ n
lemma-n≤sn zero = z≤n (succ zero)
lemma-n≤sn (succ n) = s≤s (lemma-n≤sn n)

lemma-≤′-≤ : {ι ι' : Size}{m : SNat {ι}}{n : SNat {ι'}} → m ≤′ n → m ≤ n
lemma-≤′-≤ (≤′-eq m≅n) = lemma-≅-≤ m≅n
lemma-≤′-≤ (≤′-step {n = n} m≤′n) = trans≤ (lemma-≤′-≤ m≤′n) (lemma-n≤sn n)

refl≤′ : {n : SNat} → n ≤′ n
refl≤′ = lemma-≤-≤′ refl≤

trans≤′ :  {ι ι' ι'' : Size}{n : SNat {ι}}{n' : SNat {ι'}}{n'' : SNat {ι''}} → n ≤′ n' → n' ≤′ n'' → n ≤′ n''
trans≤′ n≤′n' n'≤′n'' = lemma-≤-≤′ (trans≤ (lemma-≤′-≤ n≤′n') (lemma-≤′-≤ n'≤′n''))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
------------------------------------------------------------------------
-- Modules that can (perhaps) not be type-checked in safe mode, and
-- do not use --sized-types
------------------------------------------------------------------------

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

module README.Unsafe where

-- Strings.

import String

-- IO.

import IO-monad

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- Issue #1842, __IMPOSSIBLE__ showed up in debug output

{-# OPTIONS -v interaction.case:65 #-} -- KEEP

data Bool : Set where
  true false : Bool

test : Bool → Bool
test x = {!x!} -- C-c C-c

-- Splitting here with debug output turned on
-- should not crash.

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommMonoid.CommMonoidProd where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma

open import Cubical.Algebra.CommMonoid.Base

open CommMonoidStr

private
  variable
    ℓ ℓ' : Level

CommMonoidProd : CommMonoid ℓ → CommMonoid ℓ' → CommMonoid (ℓ-max ℓ ℓ')
CommMonoidProd M N = makeCommMonoid ε× _·×_ is-set× assoc× ·IdR× comm×
  where
  ε× : (fst M) × (fst N)
  ε× = (ε (snd M)) , (ε (snd N))

  _·×_ : (fst M) × (fst N) → (fst M) × (fst N) → (fst M) × (fst N)
  (x₁ , x₂) ·× (y₁ , y₂) = (_·_ (snd M) x₁ y₁) , (_·_ (snd N) x₂ y₂)

  is-set× : isSet ((fst M) × (fst N))
  is-set× = isSet× (is-set (snd M)) (is-set (snd N))

  assoc× : ∀ x y z → x ·× (y ·× z) ≡ (x ·× y) ·× z
  assoc× _ _ _ = cong₂ (_,_) (·Assoc (snd M) _ _ _) (·Assoc (snd N) _ _ _)

  ·IdR× : ∀ x → x ·× ε× ≡ x
  ·IdR× _ =  cong₂ (_,_) (·IdR (snd M) _) (·IdR (snd N) _)

  comm× : ∀ x y → x ·× y ≡ y ·× x
  comm× _ _ = cong₂ (_,_) (·Comm (snd M) _ _) (·Comm (snd N) _ _)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
open import Common.Prelude

test : List Char → Char
test []         = 'a'
test ('a' ∷ []) = 'b'
-- test (c ∷ cs)   = c

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --rewriting --allow-unsolved-metas #-}

open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Equality.Rewrite

postulate
  cast : (A B : Set) → A → B
  cast-rew : (A : Set) (x : A) → cast A A x ≡ x
{-# REWRITE cast-rew #-}

postulate
  A : Set
  x y : A

data D (B : A → Set) (b : B y) : Set where
  con : cast (B x) (B y) ? ≡ b → D B b

record R (B : A → Set) (b : B y) : Set where
  field
    eq : cast (B x) (B y) ? ≡ b


text:
module ShowNat where

open import IO
open import Data.Unit
open import Data.Nat.Show

main = run (putStrLn (Data.Nat.Show.show 10))

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module nat where

open import product
open import bool
open import maybe
open import eq

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

nat = ℕ

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infixl 10 _*_
infixl 9 _+_ _∸_
infixl 8 _<_ _=ℕ_ _≤_ _>_ _≥_

-- pragmas to get decimal notation:

{-# BUILTIN NATURAL ℕ #-}

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------

---------------------------------------
-- basic arithmetic operations
---------------------------------------

_+_ : ℕ → ℕ → ℕ
zero  + n = n
suc m + n = suc (m + n)

{-# BUILTIN NATPLUS _+_ #-}

_*_ : ℕ → ℕ → ℕ
zero  * n = zero
suc m * n = n + (m * n)

{-# BUILTIN NATTIMES _*_ #-}

pred : ℕ → ℕ
pred 0 = 0
pred (suc n) = n

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero  = m
zero  ∸ suc n = zero
suc m ∸ suc n = m ∸ n

-- see nat-division.agda for division function

{-# BUILTIN NATMINUS _∸_ #-}

square : ℕ → ℕ
square x = x * x

--------------------------------------------------
-- comparisons
--------------------------------------------------

_<_ : ℕ → ℕ → 𝔹
0 < 0 = ff
0 < (suc y) = tt
(suc x) < (suc y) = x < y
(suc x) < 0 = ff

_=ℕ_ : ℕ → ℕ → 𝔹
0 =ℕ 0 = tt
suc x =ℕ suc y = x =ℕ y
_ =ℕ _ = ff

_≤_ : ℕ → ℕ → 𝔹
x ≤ y = (x < y) || x =ℕ y

_>_ : ℕ → ℕ → 𝔹
a > b = b < a

_≥_ : ℕ → ℕ → 𝔹
a ≥ b = b ≤ a

min : ℕ → ℕ → ℕ
min x y = if x < y then x else y

max : ℕ → ℕ → ℕ
max x y = if x < y then y else x

data compare-t : Set where
  compare-lt : compare-t
  compare-eq : compare-t
  compare-gt : compare-t

compare : ℕ → ℕ → compare-t
compare 0 0 = compare-eq
compare 0 (suc y) = compare-lt
compare (suc x) 0 = compare-gt
compare (suc x) (suc y) = compare x y

iszero : ℕ → 𝔹
iszero 0 = tt
iszero _ = ff

parity : ℕ → 𝔹
parity 0 = ff
parity (suc x) = ~ (parity x)

_pow_ : ℕ → ℕ → ℕ
x pow 0 = 1
x pow (suc y) = x * (x pow y)

factorial : ℕ → ℕ
factorial 0 = 1
factorial (suc x) = (suc x) * (factorial x)

is-even : ℕ → 𝔹
is-odd : ℕ → 𝔹
is-even 0 = tt
is-even (suc x) = is-odd x
is-odd 0 = ff
is-odd (suc x) = is-even x

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
module ctxt where

open import cedille-types
open import ctxt-types public
open import subst
open import general-util
open import syntax-util
open import type-util
open import free-vars

new-sym-info-trie : trie sym-info
new-sym-info-trie = trie-insert empty-trie compileFail-qual ((term-decl compileFailType) , "missing" , "missing")

new-qualif : qualif
new-qualif = trie-insert empty-trie compileFail (compileFail-qual , [])

qualif-nonempty : qualif → 𝔹
qualif-nonempty q = trie-nonempty (trie-remove q compileFail)

qualif-insert-params : qualif → var → var → params → qualif
qualif-insert-params σ qv v ps = trie-insert σ v (qv , params-to-args ps)

qualif-insert-import : qualif → var → maybe import-as → 𝕃 string → args → qualif
qualif-insert-import σ mn oa [] as = σ
qualif-insert-import σ mn oa (v :: vs) as = qualif-insert-import (trie-insert σ (maybe-else v (λ {(ImportAs _ pfx) → pfx # v}) oa) (mn # v , as)) mn oa vs as

new-ctxt : (filename modname : string) → ctxt
new-ctxt fn mn =
  record {
    fn = fn;
    mn = mn;
    ps = [];
    qual = new-qualif;
    syms = empty-trie;
    mod-map = empty-trie;
    id-map = empty-trie;
    id-current = 0;
    id-list = [];
    i = empty-trie;
    μ = empty-trie;
    μ' = empty-trie;
    Is/μ = empty-trie;
    μ~ = empty-trie;
    μᵤ = nothing;
    μ̲ = empty-stringset
  }

empty-ctxt : ctxt
empty-ctxt = new-ctxt "" ""

ctxt-get-info : var → ctxt → maybe sym-info
ctxt-get-info v Γ = trie-lookup (ctxt.i Γ) v

ctxt-get-qi : ctxt → var → maybe qualif-info
ctxt-get-qi = trie-lookup ∘ ctxt.qual

ctxt-qualif-args-length : ctxt → erased? → var → maybe ℕ
ctxt-qualif-args-length Γ me v =
  ctxt-get-qi Γ v >>= λ qv →
  just (if me then length (snd qv) else length (erase-args (snd qv)))

qi-var-if : maybe qualif-info → var → var
qi-var-if (just (v , _)) _ = v
qi-var-if nothing v = v

--ctxt-restore-info : ctxt → var → maybe qualif-info → maybe sym-info → ctxt
--ctxt-restore-info (mk-ctxt (fn , mn , ps , q , ) syms i Δ) v qi si =
--  mk-ctxt (fn , mn , ps , f qi v q) syms (f si (qi-var-if qi v) (trie-remove i (qi-var-if (trie-lookup q v) v))) Δ
--  where
--    f : ∀{A : Set} → maybe A → string → trie A → trie A
--    f (just a) s t = trie-insert t s a
--    f nothing s t = trie-remove t s

--ctxt-restore-info* : ctxt → 𝕃 (string × maybe qualif-info × maybe sym-info) → ctxt
--ctxt-restore-info* Γ [] = Γ
--ctxt-restore-info* Γ ((v , qi , m) :: ms) = ctxt-restore-info* (ctxt-restore-info Γ v qi m) ms

def-params : defScope → params → defParams
def-params tt ps = nothing
def-params ff ps = just ps

inst-term : ctxt → params → args → term → term
inst-term Γ ps as t with subst-params-args ps as
...| σ , ps' , as' = lam-expand-term (substs-params Γ σ ps') (substs Γ σ t)

-- TODO add renamectxt to avoid capture bugs?
inst-type : ctxt → params → args → type → type
inst-type Γ ps as T with subst-params-args ps as
...| σ , ps' , as' = abs-expand-type (substs-params Γ σ ps') (substs Γ σ T)

inst-kind : ctxt → params → args → kind → kind
inst-kind Γ ps as k with subst-params-args ps as
...| σ , ps' , as' = abs-expand-kind (substs-params Γ σ ps') (substs Γ σ k)

inst-ctrs : ctxt → params → args → ctrs → ctrs
inst-ctrs Γ ps as c with subst-params-args ps as
...| σ , ps' , as' = flip map c λ where
  (Ctr x T) → Ctr x (abs-expand-type (substs-params Γ σ ps') (substs Γ σ T))

maybe-inst-type = maybe-else (λ as T → T) ∘ inst-type
maybe-inst-kind = maybe-else (λ as T → T) ∘ inst-kind
maybe-inst-ctrs = maybe-else (λ as c → c) ∘ inst-ctrs

ctxt-term-decl : posinfo → var → type → ctxt → ctxt
ctxt-term-decl pi v T Γ =
  let v' =  pi % v in
  record Γ {
    qual = qualif-insert-params (ctxt.qual Γ) v' v [];
    i = trie-insert (ctxt.i Γ) v' (term-decl T , ctxt.fn Γ , pi)
  }

ctxt-type-decl : posinfo → var → kind → ctxt → ctxt
ctxt-type-decl pi v k Γ =
  let v' = pi % v in
  record Γ {
    qual = qualif-insert-params (ctxt.qual Γ) v' v [];
    i = trie-insert (ctxt.i Γ) v' (type-decl k , ctxt.fn Γ , pi)
  }

ctxt-tk-decl : posinfo → var → tpkd → ctxt → ctxt
ctxt-tk-decl p x (Tkt t) Γ = ctxt-term-decl p x t Γ
ctxt-tk-decl p x (Tkk k) Γ = ctxt-type-decl p x k Γ

infix 4 _,_-_:`_
_,_-_:`_ : ctxt → posinfo → var → tpkd → ctxt
Γ , pi - x :` tk = ctxt-tk-decl pi x tk Γ

-- TODO not sure how this and renaming interacts with module scope
ctxt-var-decl-if : var → ctxt → ctxt
ctxt-var-decl-if v Γ with trie-lookup (ctxt.i Γ) v
... | just (rename-def _ , _) = Γ
... | just (var-decl , _) = Γ
... | _ = ctxt-var-decl v Γ

add-indices-to-ctxt : indices → ctxt → ctxt
add-indices-to-ctxt = flip $ foldr λ {(Index x _) → ctxt-var-decl x}

add-params-to-ctxt : params → ctxt → ctxt
add-params-to-ctxt = flip $ foldr λ {(Param me x _) Γ → if ctxt-binds-var Γ (unqual-local x) then Γ else (ctxt-var-decl x ∘ ctxt-var-decl (unqual-local x)) Γ}

add-caseArgs-to-ctxt : case-args → ctxt → ctxt
add-caseArgs-to-ctxt = flip $ foldr λ {(CaseArg me x _) → ctxt-var-decl x}

add-ctrs-to-ctxt : ctrs → ctxt → ctxt
add-ctrs-to-ctxt = flip $ foldr λ {(Ctr x T) → ctxt-var-decl x}

ctxt-rename-rep : ctxt → var → var
ctxt-rename-rep Γ v with trie-lookup (ctxt.i Γ) v
...| just (rename-def v' , _) = v'
...| _ = v

-- we assume that only the left variable might have been renamed
ctxt-eq-rep : ctxt → var → var → 𝔹
ctxt-eq-rep Γ x y = (ctxt-rename-rep Γ x) =string y

{- add a renaming mapping the first variable to the second, unless they are equal.
   Notice that adding a renaming for v will overwrite any other declarations for v. -}

ctxt-rename : var → var → ctxt → ctxt
ctxt-rename v v' Γ =
  record Γ {
    qual = trie-insert (ctxt.qual Γ) v (v' , []);
    i = trie-insert (ctxt.i Γ) v (rename-def v' , missing-location)
  }

----------------------------------------------------------------------
-- lookup functions
----------------------------------------------------------------------

-- lookup mod params from filename
lookup-mod-params : ctxt → var → maybe params
lookup-mod-params Γ fn =
  trie-lookup (ctxt.syms Γ) fn >>=c λ mn _ →
  trie-lookup (ctxt.mod-map Γ) mn >>=c λ fn' → just

-- look for a defined kind for the given var, which is assumed to be a type,
-- then instantiate its parameters
qual-lookup : ctxt → var → maybe (var × args × sym-info)
qual-lookup Γ v =
  trie-lookup (ctxt.qual Γ) v >>=c λ qv as →
  trie-lookup (ctxt.i Γ) qv >>= λ si →
  just (qv , as , si)

env-lookup : ctxt → var → maybe sym-info
env-lookup = trie-lookup ∘ ctxt.i

ctxt-lookup-tpkd-var : ctxt → var → maybe (var × args × tpkd)
ctxt-lookup-tpkd-var Γ v with qual-lookup Γ v
... | just (qv , as , term-decl T , _) = just $ qv , as , Tkt T
... | just (qv , as , type-decl k , _) = just $ qv , as , Tkk k
... | just (qv , as , term-def mps _ t T , _) = just $ qv , as , Tkt (maybe-inst-type Γ mps as T)
... | just (qv , as , ctr-def ps T _ _ _ , _) = just $ qv , as , Tkt (inst-type Γ ps as T)
... | just (qv , as , type-def mps _ T k , _) = just $ qv , as , Tkk (maybe-inst-kind Γ mps as k)
... | _ = nothing

ctxt-lookup-type-var : ctxt → var → maybe (var × args × kind)
ctxt-lookup-type-var Γ v = ctxt-lookup-tpkd-var Γ v >>= λ where
  (qv , as , Tkt T) → nothing
  (qv , as , Tkk k) → just (qv , as , k)

ctxt-lookup-term-var : ctxt → var → maybe (var × args × type)
ctxt-lookup-term-var Γ v = ctxt-lookup-tpkd-var Γ v >>= λ where
  (qv , as , Tkt T) → just (qv , as , T)
  (qv , as , Tkk k) → nothing

ctxt-lookup-term-var-def : ctxt → var → maybe term
ctxt-lookup-term-var-def Γ v with env-lookup Γ v
... | just (term-def mps opacity-open (just t) _ , _) = just $ maybe-else id lam-expand-term mps t
... | just (term-udef mps opacity-open t , _) = just $ maybe-else id lam-expand-term mps t
... | _ = nothing

ctxt-lookup-type-var-def : ctxt → var → maybe type
ctxt-lookup-type-var-def Γ v with env-lookup Γ v
... | just (type-def mps opacity-open (just T) _ , _) = just $ maybe-else id lam-expand-type mps T
... | _ = nothing

ctxt-lookup-kind-var-def : ctxt → var → maybe (params × kind)
ctxt-lookup-kind-var-def Γ x with qual-lookup Γ x
...| just (_ , as , kind-def ps k , _) = case subst-params-args' Γ ps as k of λ where
  (k' , ps' , as') → just (ps' , k')
...| _ = nothing

ctxt-binds-term-var : ctxt → var → maybe (var × args)
ctxt-binds-term-var Γ x with qual-lookup Γ x
...| just (qx , as , term-def _ _ _ _ , _) = just (qx , as)
...| just (qx , as , term-udef _ _ _ , _) = just (qx , as)
...| just (qx , as , term-decl _ , _) = just (qx , as)
...| just (qx , as , ctr-def _ _ _ _ _ , _) = just (qx , as)
--...| just (qx , as , var-decl , _) = just (qx , as)
...| _ = nothing

ctxt-binds-type-var : ctxt → var → maybe (var × args)
ctxt-binds-type-var Γ x with qual-lookup Γ x
...| just (qx , as , type-def _ _ _ _ , _) = just (qx , as)
...| just (qx , as , type-decl _ , _) = just (qx , as)
...| _ = nothing

{-
inst-enc-defs : ctxt → params → args → encoding-defs → encoding-defs
inst-enc-defs Γ ps as (mk-enc-defs ecs gcs Cast cast-in cast-out cast-is Functor functor-in functor-out Fix fix-in fix-out lambek1 lambek2 fix-ind) =
  let as = arg-set-erased tt <$> as in
  mk-enc-defs ecs gcs
    (inst-type Γ ps as Cast)
    (inst-term Γ ps as cast-in)
    (inst-term Γ ps as cast-out)
    (inst-term Γ ps as cast-is)
    (inst-type Γ ps as Functor)
    (inst-term Γ ps as functor-in)
    (inst-term Γ ps as functor-out)
    (inst-type Γ ps as Fix)
    (inst-term Γ ps as fix-in)
    (inst-term Γ ps as fix-out)
    (inst-term Γ ps as lambek1)
    (inst-term Γ ps as lambek2)
    (inst-term Γ ps as fix-ind)
-}

data-lookup' : ctxt → var → var → 𝕃 tmtp → maybe datatype-info
data-lookup' Γ xₒ x as =
  (maybe-else'
    {B = maybe (var × args × 𝕃 tmtp ×
                 params × kind × kind × ctrs × encoding-defs × encoded-defs)}
    (trie-lookup (ctxt.μ' Γ) x) -- Is x known locally to be a datatype?
    (trie-lookup (ctxt.μ Γ) x >>=c λ ps rest → -- No, so is it a global datatype?
      let asₚ = tmtps-to-args-for-params nothing ps as
          asᵢ = drop (length ps) as in
      just (x , asₚ , asᵢ , ps , rest))
   λ where
    (x' , as') → -- Yes, it is a local datatype of x', and gives as' as parameters to x'
      trie-lookup (ctxt.μ Γ) x' >>= λ rest → just (x' , as' , as , rest))
  >>= λ where
    (x' , asₚ , asᵢ , ps , kᵢ , k , cs , eds , gds) →
      just $ mk-data-info x' xₒ asₚ asᵢ ps
        (inst-kind Γ ps asₚ kᵢ)
        (inst-kind Γ ps asₚ k)
        cs
        (inst-ctrs Γ ps asₚ (map-snd (subst Γ (params-to-tpapps ps (TpVar x')) x') <$> cs))
        eds {-(inst-enc-defs Γ ps asₚ eds)-}
        gds
        --λ y → inst-ctrs Γ ps asₚ (map-snd (rename-var {TYPE} Γ x' y) <$> cs)

data-lookup : ctxt → var → 𝕃 tmtp → maybe datatype-info
data-lookup Γ x = data-lookup' Γ x x

data-lookup-mu : ctxt → var → var → 𝕃 tmtp → maybe datatype-info
data-lookup-mu Γ xₒ x as =
  trie-lookup (ctxt.Is/μ Γ) x >>= λ x' → data-lookup' Γ xₒ x' as

data-highlight : ctxt → var → ctxt
data-highlight Γ x = record Γ { μ̲ = stringset-insert (ctxt.μ̲ Γ) x }

ctxt-lookup-term-loc : ctxt → var → maybe location
ctxt-lookup-term-loc Γ x = qual-lookup Γ x >>= λ where
  (_ , _ , term-decl _ , loc) → just loc
  (_ , _ , term-def _ _ _ _ , loc) → just loc
  (_ , _ , term-udef _ _ _ , loc) → just loc
  (_ , _ , ctr-def _ _ _ _ _ , loc) → just loc
  (_ , _ , var-decl , loc) → just loc
  _ → nothing

ctxt-lookup-type-loc : ctxt → var → maybe location
ctxt-lookup-type-loc Γ x = qual-lookup Γ x >>= λ where
  (_ , _ , type-decl _ , loc) → just loc
  (_ , _ , type-def _ _ _ _ , loc) → just loc
  (_ , _ , var-decl , loc) → just loc
  _ → nothing

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

ctxt-var-location : ctxt → var → location
ctxt-var-location Γ x with trie-lookup (ctxt.i Γ) x
... | just (_ , l) = l
... | nothing = missing-location

ctxt-clarify-def : ctxt → opacity → var → maybe ctxt
ctxt-clarify-def Γ o x with qual-lookup Γ x
...| just (qx , as , type-def ps o' T? k , loc) =
  maybe-if (o xor o') >>
  just (record Γ { i = trie-insert (ctxt.i Γ) qx (type-def ps o T? k , loc) })
...| just (qx , as , term-def ps o' t? T , loc) =
  maybe-if (o xor o') >>
  just (record Γ { i = trie-insert (ctxt.i Γ) qx (term-def ps o t? T , loc) })
...| just (qx , as , term-udef ps o' t , loc) =
  maybe-if (o xor o') >>
  just (record Γ { i = trie-insert (ctxt.i Γ) qx (term-udef ps o t , loc) })
...| _ = nothing

ctxt-set-current-file : ctxt → string → string → ctxt
ctxt-set-current-file Γ fn mn = record Γ { fn = fn; mn = mn; ps = []; qual = new-qualif }

ctxt-set-current-mod : ctxt → string × string × params × qualif → ctxt
ctxt-set-current-mod Γ (fn , mn , ps , qual) = record Γ { fn = fn; mn = mn; ps = ps; qual = qual }

ctxt-add-current-params : ctxt → ctxt
ctxt-add-current-params Γ =
  record Γ {
    syms = trie-insert (ctxt.syms Γ) (ctxt.fn Γ) (ctxt.mn Γ , []);
    mod-map = trie-insert (ctxt.mod-map Γ) (ctxt.mn Γ) (ctxt.fn Γ , ctxt.ps Γ)
  }

ctxt-clear-symbol : ctxt → string → ctxt
ctxt-clear-symbol Γ x =
  let qx = qualif-var Γ x in
  record Γ {
    qual = trie-remove (ctxt.qual Γ) x;
    syms = trie-map (λ ss → fst ss , remove _=string_ x (snd ss)) (ctxt.syms Γ);
    i = trie-remove (ctxt.i Γ) qx;
    μ = trie-remove (ctxt.μ Γ) qx;
    Is/μ = trie-remove (ctxt.Is/μ Γ) qx;
    μ̲ = trie-remove (ctxt.μ̲ Γ) qx
  }

ctxt-clear-symbols : ctxt → 𝕃 string → ctxt
ctxt-clear-symbols Γ [] = Γ
ctxt-clear-symbols Γ (v :: vs) = ctxt-clear-symbols (ctxt-clear-symbol Γ v) vs

ctxt-clear-symbols-of-file : ctxt → (filename : string) → ctxt
ctxt-clear-symbols-of-file Γ fn =
  elim-pair (trie-lookup𝕃2 (ctxt.syms Γ) fn) λ mn xs →
  let ps = maybe-else' (trie-lookup (ctxt.mod-map Γ) mn) [] snd in
  record Γ {
    syms = trie-insert (ctxt.syms Γ) fn (mn , []);
    mod-map = trie-insert (ctxt.mod-map Γ) mn (fn , ps);
    i = hremove (ctxt.i Γ) mn xs;
    μ = hremove (ctxt.μ Γ) mn xs;
    Is/μ = hremove (ctxt.Is/μ Γ) mn xs;
    μ̲ = hremove (ctxt.μ̲ Γ) mn xs
  }
  where
  hremove : ∀ {A : Set} → trie A → var → 𝕃 string → trie A
  hremove i mn [] = i
  hremove i mn (x :: xs) = hremove (trie-remove i (mn # x)) mn xs

ctxt-add-current-id : ctxt → ctxt
ctxt-add-current-id Γ with trie-contains (ctxt.id-map Γ) (ctxt.fn Γ)
...| tt = Γ
...| ff =
  record Γ {
    id-map = trie-insert (ctxt.id-map Γ) (ctxt.fn Γ) (suc (ctxt.id-current Γ));
    id-current = suc (ctxt.id-current Γ);
    id-list = ctxt.fn Γ :: ctxt.id-list Γ
  }

ctxt-initiate-file : ctxt → (filename modname : string) → ctxt
ctxt-initiate-file Γ fn mn = ctxt-add-current-id (ctxt-set-current-file (ctxt-clear-symbols-of-file Γ fn) fn mn)

unqual : ctxt → var → string
unqual Γ v =
  if qualif-nonempty (ctxt.qual Γ)
  then unqual-local (unqual-all (ctxt.qual Γ) v)
  else v

qualified-ctxt : ctxt → ctxt
qualified-ctxt Γ = -- use ctxt.i so we bring ALL defs (even from cousin modules, etc...) into scope
  record Γ {qual = for trie-strings (ctxt.i Γ) accum empty-trie use λ x q → trie-insert q x (x , [])}

max_stars_repo_name: zmthy/cedille

max_issues_repo_name: zmthy/cedille

max_forks_repo_name: zmthy/cedille


text:
module nat-division-wf where

open import bool
open import bool-thms
open import eq
open import neq
open import nat
open import nat-thms
open import product
open import product-thms
open import sum
open import termination

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infixl 10 _÷_!_

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------

{- a div-result for dividend x and divisor d consists of the quotient q, remainder r,
   a proof that q * d + r = x, and a proof that the remainder is less than the divisor. -}
div-result : ℕ → ℕ → Set
div-result x d = Σ ℕ (λ q → Σ ℕ (λ r → q * d + r ≡ x ∧ r < d ≡ tt))

-- this uses well-founded recursion.  The approach in nat-division.agda is arguably simpler.
div-helper : ∀ (x : ℕ) → ↓𝔹 _>_ x → (d : ℕ) → d =ℕ 0 ≡ ff → div-result x d
div-helper x ↓x 0 ()
div-helper 0 (pf↓ fx) (suc d) _ = 0 , 0 , refl , refl
div-helper (suc x) (pf↓ fx) (suc d) _ with keep (x < d)
div-helper (suc x) (pf↓ fx) (suc d) _ | tt , p = 0 , suc x , refl , p
div-helper (suc x) (pf↓ fx) (suc d) _ | ff , p
  with div-helper (x ∸ d) (fx (∸<1 {x} {d})) (suc d) refl
div-helper (suc x) (pf↓ fx) (suc d) _ | ff , p | q , r , u , v =
  suc q , r , lem{q * suc d} (∸eq-swap{x}{d}{q * suc d + r} (<ff{x} p) u) , v
  where lem : ∀ {a b c : ℕ} → a + b + c ≡ x → suc (c + a + b) ≡ suc x
        lem{a}{b}{c} p' rewrite +comm c a | sym (+assoc a c b)
                              | +comm c b | +assoc a b c | p' = refl

_÷_!_ : (x : ℕ) → (d : ℕ) → d =ℕ 0 ≡ ff → div-result x d
x ÷ d ! p = div-helper x (↓-> x) d p

_÷_!!_ : ℕ → (d : ℕ) → d =ℕ 0 ≡ ff → ℕ × ℕ
x ÷ d !! p with x ÷ d ! p
... | q , r , p' = q , r

-- return quotient only
_÷_div_ : ℕ → (d : ℕ) → d =ℕ 0 ≡ ff → ℕ
x ÷ d div p with x ÷ d ! p
... | q , r , p' = q

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Useful views.
------------------------------------------------------------------------------

open import Data.Nat using (ℕ)

module Data.PropFormula.Views (n : ℕ) where

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

open import Data.PropFormula.Syntax n

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

data nView : PropFormula  → Set where
  conj   : (φ₁ φ₂ : PropFormula) → nView (φ₁ ∧ φ₂)
  disj   : (φ₁ φ₂ : PropFormula) → nView (φ₁ ∨ φ₂)
  impl   : (φ₁ φ₂ : PropFormula) → nView (φ₁ ⊃ φ₂)
  biimpl : (φ₁ φ₂ : PropFormula) → nView (φ₁ ⇔ φ₂)
  nconj  : (φ₁ φ₂ : PropFormula) → nView (¬ (φ₁ ∧ φ₂))
  ndisj  : (φ₁ φ₂ : PropFormula) → nView (¬ (φ₁ ∨ φ₂))
  nneg   : (φ₁ : PropFormula)    → nView (¬ ¬ φ₁)
  nimpl  : (φ₁ φ₂ : PropFormula) → nView (¬ (φ₁ ⊃ φ₂))
  nbiim  : (φ₁ φ₂ : PropFormula) → nView (¬ (φ₁ ⇔ φ₂))
  ntop   : nView (¬ ⊤)
  nbot   : nView (¬ ⊥)
  other  : (φ₁ : PropFormula)    → nView φ₁

n-view : (φ : PropFormula) → nView φ
n-view (φ₁ ∧ φ₂)     = conj _ _
n-view (φ₁ ∨ φ₂)     = disj _ _
n-view (φ₁ ⊃ φ₂)     = impl _ _
n-view (φ₁ ⇔ φ₂)     = biimpl _ _
n-view (¬ (φ₁ ∧ φ₂)) = nconj _ _
n-view (¬ (φ₁ ∨ φ₂)) = ndisj _ _
n-view (¬ (φ₁ ⊃ φ₂)) = nimpl _ _
n-view (¬ (φ₁ ⇔ φ₂)) = nbiim _ _
n-view (¬ (¬ φ₁))    = nneg _
n-view (¬ ⊤)         = ntop
n-view (¬ ⊥)         = nbot
n-view φ₁            = other _

data ConjView : PropFormula → Set where
  conj  : (φ₁ φ₂ : PropFormula) → ConjView (φ₁ ∧ φ₂)
  other : (φ : PropFormula)     → ConjView φ

conj-view : (φ : PropFormula) → ConjView φ
conj-view (φ₁ ∧ φ₂) = conj _ _
conj-view φ         = other _

data DisjView : PropFormula → Set where
  disj  : (φ₁ φ₂ : PropFormula) → DisjView (φ₁ ∨ φ₂)
  other : (φ : PropFormula)     → DisjView φ

disj-view : (φ : PropFormula) → DisjView φ
disj-view (φ₁ ∨ φ₂) = disj _ _
disj-view φ         = other _

data dView : PropFormula → Set where
  conj  : (φ₁ φ₂ : PropFormula) → dView (φ₁ ∧ φ₂)
  disj  : (φ₁ φ₂ : PropFormula) → dView (φ₁ ∨ φ₂)
  other : (φ : PropFormula)     → dView φ

d-view : (φ : PropFormula) → dView φ
d-view (φ₁ ∧ φ₂) = conj _ _
d-view (φ₁ ∨ φ₂) = disj _ _
d-view φ         = other _

data dViewAux : PropFormula → Set where
  case₁ : (φ₁ φ₂ φ₃ : PropFormula) → dViewAux ((φ₁ ∨ φ₂) ∧ φ₃)
  case₂ : (φ₁ φ₂ φ₃ : PropFormula) → dViewAux (φ₁ ∧ (φ₂ ∨ φ₃))
  other : (φ : PropFormula)        → dViewAux φ

d-view-aux : (φ : PropFormula) → dViewAux φ
d-view-aux ((φ₁ ∨ φ₂) ∧ φ₃) = case₁ _ _ _
d-view-aux (φ₁ ∧ (φ₂ ∨ φ₃)) = case₂ _ _ _
d-view-aux φ                = other _

data cViewAux : PropFormula → Set where
  case₁ : (φ₁ φ₂ φ₃ : PropFormula) → cViewAux ((φ₁ ∧ φ₂) ∨ φ₃)
  case₂ : (φ₁ φ₂ φ₃ : PropFormula) → cViewAux (φ₁ ∨ (φ₂ ∧ φ₃))
  other : (φ : PropFormula)        → cViewAux φ

c-view-aux : (φ : PropFormula) → cViewAux φ
c-view-aux ((φ ∧ ψ) ∨ φ₃) = case₁ _ _ _
c-view-aux (φ ∨ (ψ ∧ φ₃)) = case₂ _ _ _
c-view-aux φ              = other _

data ImplView : PropFormula → Set where
  impl  : (φ₁ φ₂ : PropFormula) → ImplView (φ₁ ⊃ φ₂)
  other : (φ : PropFormula)     → ImplView φ

impl-view : (φ : PropFormula) → ImplView φ
impl-view (φ₁ ⊃ φ₂) = impl _ _
impl-view φ         = other _

data BiimplView : PropFormula → Set where
  biimpl  : (φ₁ φ₂ : PropFormula) → BiimplView (φ₁ ⇔ φ₂)
  other : (φ : PropFormula)       → BiimplView φ

biimpl-view : (φ : PropFormula) → BiimplView φ
biimpl-view (φ₁ ⇔ φ₂) = biimpl _ _
biimpl-view φ         = other _

data NegView : PropFormula → Set where
  neg : (φ : PropFormula) → NegView (¬ φ)
  pos : (φ : PropFormula) → NegView φ

neg-view : (φ : PropFormula) → NegView φ
neg-view (¬ φ) = neg _
neg-view φ     = pos _

data PushNegView : PropFormula → Set where
  yes  : (φ : PropFormula)     → PushNegView φ
  no-∧ : (φ₁ φ₂ : PropFormula) → PushNegView (φ₁ ∧ φ₂)
  no-∨ : (φ₁ φ₂ : PropFormula) → PushNegView (φ₁ ∨ φ₂)
  no   : (φ : PropFormula)     → PushNegView φ

push-neg-view : (φ : PropFormula) → PushNegView φ
push-neg-view φ with n-view φ
push-neg-view .(φ₁ ∧ φ₂)     | conj φ₁ φ₂   = no-∧ _ _
push-neg-view .(φ₁ ∨ φ₂)     | disj φ₁ φ₂   = no-∨ _ _
push-neg-view .(φ₁ ⊃ φ₂)     | impl φ₁ φ₂   = yes _
push-neg-view .(φ₁ ⇔ φ₂)     | biimpl φ₁ φ₂ = yes _
push-neg-view .(¬ (φ₁ ∧ φ₂)) | nconj φ₁ φ₂  = yes _
push-neg-view .(¬ (φ₁ ∨ φ₂)) | ndisj φ₁ φ₂  = yes _
push-neg-view .(¬ (¬ φ₁))    | nneg φ₁      = yes _
push-neg-view .(¬ (φ₁ ⊃ φ₂)) | nimpl φ₁ φ₂  = yes _
push-neg-view .(¬ (φ₁ ⇔ φ₂)) | nbiim φ₁ φ₂  = yes _
push-neg-view .(¬ ⊤)         | ntop         = yes _
push-neg-view .(¬ ⊥)         | nbot         = yes _
push-neg-view φ              | other .φ     = no _

data LiteralView : PropFormula → Set where
  yes : (φ : PropFormula) → LiteralView φ
  no  : (φ : PropFormula) → LiteralView φ

literal-view : (φ : PropFormula) → LiteralView φ
literal-view φ with n-view φ
literal-view .(φ₁ ∧ φ₂)     | conj φ₁ φ₂   = no _
literal-view .(φ₁ ∨ φ₂)     | disj φ₁ φ₂   = no _
literal-view .(φ₁ ⊃ φ₂)     | impl φ₁ φ₂   = no _
literal-view .(φ₁ ⇔ φ₂)     | biimpl φ₁ φ₂ = no _
literal-view .(¬ (φ₁ ∧ φ₂)) | nconj φ₁ φ₂  = no _
literal-view .(¬ (φ₁ ∨ φ₂)) | ndisj φ₁ φ₂  = no _
literal-view .(¬ (¬ φ₁))    | nneg φ₁      = no _
literal-view .(¬ (φ₁ ⊃ φ₂)) | nimpl φ₁ φ₂  = no _
literal-view .(¬ (φ₁ ⇔ φ₂)) | nbiim φ₁ φ₂  = no _
literal-view .(¬ ⊤)         | ntop         = yes _
literal-view .(¬ ⊥)         | nbot         = yes _
literal-view φ              | other _      = yes _

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
open import Agda.Builtin.Nat

f : Nat → Nat
f 0 = zero
f 0 = 0        -- All                      -- But Only
f (suc n) = n  -- These
f 0 = 0        -- Lines                    -- These Two
               -- Used to be highlighted   -- Should be!

g : Nat → Nat
g 0 = zero
g 0     -- The highlihting should still
  = 0   -- span multiple lines if the clause does
g (suc n) = n
g 0     -- Even
        -- With
        -- A Lot
   = 0  -- Of Empty Lines in between


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

open import lib.Basics
open import lib.NType2
open import lib.types.Empty
open import lib.types.Group
open import lib.types.Int
open import lib.types.List
open import lib.types.Nat
open import lib.types.Pi
open import lib.types.SetQuotient
open import lib.types.Sigma
open import lib.types.Word
open import lib.groups.GroupProduct
open import lib.groups.Homomorphism
open import lib.groups.Isomorphism

module lib.groups.FreeAbelianGroup {i} where

-- the relation for making the quotient.

-- [fsr-sym] is not needed, but it seems more principled to
-- make [FormalSumRel] an equivalence relation.
data FormalSumRel {A : Type i} : Word A → Word A → Type i where
  fsr-refl : ∀ {l₁ l₂} → l₁ == l₂ → FormalSumRel l₁ l₂
  fsr-trans : ∀ {l₁ l₂ l₃} → FormalSumRel l₁ l₂ → FormalSumRel l₂ l₃ → FormalSumRel l₁ l₃
  fsr-sym : ∀ {l₁ l₂} → FormalSumRel l₁ l₂ → FormalSumRel l₂ l₁
  fsr-cons : ∀ x {l₁ l₂} → FormalSumRel l₁ l₂ → FormalSumRel (x :: l₁) (x :: l₂)
  fsr-swap : ∀ x₁ x₂ l → FormalSumRel (x₁ :: x₂ :: l) (x₂ :: x₁ :: l)
  fsr-flip : ∀ x₁ l → FormalSumRel (x₁ :: flip x₁ :: l) l

-- The quotient
FormalSum : Type i → Type i
FormalSum A = SetQuot (FormalSumRel {A})

module _ {A : Type i} where

  fs[_] : Word A → FormalSum A
  fs[_] = q[_]

  module FormalSumElim {k} {P : FormalSum A → Type k}
    {{p : {x : FormalSum A} → is-set (P x)}} (incl* : (a : Word A) → P fs[ a ])
    (rel* : ∀ {a₁ a₂} (r : FormalSumRel a₁ a₂) → incl* a₁ == incl* a₂ [ P ↓ quot-rel r ])
    = SetQuotElim incl* rel*
  open FormalSumElim public using () renaming (f to FormalSum-elim)

  module FormalSumRec {k} {B : Type k} {{p : is-set B}} (incl* : Word A → B)
    (rel* : ∀ {a₁ a₂} (r : FormalSumRel a₁ a₂) → incl* a₁ == incl* a₂)
    = SetQuotRec incl* rel*
  open FormalSumRec public using () renaming (f to FormalSum-rec)

module _ {A : Type i} where
  -- useful properties that remain public
  abstract
    FormalSumRel-cong-++-l :
      ∀ {l₁ l₁'} → FormalSumRel {A} l₁ l₁'
      → (l₂ : Word A)
      → FormalSumRel (l₁ ++ l₂) (l₁' ++ l₂)
    FormalSumRel-cong-++-l (fsr-refl idp) l₂ = fsr-refl idp
    FormalSumRel-cong-++-l (fsr-trans fsr₁ fsr₂) l₂ = fsr-trans (FormalSumRel-cong-++-l fsr₁ l₂) (FormalSumRel-cong-++-l fsr₂ l₂)
    FormalSumRel-cong-++-l (fsr-sym fsr) l₂ = fsr-sym (FormalSumRel-cong-++-l fsr l₂)
    FormalSumRel-cong-++-l (fsr-cons x fsr₁) l₂ = fsr-cons x (FormalSumRel-cong-++-l fsr₁ l₂)
    FormalSumRel-cong-++-l (fsr-swap x₁ x₂ l₁) l₂ = fsr-swap x₁ x₂ (l₁ ++ l₂)
    FormalSumRel-cong-++-l (fsr-flip x₁ l₁) l₂ = fsr-flip x₁ (l₁ ++ l₂)

    FormalSumRel-cong-++-r :
      ∀ (l₁ : Word A)
      → ∀ {l₂ l₂'} → FormalSumRel l₂ l₂'
      → FormalSumRel (l₁ ++ l₂) (l₁ ++ l₂')
    FormalSumRel-cong-++-r nil fsr₂ = fsr₂
    FormalSumRel-cong-++-r (x :: l₁) fsr₂ = fsr-cons x (FormalSumRel-cong-++-r l₁ fsr₂)

    FormalSumRel-swap1 : ∀ x l₁ l₂ → FormalSumRel {A} (l₁ ++ (x :: l₂)) (x :: l₁ ++ l₂)
    FormalSumRel-swap1 x nil l₂ = fsr-refl idp
    FormalSumRel-swap1 x (x₁ :: l₁) l₂ = fsr-trans (fsr-cons x₁ (FormalSumRel-swap1 x l₁ l₂)) (fsr-swap x₁ x (l₁ ++ l₂))

module _ (A : Type i) where
  private
    infixl 80 _⊞_
    _⊞_ : FormalSum A → FormalSum A → FormalSum A
    _⊞_ = FormalSum-rec
      (λ l₁ → FormalSum-rec (λ l₂ → fs[ l₁ ++ l₂ ])
        (λ r → quot-rel $ FormalSumRel-cong-++-r l₁ r))
      (λ {l₁} {l₁'} r → λ= $ FormalSum-elim
        (λ l₂ → quot-rel $ FormalSumRel-cong-++-l r l₂)
        (λ _ → prop-has-all-paths-↓))

    abstract
      FormalSumRel-cong-flip : ∀ {l₁ l₂}
        → FormalSumRel {A} l₁ l₂ → FormalSumRel (Word-flip l₁) (Word-flip l₂)
      FormalSumRel-cong-flip (fsr-refl idp) = fsr-refl idp
      FormalSumRel-cong-flip (fsr-trans fsr₁ fsr₂) = fsr-trans (FormalSumRel-cong-flip fsr₁) (FormalSumRel-cong-flip fsr₂)
      FormalSumRel-cong-flip (fsr-sym fsr) = fsr-sym (FormalSumRel-cong-flip fsr)
      FormalSumRel-cong-flip (fsr-cons x fsr₁) = fsr-cons (flip x) (FormalSumRel-cong-flip fsr₁)
      FormalSumRel-cong-flip (fsr-swap x₁ x₂ l) = fsr-swap (flip x₁) (flip x₂) (Word-flip l)
      FormalSumRel-cong-flip (fsr-flip (inl x) l) = fsr-flip (inr x) (Word-flip l)
      FormalSumRel-cong-flip (fsr-flip (inr x) l) = fsr-flip (inl x) (Word-flip l)

    ⊟ : FormalSum A → FormalSum A
    ⊟ = FormalSum-rec (fs[_] ∘ Word-flip)
      (λ r → quot-rel $ FormalSumRel-cong-flip r)

    ⊞-unit : FormalSum A
    ⊞-unit = fs[ nil ]

    abstract
      ⊞-unit-l : ∀ g → ⊞-unit ⊞ g == g
      ⊞-unit-l = FormalSum-elim
        (λ _ → idp)
        (λ _ → prop-has-all-paths-↓)

      ⊞-assoc : ∀ g₁ g₂ g₃ → (g₁ ⊞ g₂) ⊞ g₃ == g₁ ⊞ (g₂ ⊞ g₃)
      ⊞-assoc = FormalSum-elim
        (λ l₁ → FormalSum-elim
          (λ l₂ → FormalSum-elim
            (λ l₃ → ap fs[_] $ ++-assoc l₁ l₂ l₃)
            (λ _ → prop-has-all-paths-↓))
          (λ _ → prop-has-all-paths-↓))
        (λ _ → prop-has-all-paths-↓)

      Word-inv-l : ∀ l → FormalSumRel {A} (Word-flip l ++ l) nil
      Word-inv-l nil = fsr-refl idp
      Word-inv-l (x :: l) =
        fsr-trans (FormalSumRel-swap1 x (flip x :: Word-flip l) l) $
        fsr-trans (fsr-flip x (Word-flip l ++ l)) (Word-inv-l l)

      ⊟-inv-l : ∀ g → (⊟ g) ⊞ g == ⊞-unit
      ⊟-inv-l = FormalSum-elim
        (λ l → quot-rel (Word-inv-l l))
        (λ _ → prop-has-all-paths-↓)

      FormalSumRel-swap : ∀ l₁ l₂ → FormalSumRel {A} (l₁ ++ l₂) (l₂ ++ l₁)
      FormalSumRel-swap l₁ nil = fsr-refl (++-unit-r l₁)
      FormalSumRel-swap l₁ (x :: l₂) = fsr-trans (FormalSumRel-swap1 x l₁ l₂) (fsr-cons x (FormalSumRel-swap l₁ l₂))

      ⊞-comm : ∀ g₁ g₂ → g₁ ⊞ g₂ == g₂ ⊞ g₁
      ⊞-comm = FormalSum-elim
        (λ l₁ → FormalSum-elim
          (λ l₂ → quot-rel $ FormalSumRel-swap l₁ l₂)
          (λ _ → prop-has-all-paths-↓))
        (λ _ → prop-has-all-paths-↓)

  FormalSum-group-structure : GroupStructure (FormalSum A)
  FormalSum-group-structure = record
    { ident = ⊞-unit
    ; inv = ⊟
    ; comp = _⊞_
    ; unit-l = ⊞-unit-l
    ; assoc = ⊞-assoc
    ; inv-l = ⊟-inv-l
    }

  FreeAbGroup : AbGroup i
  FreeAbGroup = group _ FormalSum-group-structure , ⊞-comm

  module FreeAbGroup = AbGroup FreeAbGroup

{- Freeness (universal properties) -}

module _ {A : Type i} {j} (G : AbGroup j) where

  private
    module G = AbGroup G

    abstract
      Word-extendᴳ-emap : ∀ f {l₁ l₂}
        → FormalSumRel {A} l₁ l₂
        → Word-extendᴳ G.grp f l₁ == Word-extendᴳ G.grp f l₂
      Word-extendᴳ-emap f (fsr-refl idp) = idp
      Word-extendᴳ-emap f (fsr-trans fsr fsr₁) = (Word-extendᴳ-emap f fsr) ∙ (Word-extendᴳ-emap f fsr₁)
      Word-extendᴳ-emap f (fsr-sym fsr) = ! (Word-extendᴳ-emap f fsr)
      Word-extendᴳ-emap f (fsr-cons x fsr) = ap (G.comp (PlusMinus-extendᴳ G.grp f x)) (Word-extendᴳ-emap f fsr)
      Word-extendᴳ-emap f (fsr-swap x₁ x₂ l) =
          ! (G.assoc (PlusMinus-extendᴳ G.grp f x₁) (PlusMinus-extendᴳ G.grp f x₂) (Word-extendᴳ G.grp f l))
        ∙ ap (λ g → G.comp g (Word-extendᴳ G.grp f l)) (G.comm (PlusMinus-extendᴳ G.grp f x₁) (PlusMinus-extendᴳ G.grp f x₂))
        ∙ G.assoc (PlusMinus-extendᴳ G.grp f x₂) (PlusMinus-extendᴳ G.grp f x₁) (Word-extendᴳ G.grp f l)
      Word-extendᴳ-emap f (fsr-flip (inl x) l) =
          ! (G.assoc (f x) (G.inv (f x)) (Word-extendᴳ G.grp f l))
        ∙ ap (λ g → G.comp g (Word-extendᴳ G.grp f l)) (G.inv-r (f x)) ∙ G.unit-l _
      Word-extendᴳ-emap f (fsr-flip (inr x) l) =
          ! (G.assoc (G.inv (f x)) (f x) (Word-extendᴳ G.grp f l))
        ∙ ap (λ g → G.comp g (Word-extendᴳ G.grp f l)) (G.inv-l (f x)) ∙ G.unit-l _

  FormalSum-extend : (A → G.El) → FormalSum A → G.El
  FormalSum-extend f = FormalSum-rec (Word-extendᴳ G.grp f)
    (λ r → Word-extendᴳ-emap f r)

  FreeAbGroup-extend : (A → G.El) → (FreeAbGroup.grp A →ᴳ G.grp)
  FreeAbGroup-extend f' = record {M} where
    module M where
      f : FreeAbGroup.El A → G.El
      f = FormalSum-extend f'
      abstract
        pres-comp : preserves-comp (FreeAbGroup.comp A) G.comp f
        pres-comp =
          FormalSum-elim
            (λ l₁ → FormalSum-elim
              (λ l₂ → Word-extendᴳ-++ G.grp f' l₁ l₂)
              (λ _ → prop-has-all-paths-↓))
            (λ _ → prop-has-all-paths-↓)

  private
    module Lemma (hom : FreeAbGroup.grp A →ᴳ G.grp) where
      open GroupHom hom
      f* : A → G.El
      f* a = f fs[ inl a :: nil ]

      abstract
        PlusMinus-extend-hom : ∀ x → PlusMinus-extendᴳ G.grp f* x == f fs[ x :: nil ]
        PlusMinus-extend-hom (inl x) = idp
        PlusMinus-extend-hom (inr x) = ! $ pres-inv fs[ inl x :: nil ]

        Word-extend-hom : ∀ l → Word-extendᴳ G.grp f* l == f fs[ l ]
        Word-extend-hom nil = ! pres-ident
        Word-extend-hom (x :: l) = ap2 G.comp (PlusMinus-extend-hom x) (Word-extend-hom l) ∙ ! (pres-comp _ _)
    open Lemma

  FreeAbGroup-extend-is-equiv : is-equiv FreeAbGroup-extend
  FreeAbGroup-extend-is-equiv = is-eq _ from to-from from-to where
    to = FreeAbGroup-extend
    from = f*

    abstract
      to-from : ∀ h → to (from h) == h
      to-from h = group-hom= $ λ= $ FormalSum-elim
        (λ l → Word-extend-hom h l)
        (λ _ → prop-has-all-paths-↓)

      from-to : ∀ f → from (to f) == f
      from-to f = λ= λ a → G.unit-r (f a)

  FreeAbGroup-extend-hom : Πᴳ A (λ _ → G.grp) →ᴳ hom-group (FreeAbGroup.grp A) G
  FreeAbGroup-extend-hom = record {M} where
    module M where
      f : (A → G.El) → (FreeAbGroup.grp A →ᴳ G.grp)
      f = FreeAbGroup-extend
      abstract
        pres-comp : preserves-comp (Group.comp (Πᴳ A (λ _ → G.grp))) (Group.comp (hom-group (FreeAbGroup.grp A) G)) f
        pres-comp = λ f₁ f₂ → group-hom= $ λ= $
          FormalSum-elim
            (Word-extendᴳ-comp G f₁ f₂)
            (λ _ → prop-has-all-paths-↓)

  FreeAbGroup-extend-iso : Πᴳ A (λ _ → G.grp) ≃ᴳ hom-group (FreeAbGroup.grp A) G
  FreeAbGroup-extend-iso = FreeAbGroup-extend-hom , FreeAbGroup-extend-is-equiv

{- relation with [Word-exp] -}

module _ {A : Type i} where

  abstract
    FormalSumRel-pres-exp : ∀ (a : A) z →
      fs[ Word-exp a z ] == GroupStructure.exp (FormalSum-group-structure A) fs[ inl a :: nil ] z
    FormalSumRel-pres-exp a (pos O) = idp
    FormalSumRel-pres-exp a (pos (S O)) = idp
    FormalSumRel-pres-exp a (pos (S (S n))) =
      ap (Group.comp (FreeAbGroup.grp A) fs[ inl a :: nil ]) (FormalSumRel-pres-exp a (pos (S n)))
    FormalSumRel-pres-exp a (negsucc O) = idp
    FormalSumRel-pres-exp a (negsucc (S n)) =
      ap (Group.comp (FreeAbGroup.grp A) fs[ inr a :: nil ]) (FormalSumRel-pres-exp a (negsucc n))


text:
open import Agda.Builtin.IO
open import Agda.Builtin.Reflection
open import Agda.Builtin.String
open import Agda.Builtin.Unit

_>>=_ : {A B : Set} → TC A → (A → TC B) → TC B
_>>=_ = λ x f → bindTC x f

postulate
  putStr : String → IO ⊤

{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# COMPILE GHC putStr = Data.Text.IO.putStr #-}
{-# COMPILE JS putStr =
    function (x) {
      return function(cb) {
        process.stdout.write(x); cb(0); }; } #-}

main : IO ⊤
main = putStr "Success\n"


text:
{- trying (and failing) to create a univesal "successor" -}
-- types with and without payloads defined dependently, those w/o payloads in terms of those with (using ⊤ as a trivial payload)
-- this complicates the successor constructor, `!`, so we use use pattern (OR function?), `¡`
module Oscar.Data3 where

record ⊤ : Set where
  constructor tt

infixr 20 _∷_

-- List
data ⟦_⟧ {a} (A : Set a) : Set a where
  ∅ : ⟦ A ⟧
  _∷_ : A → ⟦ A ⟧ → ⟦ A ⟧

-- Nat
⟦⟧ = ⟦ ⊤ ⟧

infix 21 ¡_
pattern ¡_ ⟦A⟧ = tt ∷ ⟦A⟧
--¡ : ⟦⟧ → ⟦⟧
--¡ ⟦A⟧ = tt ∷ ⟦A⟧

-- Fin, with payload
data ⟦_⟧[_] {a} (A : ⟦⟧ → Set a) : ⟦⟧ → Set a where
  ∅ : ∀ {n} → ⟦ A ⟧[ ¡ n ]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ n ] → ⟦ A ⟧[ ¡ n ]

data ⟦_⟧[_₀] {a} (A : ⟦⟧ → Set a) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[ ∅ ₀]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ n ₀] → ⟦ A ⟧[ ¡ n ₀]

Const_ : ∀ {a} {A : Set a} {b} {B : Set b} → B → A → B
Const_ x _ = x

⟦⟧[_₀] = ⟦ Const ⊤ ⟧[_₀]

-- Fin
⟦⟧[_] = ⟦ Const ⊤ ⟧[_]

-- m ≤ n, counting down from n-1 to m
data ⟦_⟧[_≤↓_] {a} (A : ⟦⟧ → Set a) (m : ⟦⟧) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[ m ≤↓ m ]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ m ≤↓ n ] → ⟦ A ⟧[ m ≤↓ ¡ n ]

infix 21 ‼_
pattern ‼_ ⟦A⟧ = tt ∷ ⟦A⟧ -- tricky, works for all above _∷_ constructors only because it is defined afterwards, won't work for later-defined constructors

testNat : ⟦⟧
testNat = ¡ ∅

testListNat : ⟦ ⟦⟧ ⟧
testListNat = ¡ ∅ ∷ ‼ ∅ ∷ ‼ ‼ ∅ ∷ ∅ ∷ ¡ ¡ ¡ ∅ ∷ ∅

testFin : ⟦⟧[ ¡ ¡ ∅ ]
testFin = ‼ ∅

⟦⟧[_≤↓_] = ⟦ Const ⊤ ⟧[_≤↓_]

test≤↓ : ⟦⟧[ ‼ ‼ ‼ ∅ ≤↓ ‼ ‼ ‼ ‼ ‼ ∅ ]
test≤↓ = ‼ ‼ ∅

-- m ≤ n, counting up from m to n-1
data ⟦_⟧[_↑≤_] {a} (A : ⟦⟧ → Set a) (m : ⟦⟧) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[ m ↑≤ m ]
  _∷_ : ∀ {n} → A m → ⟦ A ⟧[ ¡ m ↑≤ n ] → ⟦ A ⟧[ m ↑≤ n ]

⟦⟧[_↑≤_] = ⟦ Const ⊤ ⟧[_↑≤_]

-- Inj (almost)
data ⟦_⟧[_↓≤↓_] {a} (A : ⟦⟧ → ⟦⟧ → Set a) : ⟦⟧ → ⟦⟧ → Set a where
  ∅ : ∀ {n} → ⟦ A ⟧[ ∅ ↓≤↓ n ]
  _∷_ : ∀ {m n} → A m n → ⟦ A ⟧[ m ↓≤↓ n ] → ⟦ A ⟧[ ¡ m ↓≤↓ ¡ n ]

⟦⟧[_↓≤↓_] = ⟦ Const Const ⊤ ⟧[_↓≤↓_]

⓪ ⑴ ⑵ : ⟦⟧
⓪ = ∅
⑴ = ‼ ∅
⑵ = ‼ ⑴

data D : ⟦⟧ → ⟦⟧ → Set where
  List : D ⓪ ⓪
  Fin : D ⑴ ⑴
  Vec : D ⑴ ⑴
  Descend : D ⑴ ⑵
  Ascend : D ⑴ ⑵
  Inj : D ⑵ ⑵

open import Oscar.Level
theA : ∀ ℓ → ⟦⟧ → Set (lsuc ℓ)
theA ℓ ∅ = Set ℓ
theA ℓ (tt ∷ x₁) = ⟦⟧ → theA ℓ x₁

theIndices : ⟦⟧ → Set
theIndices x = ⟦ Const ⟦⟧ ⟧[ x ₀]

μ : ∀ {p i} → D p i → ∀ {a} → theA a p → theIndices i → Set a
μ List A _ = ⟦ A ⟧
μ Fin A (n ∷ _) = ⟦ A ⟧[ n ]
μ Vec A (n ∷ _) = ⟦ A ⟧[ n ₀]
μ Descend A (m ∷ n ∷ _) = ⟦ A ⟧[ m ≤↓ n ]
μ Ascend A (m ∷ n ∷ _) = ⟦ A ⟧[ m ↑≤ n ]
μ Inj A (m ∷ n ∷ ∅) = ⟦ A ⟧[ m ↓≤↓ n ]

μ¡ : ∀ {p i} → D p i → theIndices i → Set
μ¡ List _ = ⟦⟧ → ⟦⟧
μ¡ Fin (n ∷ _) = ⟦⟧[ n ] → ⟦⟧[ ¡ n ]
μ¡ Vec (n ∷ _) = ⟦⟧[ n ₀] → ⟦⟧[ ¡ n ₀]
μ¡ Descend (m ∷ n ∷ _) = ⟦⟧[ m ≤↓ n ] → ⟦⟧[ m ≤↓ ¡ n ]
μ¡ Ascend (m ∷ n ∷ _) = ⟦⟧[ ¡ m ↑≤ n ] → ⟦⟧[ m ↑≤ n ]
μ¡ Inj (m ∷ n ∷ _) = ⟦⟧[ m ↓≤↓ n ] → ⟦⟧[ ¡ m ↓≤↓ ¡ n ]

μ¡↑ : ∀ {p i} → D p i → Set
μ¡↑ List = ⟦⟧ → ⟦⟧
μ¡↑ Fin = {!!}
μ¡↑ Vec = {!!}
μ¡↑ Descend = {!!}
μ¡↑ Ascend = {!!}
μ¡↑ Inj = {!!}

theArguments : ∀ {p i} → (d : D p i) → Set
theArguments List = μ¡ List ∅
theArguments Fin = {n : ⟦⟧} → μ¡ Fin (n ∷ ∅)
theArguments Vec = {n : ⟦⟧} → μ¡ Vec (n ∷ ∅)
theArguments Descend = {m : ⟦⟧} → {n : ⟦⟧} → μ¡ Descend (m ∷ n ∷ ∅)
theArguments Ascend = {m : ⟦⟧} → {n : ⟦⟧} → μ¡ Ascend (m ∷ n ∷ ∅)
theArguments Inj = {m : ⟦⟧} → {n : ⟦⟧} → μ¡ Inj (m ∷ n ∷ ∅)

infix 21 ↑_
↑_ : ∀ {p i} → {d : D p i} → {I : theIndices i} → μ¡ d I
↑_ {d = List} = ‼_
↑_ {d = Fin} {x ∷ I} = ‼_
↑_ {d = Vec} {x ∷ I} = ‼_
↑_ {d = Descend} {x ∷ x₁ ∷ I} = ‼_
↑_ {d = Ascend} {x ∷ x₁ ∷ I} = tt ∷_
↑_ {d = Inj} {x ∷ x₁ ∷ I} = tt ∷_

↑↑ : ∀ {p i} → {d : D p i} → theArguments d
↑↑ {d = List} = {!‼_!}
↑↑ {d = Fin} = ‼_
↑↑ {d = Vec} = ‼_
↑↑ {d = Descend} = ‼_
↑↑ {d = Ascend} = tt ∷_
↑↑ {d = Inj} = tt ∷_

record BANG {p i} (d : D p i) : Set where
  field
    ⟰ : theArguments d

open BANG ⦃ … ⦄

instance BANGFin : BANG Fin
BANG.⟰ BANGFin {n} = ‼_

testμ : μ Fin (Const ⊤) (‼ ‼ ‼ ‼ ∅ ∷ ∅)
testμ = ⟰ {d = Fin} {!!}  -- ↑↑ {d = Fin} {!!}
-- ↑_ {d = Fin} {I = _ ∷ {!!}} ∅
-- ↑_ {d = Fin} {I = {!!} ∷ {!!}} {!!}
{-
data ⟦_⟧ {a} (A : Set a) : Set a where
data ⟦_⟧[_] {a} (A : ⟦⟧ → Set a) : ⟦⟧ → Set a where
data ⟦_⟧[_≤↓_] {a} (A : ⟦⟧ → Set a) (m : ⟦⟧) : ⟦⟧ → Set a where
data ⟦_⟧[_↑≤_] {a} (A : ⟦⟧ → Set a) (m : ⟦⟧) : ⟦⟧ → Set a where
data ⟦_⟧[_↓≤↓_] {a} (A : ⟦⟧ → ⟦⟧ → Set a) : ⟦⟧ → ⟦⟧ → Set a where
-}