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

module abelian-groups where

import 17-number-theory
open 17-number-theory public

is-abelian-Group :
  {l : Level} (G : Group l) → UU l
is-abelian-Group G =
  (x y : type-Group G) → Id (mul-Group G x y) (mul-Group G y x)

Ab : (l : Level) → UU (lsuc l)
Ab l = Σ (Group l) is-abelian-Group

group-Ab :
  {l : Level} (A : Ab l) → Group l
group-Ab A = pr1 A

set-Ab :
  {l : Level} (A : Ab l) → UU-Set l
set-Ab A = set-Group (group-Ab A)

type-Ab :
  {l : Level} (A : Ab l) → UU l
type-Ab A = type-Group (group-Ab A)

is-set-type-Ab :
  {l : Level} (A : Ab l) → is-set (type-Ab A)
is-set-type-Ab A = is-set-type-Group (group-Ab A)

associative-add-Ab :
  {l : Level} (A : Ab l) → has-associative-bin-op (set-Ab A)
associative-add-Ab A = associative-mul-Group (group-Ab A)

add-Ab :
  {l : Level} (A : Ab l) → type-Ab A → type-Ab A → type-Ab A
add-Ab A = mul-Group (group-Ab A)

is-associative-add-Ab :
  {l : Level} (A : Ab l) (x y z : type-Ab A) →
  Id (add-Ab A (add-Ab A x y) z) (add-Ab A x (add-Ab A y z))
is-associative-add-Ab A = is-associative-mul-Group (group-Ab A)

semi-group-Ab :
  {l : Level} (A : Ab l) → Semi-Group l
semi-group-Ab A = semi-group-Group (group-Ab A)

is-group-Ab :
  {l : Level} (A : Ab l) → is-group (semi-group-Ab A)
is-group-Ab A = is-group-Group (group-Ab A)

has-zero-Ab :
  {l : Level} (A : Ab l) → is-unital (semi-group-Ab A)
has-zero-Ab A = is-unital-Group (group-Ab A)

zero-Ab :
  {l : Level} (A : Ab l) → type-Ab A
zero-Ab A = unit-Group (group-Ab A)

left-zero-law-Ab :
  {l : Level} (A : Ab l) → (x : type-Ab A) →
  Id (add-Ab A (zero-Ab A) x) x
left-zero-law-Ab A = left-unit-law-Group (group-Ab A)

right-zero-law-Ab :
  {l : Level} (A : Ab l) → (x : type-Ab A) →
  Id (add-Ab A x (zero-Ab A)) x
right-zero-law-Ab A = right-unit-law-Group (group-Ab A)

has-negatives-Ab :
  {l : Level} (A : Ab l) → is-group' (semi-group-Ab A) (has-zero-Ab A)
has-negatives-Ab A = has-inverses-Group (group-Ab A)

neg-Ab :
  {l : Level} (A : Ab l) → type-Ab A → type-Ab A
neg-Ab A = inv-Group (group-Ab A)

left-negative-law-Ab :
  {l : Level} (A : Ab l) (x : type-Ab A) →
  Id (add-Ab A (neg-Ab A x) x) (zero-Ab A)
left-negative-law-Ab A = left-inverse-law-Group (group-Ab A)

right-negative-law-Ab :
  {l : Level} (A : Ab l) (x : type-Ab A) →
  Id (add-Ab A x (neg-Ab A x)) (zero-Ab A)
right-negative-law-Ab A = right-inverse-law-Group (group-Ab A)

is-commutative-add-Ab :
  {l : Level} (A : Ab l) (x y : type-Ab A) →
  Id (add-Ab A x y) (add-Ab A y x)
is-commutative-add-Ab A = pr2 A

{- So far the basic interface of abelian groups. -}

is-prop-is-abelian-Group :
  {l : Level} (G : Group l) → is-prop (is-abelian-Group G)
is-prop-is-abelian-Group G =
  is-prop-Π (λ x → is-prop-Π (λ y → is-set-type-Group G _ _))

{- Homomorphisms of abelian groups -}

preserves-add :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) →
  (type-Ab A → type-Ab B) → UU (l1 ⊔ l2)
preserves-add A B = preserves-mul (semi-group-Ab A) (semi-group-Ab B)

hom-Ab :
  {l1 l2 : Level} → Ab l1 → Ab l2 → UU (l1 ⊔ l2)
hom-Ab A B = hom-Group (group-Ab A) (group-Ab B)

map-hom-Ab :
  {l1 l2 : Level} (A : Ab l1) (B : Ab l2) →
  hom-Ab A B → type-Ab A → type-Ab B
map-hom-Ab A B = map-hom-Group (group-Ab A) (group-Ab B)

preserves-add-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) →
  ( f : hom-Ab A B) → preserves-add A B (map-hom-Ab A B f)
preserves-add-Ab A B f = preserves-mul-hom-Group (group-Ab A) (group-Ab B) f

{- We characterize the identity type of the abelian group homomorphisms. -}

htpy-hom-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2)
  ( f g : hom-Ab A B) → UU (l1 ⊔ l2)
htpy-hom-Ab A B f g = htpy-hom-Group (group-Ab A) (group-Ab B) f g

reflexive-htpy-hom-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) →
  ( f : hom-Ab A B) → htpy-hom-Ab A B f f
reflexive-htpy-hom-Ab A B f =
  reflexive-htpy-hom-Group (group-Ab A) (group-Ab B) f

htpy-hom-Ab-eq :
  {l1 l2 : Level} (A : Ab l1) (B : Ab l2) →
  (f g : hom-Ab A B) → Id f g → htpy-hom-Ab A B f g
htpy-hom-Ab-eq A B f g = htpy-hom-Group-eq (group-Ab A) (group-Ab B) f g

abstract
  is-contr-total-htpy-hom-Ab :
    { l1 l2 : Level} (A : Ab l1) (B : Ab l2) →
    ( f : hom-Ab A B) →
    is-contr (Σ (hom-Ab A B) (htpy-hom-Ab A B f))
  is-contr-total-htpy-hom-Ab A B f =
    is-contr-total-htpy-hom-Group (group-Ab A) (group-Ab B) f

abstract
  is-equiv-htpy-hom-Ab-eq :
    { l1 l2 : Level} (A : Ab l1) (B : Ab l2) →
    ( f g : hom-Ab A B) → is-equiv (htpy-hom-Ab-eq A B f g)
  is-equiv-htpy-hom-Ab-eq A B f g =
    is-equiv-htpy-hom-Group-eq (group-Ab A) (group-Ab B) f g

eq-htpy-hom-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) →
  { f g : hom-Ab A B} → htpy-hom-Ab A B f g → Id f g
eq-htpy-hom-Ab A B =
  eq-htpy-hom-Group (group-Ab A) (group-Ab B)

is-set-hom-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) →
  is-set (hom-Ab A B)
is-set-hom-Ab A B = is-set-hom-Group (group-Ab A) (group-Ab B)

preserves-add-id :
  {l : Level} (A : Ab l) → preserves-add A A id
preserves-add-id A = preserves-mul-id (semi-group-Ab A)

id-hom-Ab :
  { l1 : Level} (A : Ab l1) → hom-Ab A A
id-hom-Ab A = id-Group (group-Ab A)

comp-hom-Ab :
  { l1 l2 l3 : Level} (A : Ab l1) (B : Ab l2) (C : Ab l3) →
  ( hom-Ab B C) → (hom-Ab A B) → (hom-Ab A C)
comp-hom-Ab A B C =
  comp-Group (group-Ab A) (group-Ab B) (group-Ab C)

is-associative-comp-hom-Ab :
  { l1 l2 l3 l4 : Level} (A : Ab l1) (B : Ab l2) (C : Ab l3) (D : Ab l4) →
  ( h : hom-Ab C D) (g : hom-Ab B C) (f : hom-Ab A B) →
  Id (comp-hom-Ab A B D (comp-hom-Ab B C D h g) f)
     (comp-hom-Ab A C D h (comp-hom-Ab A B C g f))
is-associative-comp-hom-Ab A B C D =
  associative-Semi-Group
    ( semi-group-Ab A)
    ( semi-group-Ab B)
    ( semi-group-Ab C)
    ( semi-group-Ab D)

left-unit-law-comp-hom-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2)
  ( f : hom-Ab A B) → Id (comp-hom-Ab A B B (id-hom-Ab B) f) f
left-unit-law-comp-hom-Ab A B =
  left-unit-law-Semi-Group (semi-group-Ab A) (semi-group-Ab B)

right-unit-law-comp-hom-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2)
  ( f : hom-Ab A B) → Id (comp-hom-Ab A A B f (id-hom-Ab A)) f
right-unit-law-comp-hom-Ab A B =
  right-unit-law-Semi-Group (semi-group-Ab A) (semi-group-Ab B)

{- Isomorphisms of abelian groups -}

is-iso-hom-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) →
  ( f : hom-Ab A B) → UU (l1 ⊔ l2)
is-iso-hom-Ab A B =
  is-iso-hom-Semi-Group (semi-group-Ab A) (semi-group-Ab B)

inv-is-iso-hom-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) (f : hom-Ab A B) →
  is-iso-hom-Ab A B f → hom-Ab B A
inv-is-iso-hom-Ab A B f = pr1

map-inv-is-iso-hom-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) (f : hom-Ab A B) →
  is-iso-hom-Ab A B f → type-Ab B → type-Ab A
map-inv-is-iso-hom-Ab A B f is-iso-f =
  map-hom-Ab B A (inv-is-iso-hom-Ab A B f is-iso-f)

is-sec-inv-is-iso-hom-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) (f : hom-Ab A B) →
  ( is-iso-f : is-iso-hom-Ab A B f) →
  Id (comp-hom-Ab B A B f (inv-is-iso-hom-Ab A B f is-iso-f)) (id-hom-Ab B)
is-sec-inv-is-iso-hom-Ab A B f is-iso-f = pr1 (pr2 is-iso-f)

is-sec-map-inv-is-iso-hom-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) (f : hom-Ab A B) →
  ( is-iso-f : is-iso-hom-Ab A B f) →
  ( (map-hom-Ab A B f) ∘ (map-hom-Ab B A (inv-is-iso-hom-Ab A B f is-iso-f))) ~
  id
is-sec-map-inv-is-iso-hom-Ab A B f is-iso-f =
  htpy-hom-Ab-eq B B
    ( comp-hom-Ab B A B f (inv-is-iso-hom-Ab A B f is-iso-f))
    ( id-hom-Ab B)
    ( is-sec-inv-is-iso-hom-Ab A B f is-iso-f)

is-retr-inv-is-iso-hom-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) (f : hom-Ab A B) →
  ( is-iso-f : is-iso-hom-Ab A B f) →
  Id (comp-hom-Ab A B A (inv-is-iso-hom-Ab A B f is-iso-f) f) (id-hom-Ab A)
is-retr-inv-is-iso-hom-Ab A B f is-iso-f = pr2 (pr2 is-iso-f)

is-retr-map-inv-is-iso-hom-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) (f : hom-Ab A B) →
  ( is-iso-f : is-iso-hom-Ab A B f) →
  ( (map-inv-is-iso-hom-Ab A B f is-iso-f) ∘ (map-hom-Ab A B f)) ~ id
is-retr-map-inv-is-iso-hom-Ab A B f is-iso-f =
  htpy-hom-Ab-eq A A
    ( comp-hom-Ab A B A (inv-is-iso-hom-Ab A B f is-iso-f) f)
    ( id-hom-Ab A)
    ( is-retr-inv-is-iso-hom-Ab A B f is-iso-f)

is-prop-is-iso-hom-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) (f : hom-Ab A B) →
  is-prop (is-iso-hom-Ab A B f)
is-prop-is-iso-hom-Ab A B f =
  is-prop-is-iso-hom-Semi-Group (semi-group-Ab A) (semi-group-Ab B) f

iso-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) → UU (l1 ⊔ l2)
iso-Ab A B = Σ (hom-Ab A B) (is-iso-hom-Ab A B)

hom-iso-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) →
  iso-Ab A B → hom-Ab A B
hom-iso-Ab A B = pr1

is-iso-hom-iso-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) →
  ( f : iso-Ab A B) → is-iso-hom-Ab A B (hom-iso-Ab A B f)
is-iso-hom-iso-Ab A B = pr2

inv-hom-iso-Ab :
  { l1 l2 : Level} (A : Ab l1) (B : Ab l2) →
  iso-Ab A B → hom-Ab B A
inv-hom-iso-Ab A B f =
  inv-is-iso-hom-Ab A B
    ( hom-iso-Ab A B f)
    ( is-iso-hom-iso-Ab A B f)

id-iso-Ab :
  {l1 : Level} (A : Ab l1) → iso-Ab A A
id-iso-Ab A = iso-id-Group (group-Ab A)

iso-eq-Ab :
  { l1 : Level} (A B : Ab l1) → Id A B → iso-Ab A B
iso-eq-Ab A .A refl = id-iso-Ab A

abstract
  equiv-iso-eq-Ab' :
    {l1 : Level} (A B : Ab l1) → Id A B ≃ iso-Ab A B
  equiv-iso-eq-Ab' A B =
    ( equiv-iso-eq-Group' (group-Ab A) (group-Ab B)) ∘e
    ( equiv-ap-pr1-is-subtype is-prop-is-abelian-Group {A} {B})

abstract
  is-contr-total-iso-Ab :
    { l1 : Level} (A : Ab l1) → is-contr (Σ (Ab l1) (iso-Ab A))
  is-contr-total-iso-Ab {l1} A =
    is-contr-equiv'
      ( Σ (Ab l1) (Id A))
      ( equiv-tot (equiv-iso-eq-Ab' A))
      ( is-contr-total-path A)

is-equiv-iso-eq-Ab :
  { l1 : Level} (A B : Ab l1) → is-equiv (iso-eq-Ab A B)
is-equiv-iso-eq-Ab A =
  fundamental-theorem-id A
    ( id-iso-Ab A)
    ( is-contr-total-iso-Ab A)
    ( iso-eq-Ab A)

eq-iso-Ab :
  { l1 : Level} (A B : Ab l1) → iso-Ab A B → Id A B
eq-iso-Ab A B = inv-is-equiv (is-equiv-iso-eq-Ab A B)

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
module Empty where

  record ⊤ : Set where
    constructor tt

  data ⊥ : Set where

  {-# IMPORT Data.FFI #-}
  {-# COMPILED_DATA ⊥ Data.FFI.AgdaEmpty #-}

  absurd : ∀ { A : Set } → ⊥ → A
  absurd ()

ext: agda

max_stars_repo_name: cantsin/agda-experiments

max_issues_repo_name: cantsin/agda-experiments

max_forks_repo_name: cantsin/agda-experiments


text:
------------------------------------------------------------------------------
-- First-Order Theory of Combinators (FOTC)
------------------------------------------------------------------------------

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

-- Code accompanying the paper "Combining Interactive and Automatic
-- Reasoning in First Order Theories of Functional Programs" by Ana
-- Bove, Peter Dybjer and Andrés Sicard-Ramírez (FoSSaCS 2012).

-- The code presented here does not match the paper exactly.

module FOTC.README where

------------------------------------------------------------------------------
-- Description

-- Verification of functional programs using a version of Azcel's
-- First-Order Theory of Combinators and showing the combination of
-- interactive proofs with automatics proofs carried out by
-- first-order automatic theorem provers (ATPs).

------------------------------------------------------------------------------
-- For the paper, prerequisites, tested versions of the ATPs and use,
-- see https://github.com/asr/fotc/.

------------------------------------------------------------------------------
-- Conventions

-- If the module's name ends in 'I' the module contains interactive
-- proofs, if it ends in 'ATP' the module contains combined proofs,
-- otherwise the module contains definitions and/or interactive proofs
-- that are used by the interactive and combined proofs.

------------------------------------------------------------------------------
-- Base axioms
open import FOTC.Base

-- Properties for the base axioms

open import FOTC.Base.PropertiesATP
open import FOTC.Base.PropertiesI

-- Axioms for lists, colists, streams, etc.
open import FOTC.Base.List

-- Properties for axioms for lists, colists, streams, etc
open import FOTC.Base.List.PropertiesATP
open import FOTC.Base.List.PropertiesI

------------------------------------------------------------------------------
-- Booleans

-- The axioms
open import FOTC.Data.Bool

-- The inductive predicate
open import FOTC.Data.Bool.Type

-- Properties
open import FOTC.Data.Bool.PropertiesATP
open import FOTC.Data.Bool.PropertiesI

------------------------------------------------------------------------------
-- Natural numbers

-- The axioms
open import FOTC.Data.Nat

-- The inductive predicate
open import FOTC.Data.Nat.Type

-- Properties
open import FOTC.Data.Nat.PropertiesATP
open import FOTC.Data.Nat.PropertiesI

open import FOTC.Data.Nat.PropertiesByInductionATP
open import FOTC.Data.Nat.PropertiesByInductionI

-- Divisibility relation
open import FOTC.Data.Nat.Divisibility.By0.PropertiesATP
open import FOTC.Data.Nat.Divisibility.By0.PropertiesI
open import FOTC.Data.Nat.Divisibility.NotBy0.PropertiesATP
open import FOTC.Data.Nat.Divisibility.NotBy0.PropertiesI

-- Induction
open import FOTC.Data.Nat.Induction.Acc.WF-I
open import FOTC.Data.Nat.Induction.NonAcc.LexicographicI

-- Inequalites
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesATP
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesI
open import FOTC.Data.Nat.Inequalities.PropertiesATP
open import FOTC.Data.Nat.Inequalities.PropertiesI

-- Unary numbers
open import FOTC.Data.Nat.UnaryNumbers.Inequalities.PropertiesATP
open import FOTC.Data.Nat.UnaryNumbers.TotalityATP

------------------------------------------------------------------------------
-- Lists

-- The axioms
open import FOTC.Data.List

-- The inductive predicate
open import FOTC.Data.List.Type

-- Properties
open import FOTC.Data.List.PropertiesATP
open import FOTC.Data.List.PropertiesI

-- Well-founded induction
open import FOTC.Data.List.WF-Relation.LT-Cons.Induction.Acc.WF-I
open import FOTC.Data.List.WF-Relation.LT-Cons.PropertiesI
open import FOTC.Data.List.WF-Relation.LT-Length.Induction.Acc.WF-I
open import FOTC.Data.List.WF-Relation.LT-Length.PropertiesI

------------------------------------------------------------------------------
-- Lists of natural numbers

-- The inductive predicate
open import FOTC.Data.Nat.List

-- Properties
open import FOTC.Data.Nat.List.PropertiesATP
open import FOTC.Data.Nat.List.PropertiesI

------------------------------------------------------------------------------
-- Co-inductive natural numbers

-- Some axioms
open import FOTC.Data.Conat

-- The co-inductive predicate
open import FOTC.Data.Conat.Type

-- Properties
open import FOTC.Data.Conat.PropertiesATP
open import FOTC.Data.Conat.PropertiesI

-- Equality
open import FOTC.Data.Conat.Equality.Type

-- Equality properties
open import FOTC.Data.Conat.Equality.PropertiesATP
open import FOTC.Data.Conat.Equality.PropertiesI

------------------------------------------------------------------------------
-- Streams

-- Some axioms
open import FOTC.Data.Stream

-- The co-inductive predicate
open import FOTC.Data.Stream.Type

-- Properties
open import FOTC.Data.Stream.PropertiesATP
open import FOTC.Data.Stream.PropertiesI

-- Equality properties
open import FOTC.Data.Stream.Equality.PropertiesATP
open import FOTC.Data.Stream.Equality.PropertiesI

------------------------------------------------------------------------------
-- Bisimilary relation

-- The co-inductive predicate
open import FOTC.Relation.Binary.Bisimilarity.Type

-- Properties
open import FOTC.Relation.Binary.Bisimilarity.PropertiesATP
open import FOTC.Relation.Binary.Bisimilarity.PropertiesI

------------------------------------------------------------------------------
-- Verification of programs

-- Burstall's sort list algorithm: A structurally recursive algorithm
open import FOTC.Program.SortList.CorrectnessProofATP
open import FOTC.Program.SortList.CorrectnessProofI

-- The division algorithm: A non-structurally recursive algorithm
open import FOTC.Program.Division.CorrectnessProofATP
open import FOTC.Program.Division.CorrectnessProofI

-- The GCD algorithm: A non-structurally recursive algorithm
open import FOTC.Program.GCD.Partial.CorrectnessProofATP
open import FOTC.Program.GCD.Partial.CorrectnessProofI
open import FOTC.Program.GCD.Total.CorrectnessProofATP
open import FOTC.Program.GCD.Total.CorrectnessProofI

-- The nest function: A very simple function with nested recursion
open import FOTC.Program.Nest.PropertiesATP

-- The McCarthy 91 function: A function with nested recursion
open import FOTC.Program.McCarthy91.PropertiesATP

-- The mirror function: A function with higher-order recursion
open import FOTC.Program.Mirror.PropertiesATP
open import FOTC.Program.Mirror.PropertiesI

-- The map-iterate property: A property using co-induction
open import FOTC.Program.MapIterate.MapIterateATP
open import FOTC.Program.MapIterate.MapIterateI

-- The alternating bit protocol: A program using induction and co-induction
open import FOTC.Program.ABP.CorrectnessProofATP
open import FOTC.Program.ABP.CorrectnessProofI

-- The iter₀ function: A partial function
open import FOTC.Program.Iter0.PropertiesATP
open import FOTC.Program.Iter0.PropertiesI

-- The Collatz function: A function without a termination proof
open import FOTC.Program.Collatz.PropertiesATP
open import FOTC.Program.Collatz.PropertiesI

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module OutsideIn.Prelude where

  open import Data.Nat public
  open import Relation.Binary.PropositionalEquality public renaming ([_] to iC)
  open import Relation.Nullary public
  open import Function public hiding (case_of_)

  cong₃ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
          (f : A → B → C → D) {x y u v x′ y′} → x ≡ y → u ≡ v → x′ ≡ y′
        → f x u x′ ≡ f y v y′
  cong₃ f refl refl refl = refl

  cong₄ : ∀ {a b c d e} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {E : Set e}
          (f : A → B → C → D → E) {x y u v x′ y′ u′ v′} → x ≡ y → u ≡ v → x′ ≡ y′ → u′ ≡ v′
        → f x u x′ u′ ≡ f y v y′ v′
  cong₄ f refl refl refl refl = refl

  import Level

  postulate extensionality : Extensionality Level.zero Level.zero

  module Shapes where

    -- Used throughout to show structure preserving operations preserve structure,
    -- in order to maintain structural recursion.
    data Shape : Set where
      Nullary : Shape
      Unary : Shape → Shape
      Binary : Shape → Shape → Shape

  module Functors where

    import Data.Vec as V
    open V using (_∷_; Vec; [])

    isIdentity : ∀ {A} → (A → A) → Set
    isIdentity {A} f = ∀ {x} → f x ≡ x

    id-is-id : ∀ {A} → isIdentity {A} id
    id-is-id = refl
    record Functor (X : Set → Set) : Set₁ where
      field map : ∀ {A B} → (A → B) → X A → X B
      _<$>_ : ∀ {A B} → (A → B) → X A → X B
      _<$>_ = map
      field identity : ∀ {A : Set}{f : A → A} → isIdentity f → isIdentity (map f)
      field composite : ∀ {A B C : Set} {f : A → B} {g : B → C}
                      → {x : X A} → ( (g ∘ f) <$> x ≡ g <$> (f <$> x))

    Pointed :  (Set → Set) → Set₁
    Pointed X = ∀ {a} → a → X a

    id-is-functor : Functor id
    id-is-functor = record { map = id; identity = id; composite = refl }

    vec-is-functor : ∀ {n} → Functor (λ A → Vec A n)
    vec-is-functor {n} = record { map = V.map; identity = ident {n} ; composite = composite }
      where ident :  {n : ℕ}{A : Set} {f : A → A} → isIdentity f →{x : Vec A n} → V.map f x ≡ x
            ident isid {[]} = refl
            ident isid {x ∷ xs} = cong₂ _∷_ isid (ident isid)
            composite : {A B C : Set}{n : ℕ} {f : A → B} {g : B → C} {x : Vec A n}
                      → V.map (g ∘ f) x ≡ V.map g (V.map f x)
            composite {x = []} = refl
            composite {x = x ∷ xs} = cong₂ _∷_ refl composite
    private
      module F = Functor ⦃ ... ⦄

    combine-composite′ : {X Y : Set → Set}{A B C : Set} ⦃ F2 : Functor Y ⦄
                        {V : X (Y A)}{f : A → B}{g : B → C}
                      → (f1map  : ∀ {a b} → (a → b) → (X a → X b))
                      → (f1comp :  f1map (F.map g ∘ F.map f) V
                                ≡  f1map (F.map g) (f1map (F.map f) V))
                      → f1map (F.map ⦃ F2 ⦄ (g ∘ f)) V
                      ≡ f1map (F.map ⦃ F2 ⦄ g) (f1map (F.map ⦃ F2 ⦄ f) V)
    combine-composite′ ⦃ F2 ⦄ {V} f1map f1comp = trans (cong (λ t → f1map t V)
                                                      (extensionality (λ x → F.composite ⦃ F2 ⦄)))
                                                 f1comp

    combine-composite : {X Y : Set → Set}{A B C : Set} ⦃ F1 : Functor X ⦄ ⦃ F2 : Functor Y ⦄
                        {V : X (Y A)}{f : A → B}{g : B → C}
                      → F.map ⦃ F1 ⦄ (F.map ⦃ F2 ⦄ (g ∘ f)) V
                      ≡ F.map ⦃ F1 ⦄ (F.map ⦃ F2 ⦄ g) (F.map ⦃ F1 ⦄ (F.map ⦃ F2 ⦄ f) V)
    combine-composite {X}{Y} ⦃ F1 ⦄ ⦃ F2 ⦄ {V} = combine-composite′ {X}{Y}
                                                                    (F.map ⦃ F1 ⦄)
                                                                    (F.composite ⦃ F1 ⦄)
    infixr 6 _∘f_
    _∘f_ : {X Y : Set → Set} → ( F1 : Functor X )( F2 : Functor Y )
                                    → Functor (X ∘ Y)
    F1 ∘f F2 = record { map = F.map ⦃ F1 ⦄ ∘ F.map ⦃ F2 ⦄
                      ; composite = combine-composite ⦃ F1 ⦄ ⦃ F2 ⦄
                      ; identity = F.identity ⦃ F1 ⦄ ∘ F.identity ⦃ F2 ⦄
                      }

  module StupidEquality where
    open import Data.Bool public using (Bool; true; false)
    -- This equality doesn't place any proof demands
    -- because we don't actually care what equality is used.
    -- This is just for the initial base of type variables, where the user provides
    -- their own type equality relation. We don't care if it says Int ∼ Bool - this just
    -- provides a way for users to get some equality information threaded through the
    -- simplifier
    Eq : Set → Set
    Eq X = ∀ (a b : X) → Bool

  module Monads where
    open Functors

    record Monad (X : Set → Set) : Set₁ where
      field ⦃ is-functor ⦄ : Functor X
      field ⦃ point ⦄ : Pointed X
      open Functor is-functor
      field join : ∀ {a} → X (X a) → X a
      unit : ∀ {a} → a → X a
      unit = point
      _>>=_ : ∀ {a b} → X a → (a → X b) → X b
      _>>=_ a b = join (b <$> a)
      _>>_ : ∀ {a b} → X a → X b → X b
      _>>_ a b = a >>= λ _ → b
      _>=>_ : ∀ {a b c : Set} → (b → X c) → (a → X b) → (a → X c)
      _>=>_ a b = λ v → b v >>= a
      field is-left-ident : ∀ {a b}{x : a → X b}{v} → (point >=> x) v ≡ x v
      field is-right-ident : ∀ {a b}{x : a → X b}{v} → (x >=> point) v ≡ x v
      field >=>-assoc : ∀{p}{q}{r}{s}{a : r → X s}{b : q → X r} {c : p → X q}{v}
                      → (a >=> (b >=> c)) v ≡ ((a >=> b) >=> c) v

      abstract
        <$>-unit : ∀ {A B}{g : A → B}{x} → g <$> (unit x) ≡  unit (g x)
        <$>-unit {A}{B}{g}{x} = begin
          g <$> (unit x)                         ≡⟨ sym (is-left-ident {x = _<$>_ g}) ⟩
          join (unit <$> (g <$> (unit x)))       ≡⟨ cong join (sym (composite)) ⟩
          join ((λ x → unit (g x)) <$> (unit x)) ≡⟨ is-right-ident ⟩
          unit (g x)                             ∎
         where open ≡-Reasoning

      abstract
        <$>-bind : ∀ {A B C}{f : A → B}{g : B → X C}{x : X A}
                 → (f <$> x) >>= g ≡ x >>= (λ z → g (f z))
        <$>-bind = cong join (sym (composite))

        natural-trans : ∀ {A B}{f : A → B}{x : X( X A)} → f <$> (join x) ≡ join ((_<$>_ f) <$> x)
        natural-trans {A}{B}{f}{x} = begin
           f <$> (join x)                                  ≡⟨ sym (is-left-ident {x = _<$>_ f}) ⟩
           join (unit <$> (f <$> (join x)))                ≡⟨ † ⟩
           join (unit <$> (f <$> (join (id <$> x))))       ≡⟨ <$>-bind ⟩
           join ((λ v → unit (f v)) <$> (join (id <$> x))) ≡⟨ >=>-assoc { c = λ _ → x}{0} ⟩
           join ((λ x → join ((unit ∘ f) <$> x)) <$> x )   ≡⟨ sym (<$>-bind) ⟩
           ((_<$>_ (λ y → unit (f y))) <$> x ) >>= join    ≡⟨ <$>-bind ⟩
           x >>= (λ x → x >>= (λ y → unit (f y)))          ≡⟨ * ⟩
           join ((_<$>_ f) <$> x)                          ∎
          where open ≡-Reasoning
                † : join (unit <$> (f <$> (join x))) ≡ join (unit <$> (f <$> (join (id <$> x))))
                † = cong (λ t → join (unit <$> (f <$> join t))) (sym (identity id-is-id ))
                * : x >>= (λ x → x >>= (λ y → unit (f y))) ≡ join ((_<$>_ f) <$> x)
                * = cong (_>>=_ x)
                         (extensionality (λ y → trans (sym <$>-bind)
                                                      (is-left-ident {x = _<$>_ f}{v = y})))

    id-is-monad : Monad id
    id-is-monad = record { is-functor = id-is-functor
                         ; point = id
                         ; join = id
                         ; >=>-assoc = refl
                         ; is-left-ident = refl
                         ; is-right-ident = refl
                         }

    record MonadHomomorphism {M₁ M₂ : Set → Set}(h : ∀ {x : Set} → M₁ x → M₂ x)
                             ⦃ M₁-m : Monad M₁ ⦄ ⦃ M₂-m : Monad M₂ ⦄ : Set₁ where
      open Monad M₁-m using () renaming (unit to unit₁; join to join₁; is-functor to is-functor₁)
      open Monad M₂-m using () renaming (unit to unit₂; join to join₂; is-functor to is-functor₂)
      open Functor is-functor₁ using () renaming (map to map₁)
      open Functor is-functor₂ using () renaming (map to map₂)
      field h-return :  ∀ {A}{x : A} → h (unit₁ x) ≡ unit₂ x
      field h-fmap : {A B : Set} {f : A → B} {x : M₁ A}
                     → h (map₁ f x) ≡ map₂ f (h x)
      field h-join : ∀{τ}{x : M₁ (M₁ τ)} → h (join₁ x) ≡ join₂ (h (map₁ h x))

    record MonadTrans (X : (Set → Set) → Set → Set) : Set₁ where
      field produces-monad : ∀ {m} → Monad m → Monad (X m)
      field lift : ∀ {m}⦃ mm : Monad m ⦄{a} → m a → X m a
      field is-homomorphism : ∀ {m} → (mm : Monad m)
                            → MonadHomomorphism {m} {X m} (lift {m}) ⦃ mm ⦄ ⦃ produces-monad mm ⦄

  module Ⓢ-Type where
    open Functors
    open Monads
    open StupidEquality

    data Ⓢ (τ : Set) : Set where
      suc : τ → Ⓢ τ
      zero : Ⓢ τ

    cata-Ⓢ : {a b : Set} → b → (a → b) → Ⓢ a → b
    cata-Ⓢ nil something zero = nil
    cata-Ⓢ nil something (suc n) = something n

    sequence-Ⓢ : ∀ {m}{b} → ⦃ monad : Monad m ⦄ →  Ⓢ (m b) → m (Ⓢ b)
    sequence-Ⓢ ⦃ m ⦄ (suc n) = map suc n
      where open Functor (Monad.is-functor m)
    sequence-Ⓢ ⦃ m ⦄ (zero) = unit zero
      where open Monad (m)

    private
      fmap-Ⓢ : ∀ {a b} → (a → b) → Ⓢ a → Ⓢ b
      fmap-Ⓢ f zero = zero
      fmap-Ⓢ f (suc n) = suc (f n)
      abstract
        fmap-Ⓢ-id : ∀ {A} → {f : A → A}
                   → isIdentity f → isIdentity (fmap-Ⓢ f)
        fmap-Ⓢ-id isid {zero} = refl
        fmap-Ⓢ-id isid {suc x} = cong suc isid

        fmap-Ⓢ-comp : ∀ {A B C : Set} {f : A → B} {g : B → C} → ∀ {x}
                     → fmap-Ⓢ (g ∘ f) x ≡ fmap-Ⓢ g (fmap-Ⓢ f x)
        fmap-Ⓢ-comp {x = zero} = refl
        fmap-Ⓢ-comp {x = suc n} = refl

    Ⓢ-is-functor : Functor Ⓢ
    Ⓢ-is-functor = record { map = fmap-Ⓢ
                           ; identity = fmap-Ⓢ-id
                           ; composite = fmap-Ⓢ-comp
                           }

    Ⓢ-eq : ∀ {x} → Eq x → Eq (Ⓢ x)
    Ⓢ-eq x zero zero = true
    Ⓢ-eq x (suc n) zero = false
    Ⓢ-eq x zero (suc m) = false
    Ⓢ-eq x (suc n) (suc m) = x n m

    private
      join-Ⓢ : ∀ {x} → Ⓢ (Ⓢ x) → Ⓢ x
      join-Ⓢ (zero) = zero
      join-Ⓢ (suc τ) = τ

      test-join : ∀ {A B}{f : A → B}{x : Ⓢ( Ⓢ A)}
                → fmap-Ⓢ f (join-Ⓢ x) ≡ join-Ⓢ (fmap-Ⓢ (fmap-Ⓢ f) x)
      test-join {x = zero} = refl
      test-join {x = suc n} = refl

    Ⓢ-is-monad : Monad Ⓢ
    Ⓢ-is-monad = record { is-functor     = Ⓢ-is-functor
                         ; point          = suc
                         ; join           = join-Ⓢ
                         ; is-left-ident  = left-id
                         ; is-right-ident = refl
                         ; >=>-assoc        = λ { {c = c}{v} → assoc {τ = c v} }
                         }
        where
          left-id : ∀ {τ : Set}{v : Ⓢ τ} → join-Ⓢ (fmap-Ⓢ suc v) ≡ v
          left-id {v = zero } = refl
          left-id {v = suc v} = refl
          assoc : ∀ {q r s : Set} {a : r → Ⓢ s} {b : q → Ⓢ r}{τ : Ⓢ q}
                → join-Ⓢ (fmap-Ⓢ a (join-Ⓢ (fmap-Ⓢ b τ)))
                ≡ join-Ⓢ (fmap-Ⓢ (λ v′ → join-Ⓢ (fmap-Ⓢ  a (b v′))) τ)
          assoc {τ = zero} = refl
          assoc {τ = suc v} = refl

    Ⓢ-Trans : (Set → Set) → Set → Set
    Ⓢ-Trans m x = m (Ⓢ x)

    private
      lift : ∀ {m : Set → Set}⦃ mm : Monad m ⦄{x} → m x → m (Ⓢ x)
      lift {m}⦃ mm ⦄{x} v = suc <$> v
        where open Monad mm
              open Functor is-functor

      module MonadProofs {m : Set → Set}⦃ mm : Monad m ⦄ where
        open Monad mm
        open Functor is-functor
        functor : Functor (Ⓢ-Trans m)
        functor = record { map = λ f v → (fmap-Ⓢ f) <$> v
                         ; identity = λ p → identity (fmap-Ⓢ-id p)
                         ; composite = λ { {x = x} → trans (cong (λ t → t <$> x)
                                                           (extensionality ext)) composite }
                         }
          where open ≡-Reasoning
                ext : ∀ {A B C : Set} {f : A → B} {g : B → C} → (x' : Ⓢ A)
                    → fmap-Ⓢ (g ∘ f) x' ≡ (fmap-Ⓢ g ∘ fmap-Ⓢ f) x'
                ext (zero) = refl
                ext (suc n) = refl

        module Trans = Functor functor

        private
          cata-Ⓢ-u0 : ∀ {a b} → (a → m (Ⓢ b)) → Ⓢ a → m (Ⓢ b)
          cata-Ⓢ-u0 = cata-Ⓢ (unit zero)
        abstract
          right-id :  {a b : Set} {x : a → Ⓢ-Trans m b} {v : a}
                   → Trans.map x (lift {m} (unit v)) >>= cata-Ⓢ-u0 id ≡ x v
          right-id {a}{b}{x}{v} = begin
            Trans.map x (suc <$> (unit v)) >>= cata-Ⓢ-u0 id ≡⟨ * ⟩
            (fmap-Ⓢ x <$> (unit (suc v))) >>= cata-Ⓢ-u0 id ≡⟨ † ⟩
            join (cata-Ⓢ-u0 id <$> (unit (suc (x v))))      ≡⟨ cong join <$>-unit ⟩
            join (unit (x v))                                ≡⟨ cong join (sym(identity id-is-id)) ⟩
            join (id <$> unit (x v))                         ≡⟨ is-right-ident {x = id} ⟩
            x v                                              ∎
           where open ≡-Reasoning
                 * : Trans.map x (suc <$> (unit v)) >>= cata-Ⓢ-u0 id
                   ≡ (fmap-Ⓢ x <$> (unit (suc v))) >>= cata-Ⓢ-u0 id
                 * = cong (λ t → Trans.map x t >>= cata-Ⓢ-u0 id) <$>-unit
                 † : (fmap-Ⓢ x <$> (unit (suc v))) >>= cata-Ⓢ-u0 id
                   ≡ join (cata-Ⓢ-u0 id <$> (unit (suc (x v))))
                 † = cong (λ x → x >>= cata-Ⓢ-u0 id) <$>-unit

          left-id : {b : Set} {t : Ⓢ-Trans m b}
                  → Trans.map (λ x' → lift {m} (unit x')) t >>= cata-Ⓢ-u0 id ≡ t
          left-id {b}{t} = trans <$>-bind (subst (λ q → t >>= q ≡ t)
                                                 (sym (extensionality h≗unit))
                                                 (is-left-ident {x = λ _ → t} {v = 0}))
            where h : ∀ {A} → Ⓢ A → m (Ⓢ A)
                  h x = cata-Ⓢ-u0 id (fmap-Ⓢ (λ x' → suc <$> (unit x')) x)
                  h≗unit : ∀ {A} → h {A} ≗ unit
                  h≗unit zero = refl
                  h≗unit (suc y) = <$>-unit

          assoc : ∀ {p q r s : Set}
                    {a : r → Ⓢ-Trans m s}{b : q → Ⓢ-Trans m r}{c : p → Ⓢ-Trans m q}
                    {v : p}
                → Trans.map a (Trans.map b (c v) >>= cata-Ⓢ-u0 id) >>= cata-Ⓢ-u0 id
                ≡ Trans.map (λ v' → Trans.map a (b v') >>= cata-Ⓢ-u0 id) (c v) >>= cata-Ⓢ-u0 id
          assoc {p}{q}{r}{s}{a}{b}{c}{v}
            = let
                †₀ = cata-fmap
                †₁ = cong (λ x → x >>= cata-Ⓢ (unit zero) a) cata-fmap
                †₂ = >=>-assoc {c = λ _ → c v} {v = 0}
                †₃ = cong (_>>=_ (c v)) (extensionality ext)
                †₄ = cong (λ x → c v >>= cata-Ⓢ (unit zero) x)
                          (extensionality (λ x → sym cata-fmap))
                †₅ = sym (cata-fmap)
              in begin
                 Trans.map a (Trans.map b (c v) >>= cata-Ⓢ-u0 id) >>= cata-Ⓢ-u0 id ≡⟨ †₀ ⟩
                 ((fmap-Ⓢ b <$> c v) >>= cata-Ⓢ-u0 id) >>= cata-Ⓢ-u0 a            ≡⟨ †₁ ⟩
                 (c v >>= cata-Ⓢ-u0 b) >>= cata-Ⓢ-u0 a                             ≡⟨ †₂ ⟩
                 c v >>= (λ cv → cata-Ⓢ-u0 b cv >>= cata-Ⓢ-u0 a)                   ≡⟨ †₃ ⟩
                 c v >>= cata-Ⓢ-u0 (λ v' → b v' >>= cata-Ⓢ-u0 a)                   ≡⟨ †₄ ⟩
                 c v >>= cata-Ⓢ-u0 (λ v' → (fmap-Ⓢ a <$> b v') >>= cata-Ⓢ-u0 id)  ≡⟨ †₅ ⟩
                 Trans.map (λ v' → Trans.map a (b v') >>= cata-Ⓢ-u0 id) (c v) >>= cata-Ⓢ-u0 id ∎
           where open ≡-Reasoning
                 ext : (x : Ⓢ q) → cata-Ⓢ-u0 b x >>= cata-Ⓢ-u0 a
                                  ≡ cata-Ⓢ-u0 (λ v' → b v' >>= cata-Ⓢ-u0 a) x
                 ext zero = begin
                   join ((cata-Ⓢ-u0 a) <$> unit zero) ≡⟨ cong join <$>-unit ⟩
                   join (unit (unit zero))             ≡⟨ cong join (sym (identity id-is-id)) ⟩
                   join (id <$> unit (unit zero))      ≡⟨ is-right-ident ⟩
                   unit zero                           ∎
                 ext (suc n) = refl
                 cata-fmap : ∀{A B C}{a : A → B}{x : m (Ⓢ A)}{n : m C}{j : B → m C}
                           → (fmap-Ⓢ a <$> x) >>= cata-Ⓢ n j ≡ x >>= cata-Ⓢ n (λ x → j ( a x))
                 cata-fmap {A}{B}{C}{a}{x}{n}{j} = trans <$>-bind
                                                         (cong (_>>=_ x) (extensionality ext′))
                  where ext′ : (x' : Ⓢ A) → cata-Ⓢ n j (fmap-Ⓢ a x')
                                           ≡ cata-Ⓢ n (λ x0 → j (a x0)) x'
                        ext′ zero = refl
                        ext′ (suc n) = refl
        produces-monad = record { point = λ x → lift ⦃ mm ⦄ (unit x)
                                ; is-functor = functor
                                ; join = λ v → v >>= cata-Ⓢ (unit zero) id
                                ; is-left-ident = left-id
                                ; is-right-ident = right-id
                                ; >=>-assoc = λ {_}{_}{_}{_}{a}{b}{c}{v}
                                            → assoc {a = a}{b}{c}{v}
                                }

      module HomomorphismProofs {m : Set → Set}⦃ mm : Monad m ⦄ where
        open Monad mm
        open Functor is-functor
        open ≡-Reasoning

        cata-Ⓢ-u0 : ∀ {a b} → (a → m (Ⓢ b)) → Ⓢ a → m (Ⓢ b)
        cata-Ⓢ-u0 = cata-Ⓢ (unit zero)

        fmap-p : ∀ {A B : Set} {f : A → B} {x}
               → lift {m} (f <$> x) ≡ (fmap-Ⓢ f) <$> (lift {m} x)
        fmap-p {A}{B}{f}{x} =  begin
          suc <$> (f <$> x)               ≡⟨ sym (composite) ⟩
          (λ t → suc (f t)) <$> x         ≡⟨ refl ⟩
          (λ t → fmap-Ⓢ f (suc t)) <$> x ≡⟨ composite ⟩
          (fmap-Ⓢ f) <$> (suc <$> x)     ∎

        join-p : ∀{τ}{x : m (m (τ))}
               → suc <$> (join x) ≡ (suc <$> (_<$>_ suc <$> x)) >>= cata-Ⓢ-u0 id
        join-p {_}{x} = begin
          suc <$> (join x)                                  ≡⟨ natural-trans ⟩
          join ((_<$>_ suc) <$> x)                          ≡⟨ refl ⟩
          x >>= (λ z → cata-Ⓢ-u0 id (suc (suc <$> z)))     ≡⟨ sym (<$>-bind) ⟩
          ((λ z → suc (suc <$> z)) <$> x) >>= cata-Ⓢ-u0 id ≡⟨ † ⟩
          (suc <$> (_<$>_ suc <$> x)) >>= cata-Ⓢ-u0 id     ∎
         where † = cong (λ x → x >>= cata-Ⓢ-u0 id) (composite)

        is-homomorphism : MonadHomomorphism (lift {m}) ⦃ mm ⦄ ⦃ MonadProofs.produces-monad ⦃ mm ⦄ ⦄
        is-homomorphism = record { h-return = refl
                                 ; h-fmap = fmap-p
                                 ; h-join = join-p
                                 }

    Ⓢ-Trans-is-trans : MonadTrans (Ⓢ-Trans)
    Ⓢ-Trans-is-trans = record { produces-monad = λ mm → MonadProofs.produces-monad ⦃ mm ⦄
                               ; lift = λ{m} → lift {m}
                               ; is-homomorphism = λ mm → HomomorphismProofs.is-homomorphism ⦃ mm ⦄
                               }

  module PlusN-Type where

    open Ⓢ-Type
    open Monads
    open Functors
    open StupidEquality

    PlusN : (n : ℕ) → Set → Set
    PlusN zero = id
    PlusN (suc n) = Ⓢ-Trans (PlusN n)

    PlusN-eq : ∀ {n}{x} → Eq x → Eq (PlusN n x)
    PlusN-eq {zero} eq = eq
    PlusN-eq {suc n} eq = PlusN-eq {n} (Ⓢ-eq eq)

    PlusN-is-monad : ∀ {n} → Monad (PlusN n)
    PlusN-is-monad {zero} = id-is-monad
    PlusN-is-monad {suc n} = MonadTrans.produces-monad Ⓢ-Trans-is-trans (PlusN-is-monad {n})

    _⨁_ = flip PlusN

    sequence-PlusN : ∀ {m}{n}{b} → ⦃ monad : Monad m ⦄ → (m b) ⨁ n → m (b ⨁ n)
    sequence-PlusN {n = zero} x = x
    sequence-PlusN {n = suc n} ⦃ m ⦄ x = sequence-PlusN {n = n}⦃ m ⦄
                                                        (PlusN-f.map (sequence-Ⓢ ⦃ m ⦄) x)
      where module PlusN-f = Functor (Monad.is-functor (PlusN-is-monad {n}))

    PlusN-collect : ∀ {n}{a b} → n ⨁ (a + b) ≡ (n ⨁ a) ⨁ b
    PlusN-collect {n}{zero} = refl
    PlusN-collect {n}{suc a}{b} = PlusN-collect {Ⓢ n}{a}{b}

  open Ⓢ-Type public
  open PlusN-Type public
  open Functors public
  open Monads public
  open Shapes public
  open StupidEquality public

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


text:
-- Internal error in coverage checker.
module Issue505 where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

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

data Split : Nat → Nat → Set where
  1x1 : Split (suc zero) (suc zero)
  _∣_ : ∀ {a b c} → Split a b → Split a c → Split a (b + c)
  _/_ : ∀ {a b c} → Split b a → Split c a → Split (b + c) a

data ⊤ : Set where
  tt : ⊤

theorem : ∀ {a b} → (split : Split a b) → ⊤
theorem 1x1 = tt
theorem {suc a} .{_} (l ∣ r) = tt
theorem {zero } .{_} (l ∣ r) = tt
theorem (l / r) = tt

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Structure.Setoid.Category.HomFunctor where

import      Functional as Fn
open import Function.Equals
open import Function.Equals.Proofs
open import Logic.Predicate
import      Lvl
open import Structure.Category
open import Structure.Category.Dual
open import Structure.Category.Functor.Contravariant
open import Structure.Category.Functor
open import Structure.Categorical.Properties
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Setoid
open import Syntax.Function
open import Syntax.Transitivity
open import Structure.Setoid.Category
open import Type

private variable ℓ ℓₒ ℓₘ ℓₑ : Lvl.Level

module _ (C : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}) where
  open CategoryObject(C)
  open Category ⦃ … ⦄
  open ArrowNotation
  private open module MorphismEquiv {x}{y} = Equivalence (Equiv-equivalence ⦃ morphism-equiv{x}{y} ⦄) using ()

  covariantHomFunctor : Object → (C →ᶠᵘⁿᶜᵗᵒʳ setoidCategoryObject)
  ∃.witness (covariantHomFunctor x) y = [∃]-intro (x ⟶ y)
  Functor.map (∃.proof (covariantHomFunctor _)) f = [∃]-intro (f ∘_) ⦃ BinaryOperator.right binaryOperator ⦄
  _⊜_.proof (Function.congruence (Functor.map-function (∃.proof (covariantHomFunctor _))) {f₁} {f₂} f₁f₂) {g} =
    f₁ ∘ g 🝖-[ congruence₂ₗ(_∘_) g f₁f₂ ]
    f₂ ∘ g 🝖-end
  _⊜_.proof (Functor.op-preserving (∃.proof (covariantHomFunctor _)) {f = f} {g = g}) {h} =
    (f ∘ g) ∘ h            🝖[ _≡_ ]-[ Morphism.associativity(_∘_) ]
    f ∘ (g ∘ h)            🝖[ _≡_ ]-[]
    ((f ∘_) Fn.∘ (g ∘_)) h 🝖-end
  _⊜_.proof (Functor.id-preserving (∃.proof (covariantHomFunctor _))) {f} =
    id ∘ f   🝖[ _≡_ ]-[ Morphism.identityₗ(_∘_)(id) ]
    f        🝖[ _≡_ ]-[]
    Fn.id(f) 🝖-end

  contravariantHomFunctor : Object → (C →ᶜᵒⁿᵗʳᵃᵛᵃʳⁱᵃⁿᵗᶠᵘⁿᶜᵗᵒʳ setoidCategoryObject)
  ∃.witness (contravariantHomFunctor x) y = [∃]-intro (y ⟶ x)
  Functor.map (∃.proof (contravariantHomFunctor _)) f = [∃]-intro (_∘ f) ⦃ BinaryOperator.left binaryOperator ⦄
  _⊜_.proof (Function.congruence (Functor.map-function (∃.proof (contravariantHomFunctor _))) {g₁} {g₂} g₁g₂) {f} =
    f ∘ g₁ 🝖-[ congruence₂ᵣ(_∘_) f g₁g₂ ]
    f ∘ g₂ 🝖-end
  _⊜_.proof (Functor.op-preserving (∃.proof (contravariantHomFunctor _)) {f = h} {g = g}) {f} =
    f ∘ (g ∘ h)            🝖[ _≡_ ]-[ Morphism.associativity(_∘_) ]-sym
    (f ∘ g) ∘ h            🝖[ _≡_ ]-[]
    ((_∘ h) Fn.∘ (_∘ g)) f 🝖-end
  _⊜_.proof (Functor.id-preserving (∃.proof (contravariantHomFunctor _))) {f} =
    f ∘ id   🝖[ _≡_ ]-[ Morphism.identityᵣ(_∘_)(id) ]
    f        🝖[ _≡_ ]-[]
    Fn.id(f) 🝖-end

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Any (◇) for containers
------------------------------------------------------------------------

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

module Data.Container.Relation.Unary.Any where

open import Level using (_⊔_)
open import Relation.Unary using (Pred; _⊆_)
open import Data.Product as Prod using (_,_; proj₂; ∃)
open import Function

open import Data.Container.Core hiding (map)
import Data.Container.Morphism as M

record ◇ {s p} (C : Container s p) {x ℓ} {X : Set x}
         (P : Pred X ℓ) (cx : ⟦ C ⟧ X) : Set (p ⊔ ℓ) where
  constructor any
  field proof : ∃ λ p → P (proj₂ cx p)

module _ {s₁ p₁ s₂ p₂} {C : Container s₁ p₁} {D : Container s₂ p₂}
         {x ℓ ℓ′} {X : Set x} {P : Pred X ℓ} {Q : Pred X ℓ′}
         where

  map : (f : C ⇒ D) → P ⊆ Q → ◇ D P ∘′ ⟪ f ⟫ ⊆ ◇ C Q
  map f P⊆Q (any (p , P)) .◇.proof = f .position p , P⊆Q P

module _ {s₁ p₁ s₂ p₂} {C : Container s₁ p₁} {D : Container s₂ p₂}
         {x ℓ} {X : Set x} {P : Pred X ℓ}
         where

  map₁ : (f : C ⇒ D) → ◇ D P ∘′ ⟪ f ⟫ ⊆ ◇ C P
  map₁ f = map f id

module _ {s p} {C : Container s p}
         {x ℓ ℓ′} {X : Set x} {P : Pred X ℓ} {Q : Pred X ℓ′}
         where

  map₂ : P ⊆ Q → ◇ C P ⊆ ◇ C Q
  map₂ = map (M.id C)


text:
module SystemF.Syntax.Term.Constructors where

open import Prelude hiding (⊥-elim)
open import SystemF.WellTyped
open import SystemF.Substitutions.Lemmas
open import SystemF.Substitutions
open import SystemF.Syntax.Type.Constructors

-- polymorphic function application
-- applies a polymorphic function to an argument with the type of the domain
poly-· : ∀ {ν n} {a : Type ν} {K : Ctx ν n} {f arg} →
         (fa : IsFunction a) → K ⊢ f ∈ a → K ⊢ arg ∈ domain fa → ∃ λ t → K ⊢ t ∈ codomain fa
poly-· (lambda a b) ⊢f ⊢arg = , ⊢f · ⊢arg
poly-· {K = K} {f = f} {arg = arg} (∀'-lambda {a} fa) ⊢f ⊢arg = , Λ (proj₂ (poly-· fa f' arg'))
  where
    f' : ctx-weaken K ⊢ _ ∈ a
    f' = subst
      (λ τ → ctx-weaken K ⊢ _ ∈ τ)
     (TypeLemmas.a-/Var-varwk↑-/-sub0≡a a)
      ((⊢tp-weaken ⊢f) [ tvar zero ])
    arg' : ctx-weaken K ⊢ (tm-weaken arg) [ tvar zero ] ∈ domain fa
    arg' = subst
      (λ τ → ctx-weaken K ⊢ _ ∈ τ)
      (TypeLemmas.a-/Var-varwk↑-/-sub0≡a (domain fa))
      ((⊢tp-weaken ⊢arg) [ tvar zero ])

-- Polymorphic identity function
id' : {ν n : ℕ} → Term ν n
id' = Λ (λ' (tvar zero) (var zero))

-- Bottom elimination/univeral property of the initial type
⊥-elim : ∀ {m n} → Type n → Term n m
⊥-elim a = λ' ⊥' ((var zero) [ a ])

-- Unit value
tt = id'

-- n-ary term abstraction
λⁿ : ∀ {ν m k} → Vec (Type ν) k → Term ν (k N+ m) → Term ν m
λⁿ []       t = t
λⁿ (a ∷ as) t = λⁿ as (λ' a t)

infixl 9 _·ⁿ_

-- n-ary term application
_·ⁿ_ : ∀ {m n k} → Term m n → Vec (Term m n) k → Term m n
s ·ⁿ []       = s
s ·ⁿ (t ∷ ts) = (s ·ⁿ ts) · t

-- Record/tuple constructor
newrec : ∀ {ν n k} → Vec (Term ν n) k → {as : Vec (Type ν) k} → Term ν n
newrec []                = tt
newrec (t ∷ ts) {a ∷ as} =
  Λ (λ' (map tp-weaken (a ∷ as) →ⁿ tvar zero)
    (var zero ·ⁿ map tmtm-weaken (map tm-weaken (t ∷ ts))))

-- Field access/projection
π : ∀ {ν n k} → Fin k → Term ν n → {as : Vec (Type ν) k} → Term ν n
π     () t {[]}
π {n = n} x  t {as} =
  (t [ lookup x as ]) · (λⁿ as (var (inject+ n x)))


text:
-- {-# OPTIONS -v interaction.give:30 -v interaction.scope:30 -v highlighting:50 -v auto:10 #-}
-- Andreas, 2014-07-05 and -08

module _ where

data Unit : Set where
  unit : Unit

auto : Unit
auto = {!!}  -- C-c C-a succeeds but then an error occurs during highlighting

-- Problem WAS:
-- Auto finds a solution, but then there is the error
-- Failed to parse expression in ?0

-- Should work now.

refine : Unit
refine = {!unit!}

-- Problem WAS: Highlighting after refine triggers an error.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module examplesPaperJFP.Sized where

open import Data.Product using (_×_; _,_)
open import Data.String

open import Function using (case_of_)
open import Size

open import examplesPaperJFP.NativeIOSafe
open import examplesPaperJFP.BasicIO using (IOInterface; Command; Response)
open import examplesPaperJFP.ConsoleInterface
open import examplesPaperJFP.Console using (translateIOConsoleLocal)
open import examplesPaperJFP.Object using (Interface; Method; Result;
  cellJ; CellMethod; get; put; CellResult)

module UnfoldF where
  open import examplesPaperJFP.Coalgebra using (F; mapF)
  record νF (i : Size) : Set where
    coinductive
    constructor delay
    field force : ∀(j : Size< i) → F (νF j)

  open νF using (force)

  unfoldF : ∀{S} (t : S → F S) → ∀ i → (S → νF i)
  force (unfoldF t i s) j = mapF (unfoldF t j) (t s)

mutual
  record IO (Iᵢₒ : IOInterface) (i : Size)  (A : Set) : Set where
    coinductive

    constructor delay
    field force : {j : Size< i} → IO′ Iᵢₒ j A

  data IO′ (Iᵢₒ : IOInterface) (i : Size)  (A : Set) : Set where
    exec′      :  (c : Command Iᵢₒ) (f : Response Iᵢₒ c → IO Iᵢₒ i A)  → IO′ Iᵢₒ i A
    return′  :  (a : A)                                              → IO′ Iᵢₒ i A

module NestedRecursion (Iᵢₒ : IOInterface) (A : Set) where

  data F (X : Set) : Set where
    exec′      :  (c : Command Iᵢₒ) (f : Response Iᵢₒ c → X)  → F X
    return′  :  (a : A)                                     → F X

  record νF (i : Size) : Set where
    coinductive
    constructor delay
    field force : {j : Size< i} → F (νF j)

open IO public

module _  {Iᵢₒ : IOInterface } (let C = Command Iᵢₒ) (let R = Response Iᵢₒ) where

  infixl 2 _>>=_

  exec      :  ∀ {i A}    (c : C) (f : R c → IO Iᵢₒ i A) → IO Iᵢₒ i A
  return  :  ∀ {i A}    (a : A) → IO Iᵢₒ i A
  _>>=_   :  ∀ {i A B}  (m : IO Iᵢₒ i A) (k : A → IO Iᵢₒ i B) → IO Iᵢₒ i B

  force (exec c f)    = exec′ c f
  force (return a)  =  return′ a

  force (_>>=_ {i} m k) {j} with force m {j}
  ... | exec′ c f     =  exec′ c λ r → _>>=_ {j} (f r) k
  ... | return′ a   =  force (k a) {j}

  {-# NON_TERMINATING #-}
  translateIO : ∀{A : Set}
    →  (translateLocal : (c : C) → NativeIO (R c))
    →  IO Iᵢₒ ∞ A
    →  NativeIO A
  translateIO translateLocal m = case (force m) of
    λ{ (exec′ c f)    → (translateLocal c) native>>= λ r →
         translateIO translateLocal (f r)
     ; (return′ a) → nativeReturn a
     }

record IOObject (Iᵢₒ : IOInterface) (I : Interface) (i : Size) : Set where
  coinductive
  field method  :  ∀{j : Size< i} (m : Method I)
                   → IO Iᵢₒ ∞ (Result I m × IOObject Iᵢₒ I j)

open IOObject public

CellC : (i : Size) → Set
CellC = IOObject ConsoleInterface (cellJ String)

simpleCell : ∀{i} (s : String) → CellC i
force (method (simpleCell {i} s) {j} get) =
  exec′ (putStrLn ("getting (" ++ s ++ ")")) λ _ →
  return (s , simpleCell {j} s)
force (method (simpleCell _) (put s)) =
  exec′ (putStrLn ("putting (" ++ s ++ ")")) λ _ →
  return (unit , simpleCell s)

program : ∀{i} → IO ConsoleInterface i Unit
force program =
  let c₁ = simpleCell "Start" in
  exec′ getLine          λ{ nothing → return unit; (just s) →
  method c₁ (put s)    >>= λ{ (_ , c₂) →
  method c₂ get        >>= λ{ (s′ , c₃) →
  exec (putStrLn s′)     λ _ →
  program }}}

main : NativeIO Unit
main = translateIO translateIOConsoleLocal program

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module STLC2.Kovacs.Normalisation where

open import STLC2.Kovacs.NormalForm public

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

-- (Tyᴺ)
mutual
  infix 3 _⊩_
  _⊩_ : 𝒞 → 𝒯 → Set

  Γ ⊩ ⎵      = Γ ⊢ⁿᶠ ⎵

  Γ ⊩ A ⇒ B = ∀ {Γ′} → (η : Γ′ ⊇ Γ) (∂a : Γ′ ∂⊩ A)
                       → Γ′ ∂⊩ B

  Γ ⊩ A ⩕ B  = Γ ∂⊩ A × Γ ∂⊩ B

  Γ ⊩ ⫪     = ⊤

  Γ ⊩ ⫫     = ⊥

  Γ ⊩ A ⩖ B  = Γ ∂⊩ A ⊎ Γ ∂⊩ B

  infix 3 _∂⊩_
  _∂⊩_ : 𝒞 → 𝒯 → Set
  Γ ∂⊩ A = ∀ {Γ′ C} → (η : Γ′ ⊇ Γ)
                     → (f : ∀ {Γ″} → Γ″ ⊇ Γ′ → Γ″ ⊩ A → Γ″ ⊢ⁿᶠ C)
                     → Γ′ ⊢ⁿᶠ C

-- (Conᴺ ; ∙ ; _,_)
infix 3 _∂⊩⋆_
data _∂⊩⋆_ : 𝒞 → 𝒞 → Set
  where
    ∅   : ∀ {Γ} → Γ ∂⊩⋆ ∅

    _,_ : ∀ {Γ Ξ A} → (ρ : Γ ∂⊩⋆ Ξ) (∂a : Γ ∂⊩ A)
                    → Γ ∂⊩⋆ Ξ , A

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

-- (Tyᴺₑ)
mutual
  acc : ∀ {A Γ Γ′} → Γ′ ⊇ Γ → Γ ⊩ A → Γ′ ⊩ A
  acc {⎵}      η M        = renⁿᶠ η M
  acc {A ⇒ B} η f        = λ η′ a → f (η ○ η′) a
  acc {A ⩕ B}  η s        = ∂acc η (proj₁ s) , ∂acc η (proj₂ s)
  acc {⫪}     η s        = tt
  acc {⫫}     η s        = elim⊥ s
  acc {A ⩖ B}  η (inj₁ a) = inj₁ (∂acc η a)
  acc {A ⩖ B}  η (inj₂ b) = inj₂ (∂acc η b)
  -- TODO: Why doesn’t this work?
  -- acc {A ⩖ B}  η s = case⊎ s (λ a → ∂acc η a)
  --                            (λ b → ∂acc η b)

  ∂acc : ∀ {A Γ Γ′} → Γ′ ⊇ Γ → Γ ∂⊩ A → Γ′ ∂⊩ A
  ∂acc η ∂a = λ η′ f → ∂a (η ○ η′) f

-- (Conᴺₑ)
-- NOTE: _⬖_ = ∂acc⋆
_⬖_ : ∀ {Γ Γ′ Ξ} → Γ ∂⊩⋆ Ξ → Γ′ ⊇ Γ → Γ′ ∂⊩⋆ Ξ
∅        ⬖ η = ∅
(ρ , ∂a) ⬖ η = ρ ⬖ η , ∂acc η ∂a

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

!ƛ : ∀ {Γ A B} → (∀ {Γ′} → Γ′ ⊇ Γ → Γ′ ∂⊩ A → Γ′ ∂⊩ B)
               → Γ ⊩ A ⇒ B
!ƛ f = λ η ∂a → f η ∂a

_!∙_ : ∀ {Γ A B} → Γ ⊩ A ⇒ B → Γ ∂⊩ A
                 → Γ ∂⊩ B
f !∙ ∂a = f idₑ ∂a

_!,_ : ∀ {Γ A B} → Γ ∂⊩ A → Γ ∂⊩ B
                 → Γ ⊩ A ⩕ B
∂a !, ∂b = ∂a , ∂b

!π₁ : ∀ {Γ A B} → Γ ⊩ A ⩕ B
                → Γ ∂⊩ A
!π₁ s = proj₁ s

!π₂ : ∀ {Γ A B} → Γ ⊩ A ⩕ B
                → Γ ∂⊩ B
!π₂ s = proj₂ s

!τ : ∀ {Γ} → Γ ⊩ ⫪
!τ = tt

!φ : ∀ {Γ C} → Γ ⊩ ⫫
             → Γ ∂⊩ C
!φ s = elim⊥ s

!ι₁ : ∀ {Γ A B} → Γ ∂⊩ A
                → Γ ⊩ A ⩖ B
!ι₁ ∂a = inj₁ ∂a

!ι₂ : ∀ {Γ A B} → Γ ∂⊩ B
                → Γ ⊩ A ⩖ B
!ι₂ ∂b = inj₂ ∂b

_!⁇_!∥_ : ∀ {Γ A B C} → Γ ⊩ A ⩖ B
                      → (∀ {Γ′} → Γ′ ⊇ Γ → Γ′ ∂⊩ A → Γ′ ∂⊩ C)
                      → (∀ {Γ′} → Γ′ ⊇ Γ → Γ′ ∂⊩ B → Γ′ ∂⊩ C)
                      → Γ ∂⊩ C
s !⁇ f !∥ g = elim⊎ s (λ ∂a → f idₑ ∂a)
                      (λ ∂b → g idₑ ∂b)

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

return : ∀ {A Γ} → Γ ⊩ A → Γ ∂⊩ A
return {A} a = λ η f →
                 f idₑ (acc {A} η a)

bind : ∀ {A C Γ} → Γ ∂⊩ A → (∀ {Γ′} → Γ′ ⊇ Γ → Γ′ ⊩ A → Γ′ ∂⊩ C)
                 → Γ ∂⊩ C
bind ∂a f = λ η f′ →
              ∂a η (λ η′ a →
                f (η ○ η′) a idₑ (λ η″ b →
                  f′ (η′ ○ η″) b))

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

∂!λ : ∀ {Γ A B} → (∀ {Γ′} → Γ′ ⊇ Γ → Γ′ ∂⊩ A → Γ′ ∂⊩ B)
                → Γ ∂⊩ A ⇒ B
∂!λ {A = A} f = return {A ⇒ _}
                       (!ƛ f)

_∂!∙_ : ∀ {Γ A B} → Γ ∂⊩ A ⇒ B → Γ ∂⊩ A
                  → Γ ∂⊩ B
∂f ∂!∙ ∂a = bind ∂f (λ η f → f !∙ ∂acc η ∂a)

_∂!,_ : ∀ {Γ A B} → Γ ∂⊩ A → Γ ∂⊩ B
                  → Γ ∂⊩ A ⩕ B
∂a ∂!, ∂b = return (∂a !, ∂b)

∂!π₁ : ∀ {Γ A B} → Γ ∂⊩ A ⩕ B
                 → Γ ∂⊩ A
∂!π₁ ∂s = bind ∂s (λ η s → !π₁ s)

∂!π₂ : ∀ {Γ A B} → Γ ∂⊩ A ⩕ B
                 → Γ ∂⊩ B
∂!π₂ ∂s = bind ∂s (λ η s → !π₂ s)

∂!τ : ∀ {Γ} → Γ ∂⊩ ⫪
∂!τ {Γ} = return (!τ {Γ})

∂!φ : ∀ {Γ C} → Γ ∂⊩ ⫫
              → Γ ∂⊩ C
∂!φ ∂s = bind ∂s (λ η s → !φ s)

∂!ι₁ : ∀ {Γ A B} → Γ ∂⊩ A
                 → Γ ∂⊩ A ⩖ B
∂!ι₁ {B = B} ∂a = return {_ ⩖ B}
                         (!ι₁ ∂a)

∂!ι₂ : ∀ {Γ A B} → Γ ∂⊩ B
                 → Γ ∂⊩ A ⩖ B
∂!ι₂ {A = A} ∂b = return {A ⩖ _}
                         (!ι₂ ∂b)

_∂!⁇_∂!∥_ : ∀ {Γ A B C} → Γ ∂⊩ A ⩖ B
                        → (∀ {Γ′} → Γ′ ⊇ Γ → Γ′ ∂⊩ A → Γ′ ∂⊩ C)
                        → (∀ {Γ′} → Γ′ ⊇ Γ → Γ′ ∂⊩ B → Γ′ ∂⊩ C)
                        → Γ ∂⊩ C
∂s ∂!⁇ f ∂!∥ g = bind ∂s (λ η s → s !⁇ (λ η′ → f (η ○ η′))
                                     !∥ (λ η′ → g (η ○ η′)))

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

-- (∈ᴺ)
getᵥ : ∀ {Γ Ξ A} → Γ ∂⊩⋆ Ξ → Ξ ∋ A → Γ ∂⊩ A
getᵥ (ρ , ∂a) zero    = ∂a
getᵥ (ρ , ∂a) (suc i) = getᵥ ρ i

-- (Tmᴺ)
eval : ∀ {Γ Ξ A} → Γ ∂⊩⋆ Ξ → Ξ ⊢ A → Γ ∂⊩ A
eval ρ (𝓋 i)         = getᵥ ρ i
eval ρ (ƛ M)         = ∂!λ (λ η ∂a → eval (ρ ⬖ η , ∂a) M)
eval ρ (M ∙ N)       = eval ρ M ∂!∙ eval ρ N
eval ρ (M , N)       = eval ρ M ∂!, eval ρ N
eval ρ (π₁ M)        = ∂!π₁ (eval ρ M)
eval ρ (π₂ M)        = ∂!π₂ (eval ρ M)
eval ρ τ             = ∂!τ
eval ρ (φ M)         = ∂!φ (eval ρ M)
eval ρ (ι₁ M)        = ∂!ι₁ (eval ρ M)
eval ρ (ι₂ M)        = ∂!ι₂ (eval ρ M)
eval ρ (M ⁇ N₁ ∥ N₂) = eval ρ M ∂!⁇ (λ η ∂a → eval (ρ ⬖ η , ∂a) N₁)
                                ∂!∥ (λ η ∂b → eval (ρ ⬖ η , ∂b) N₂)

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

mutual
  -- (qᴺ)
  reify : ∀ {A Γ} → Γ ∂⊩ A → Γ ⊢ⁿᶠ A
  reify {⎵}      ∂a = ∂a idₑ (λ η M → M)
  reify {A ⇒ B} ∂a = ∂a idₑ (λ η f → ƛ (reify (f (wkₑ idₑ) (reflect 0))))
  reify {A ⩕ B}  ∂a = ∂a idₑ (λ η s → reify (proj₁ s) , reify (proj₂ s))
  reify {⫪}     ∂a = ∂a idₑ (λ η s → τ)
  reify {⫫}     ∂a = ∂a idₑ (λ η s → elim⊥ s)
  reify {A ⩖ B}  ∂a = ∂a idₑ (λ η s → elim⊎ s (λ a → ι₁ (reify a))
                                              (λ b → ι₂ (reify b)))

  -- (uᴺ)
  reflect : ∀ {A Γ} → Γ ⊢ⁿᵉ A → Γ ∂⊩ A
  reflect {⎵}      M = return (ne M)
  reflect {A ⇒ B} M = return {A ⇒ _}
                              (λ η ∂a → reflect (renⁿᵉ η M ∙ reify ∂a))
  reflect {A ⩕ B}  M = return (reflect (π₁ M) , reflect (π₂ M))
  reflect {⫪}     M = return tt
  reflect {⫫}     M = λ η f →
                         ne (φ (renⁿᵉ η M))
  reflect {A ⩖ B}  M = λ η f →
                         ne (renⁿᵉ η M ⁇ f (wkₑ idₑ) (inj₁ (reflect 0))
                                       ∥ f (wkₑ idₑ) (inj₂ (reflect 0)))

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

-- (uᶜᴺ)
idᵥ : ∀ {Γ} → Γ ∂⊩⋆ Γ
idᵥ {∅}     = ∅
idᵥ {Γ , A} = idᵥ ⬖ wkₑ idₑ , reflect 0

-- (nf)
nf : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ⁿᶠ A
nf M = reify (eval idᵥ M)

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


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

open import lib.Basics

module lib.types.Empty where

Empty-rec : ∀ {i} {A : Type i} → (Empty → A)
Empty-rec = Empty-elim

⊥-rec : ∀ {i} {A : Type i} → (⊥ → A)
⊥-rec = Empty-rec

Empty-is-prop : is-prop Empty
Empty-is-prop = Empty-elim

⊥-is-prop : is-prop ⊥
⊥-is-prop = Empty-is-prop

negated-equiv-Empty : ∀ {i} (A : Type i) → (¬ A) → (Empty ≃ A)
negated-equiv-Empty A notA = equiv Empty-elim
                                   notA
                                   (λ a → Empty-elim {P = λ _ → Empty-elim (notA a) == a} (notA a))
                                   (Empty-elim {P = λ e → notA (Empty-elim e) == e})

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Sizes for Agda's sized types
------------------------------------------------------------------------

module Size where

postulate
  Size   : Set
  Size<_ : Size → Set
  ↑_     : Size → Size
  ∞      : Size

{-# BUILTIN SIZE    Size   #-}
{-# BUILTIN SIZELT  Size<_ #-}
{-# BUILTIN SIZESUC ↑_     #-}
{-# BUILTIN SIZEINF ∞      #-}


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

module lib.Basics where

open import lib.Base public
open import lib.PathGroupoid public
open import lib.PathFunctor public
open import lib.NType public
open import lib.Equivalences public
open import lib.Univalence public
open import lib.Funext public
open import lib.PathOver public

max_stars_repo_name: sattlerc/HoTT-Agda

max_issues_repo_name: sattlerc/HoTT-Agda

max_forks_repo_name: sattlerc/HoTT-Agda


text:
-- Andreas, 2011-04-14
-- {-# OPTIONS -v tc.cover:20 -v tc.lhs.unify:20 #-}

-- Jesper, 2016-06-23: should also work --cubical-compatible
{-# OPTIONS --cubical-compatible #-}

module Issue291-1775 where

-- Example by Ulf

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

data _≡_ {A : Set}(a : A) : A -> Set where
  refl : a ≡ a

-- since 'n' occurs stronly rigid in 'suc n', the type 'n ≡ suc n' is empty
h : (n : Nat) -> n ≡ suc n -> Nat
h n ()

-- Example by jdanbr...@gmail.com

data Type : Set where
  ₁   : Type
  _×_ : Type → Type → Type
  _+_ : Type → Type → Type

data Fun : Type → Type → Set where
  _∙_ : ∀ {s t u} → Fun t u → Fun s t → Fun s u
  π₁  : ∀ {s t} →   Fun (s × t) s
  π₂  : ∀ {s t} →   Fun (s × t) t
  ι₁  : ∀ {s t} →   Fun s (s + t)
  ι₂  : ∀ {s t} →   Fun t (s + t)

data Val : (t : Type) → Fun ₁ t → Set where
  Valι₁ : ∀ {s t V} → Val s V → Val (s + t) (ι₁ ∙ V)
  Valι₂ : ∀ {s t V} → Val t V → Val (s + t) (ι₂ ∙ V)

data ⊥ : Set where

-- should succeed:
¬Valπ₁ : ∀ {s t : Type} {M : Fun ₁ (s × t)} → Val s (π₁ ∙ M) → ⊥
¬Valπ₁ ()
{- OLD ERROR:
Val .s (π₁ ∙ .M) should be empty, but it isn't obvious that it is.
when checking that the clause ¬Valπ₁ () has type
{s t : Type} {M : Fun ₁ (s × t)} → Val s (π₁ ∙ M) → ⊥
-}


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

open import lib.Basics
open import lib.NType2
open import lib.types.Group
open import lib.types.Sigma
open import lib.types.Pi
open import lib.types.Truncation
open import lib.types.SetQuotient
open import lib.groups.Homomorphism
open import lib.groups.Subgroup
open import lib.groups.SubgroupProp

module lib.groups.QuotientGroup where

module _ {i j} {G : Group i} (P : NormalSubgroupProp G j) where

  private
    module G = Group G
    module P = NormalSubgroupProp P
    infix 80 _⊙_
    _⊙_ = G.comp

  quot-group-rel : Rel G.El j
  quot-group-rel g₁ g₂ = P.prop (G.diff g₁ g₂)

  quot-group-struct : GroupStructure (SetQuot quot-group-rel)
  quot-group-struct = record {M} where
    module M where
      ident : SetQuot quot-group-rel
      ident = q[ G.ident ]

      abstract
        inv-rel : ∀ {g₁ g₂ : G.El} (pg₁g₂⁻¹ : P.prop (G.diff g₁ g₂))
          → q[ G.inv g₁ ] == q[ G.inv g₂ ] :> SetQuot quot-group-rel
        inv-rel {g₁} {g₂} pg₁g₂⁻¹ = ! $ quot-rel $
          transport! (λ g → P.prop (G.inv g₂ ⊙ g))
            (G.inv-inv g₁) $ P.comm g₁ (G.inv g₂) pg₁g₂⁻¹

      inv : SetQuot quot-group-rel → SetQuot quot-group-rel
      inv = SetQuot-rec SetQuot-level (λ g → q[ G.inv g ]) inv-rel

      abstract
        comp-rel-r : ∀ g₁ {g₂ g₂' : G.El} (pg₂g₂'⁻¹ : P.prop (G.diff g₂ g₂'))
          → q[ g₁ ⊙ g₂ ] == q[ g₁ ⊙ g₂' ] :> SetQuot quot-group-rel
        comp-rel-r g₁ {g₂} {g₂'} pg₂g₂'⁻¹ = quot-rel $ transport P.prop
          ( ap (_⊙ G.inv g₁) (! $ G.assoc g₁ g₂ (G.inv g₂'))
          ∙ G.assoc (g₁ ⊙ g₂) (G.inv g₂') (G.inv g₁)
          ∙ ap ((g₁ ⊙ g₂) ⊙_) (! $ G.inv-comp g₁ g₂'))
          (P.conj g₁ pg₂g₂'⁻¹)

      comp' : G.El → SetQuot quot-group-rel → SetQuot quot-group-rel
      comp' g₁ = SetQuot-rec SetQuot-level (λ g₂ → q[ g₁ ⊙ g₂ ]) (comp-rel-r g₁)

      abstract
        comp-rel-l : ∀ {g₁ g₁' : G.El} (pg₁g₁'⁻¹ : P.prop (G.diff g₁ g₁')) g₂
          → q[ g₁ ⊙ g₂ ] == q[ g₁' ⊙ g₂ ] :> SetQuot quot-group-rel
        comp-rel-l {g₁} {g₁'} pg₁g₁'⁻¹ g₂ = quot-rel $ transport! P.prop
            ( ap ((g₁ ⊙ g₂) ⊙_) (G.inv-comp g₁' g₂)
            ∙ ! (G.assoc (g₁ ⊙ g₂) (G.inv g₂) (G.inv g₁') )
            ∙ ap (_⊙ G.inv g₁')
              ( G.assoc g₁ g₂ (G.inv g₂)
              ∙ ap (g₁ ⊙_) (G.inv-r g₂)
              ∙ G.unit-r g₁))
            pg₁g₁'⁻¹

        comp'-rel : ∀ {g₁ g₁' : G.El} (pg₁g₁'⁻¹ : P.prop (G.diff g₁ g₁'))
          → comp' g₁ == comp' g₁'
        comp'-rel pg₁g₁'⁻¹ = λ= $ SetQuot-elim
          (λ _ → =-preserves-set SetQuot-level)
          (comp-rel-l pg₁g₁'⁻¹)
          (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _))

      comp : SetQuot quot-group-rel → SetQuot quot-group-rel → SetQuot quot-group-rel
      comp = SetQuot-rec (→-is-set SetQuot-level) comp' comp'-rel

      abstract
        unit-l : ∀ g → comp ident g == g
        unit-l = SetQuot-elim
          (λ _ → =-preserves-set SetQuot-level)
          (ap q[_] ∘ G.unit-l)
          (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _))

        assoc : ∀ g₁ g₂ g₃ → comp (comp g₁ g₂) g₃ == comp g₁ (comp g₂ g₃)
        assoc = SetQuot-elim
          (λ _ → Π-is-set λ _ → Π-is-set λ _ → =-preserves-set SetQuot-level)
          (λ g₁ → SetQuot-elim
            (λ _ → Π-is-set λ _ → =-preserves-set SetQuot-level)
            (λ g₂ → SetQuot-elim
              (λ _ → =-preserves-set SetQuot-level)
              (λ g₃ → ap q[_] $ G.assoc g₁ g₂ g₃)
              (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _)))
            (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → SetQuot-level _ _)))
          (λ _ → prop-has-all-paths-↓ (Π-is-prop λ _ → Π-is-prop λ _ → SetQuot-level _ _))

        inv-l : ∀ g → comp (inv g) g == ident
        inv-l = SetQuot-elim
          (λ _ → =-preserves-set SetQuot-level)
          (ap q[_] ∘ G.inv-l)
          (λ _ → prop-has-all-paths-↓ (SetQuot-level _ _))

  QuotGroup : Group (lmax i j)
  QuotGroup = group _ SetQuot-level quot-group-struct

{- helper functions -}
module _ {i j} {G : Group i} {P : NormalSubgroupProp G j} where
  private
    module G = Group G
    module P = NormalSubgroupProp P
    infix 80 _⊙_
    _⊙_ = G.comp

  q[_]ᴳ : G →ᴳ QuotGroup P
  q[_]ᴳ = group-hom q[_] λ _ _ → idp

  quot-relᴳ : ∀ {g₁ g₂} → P.prop (G.diff g₁ g₂) → q[ g₁ ] == q[ g₂ ]
  quot-relᴳ {g₁} {g₂} = quot-rel {R = quot-group-rel P} {a₁ = g₁} {a₂ = g₂}

  private
    abstract
      quot-group-rel-is-refl : is-refl (quot-group-rel P)
      quot-group-rel-is-refl g = transport! P.prop (G.inv-r g) P.ident

      quot-group-rel-is-sym : is-sym (quot-group-rel P)
      quot-group-rel-is-sym {g₁} {g₂} pg₁g₂⁻¹ =
        transport P.prop (G.inv-comp g₁ (G.inv g₂) ∙ ap (_⊙ G.inv g₁) (G.inv-inv g₂)) (P.inv pg₁g₂⁻¹)

      quot-group-rel-is-trans : is-trans (quot-group-rel P)
      quot-group-rel-is-trans {g₁} {g₂} {g₃} pg₁g₂⁻¹ pg₂g₃⁻¹ =
        transport P.prop
          ( G.assoc g₁ (G.inv g₂) (g₂ ⊙ G.inv g₃)
          ∙ ap (g₁ ⊙_) ( ! (G.assoc (G.inv g₂) g₂ (G.inv g₃))
                       ∙ ap (_⊙ G.inv g₃) (G.inv-l g₂)
                       ∙ G.unit-l (G.inv g₃)))
          (P.comp pg₁g₂⁻¹ pg₂g₃⁻¹)

  quot-relᴳ-equiv : {g₁ g₂ : G.El} → P.prop (g₁ ⊙ G.inv g₂) ≃ (q[ g₁ ] == q[ g₂ ])
  quot-relᴳ-equiv = quot-rel-equiv {R = quot-group-rel P} (P.level _)
    quot-group-rel-is-refl
    quot-group-rel-is-sym
    quot-group-rel-is-trans

module QuotGroup {i j} {G : Group i} (P : NormalSubgroupProp G j)
  where
  grp = QuotGroup P
  open Group grp public

module _ {i j k} {G : Group i}
  (P : SubgroupProp G j) (Q : NormalSubgroupProp G k) where

  quot-of-sub : NormalSubgroupProp (Subgroup P) k
  quot-of-sub = Q ∘nsubᴳ Subgroup.inject P

{- interactions between quotients and subgroups (work in progress) -}
{- So far not used.

-- QuotGroup rel-over-sub ≃ᴳ Subgroup prop-over-quot

module _ {i j k} {G : Group i}
  (Q : NormalSubgroupProp G j) (P : SubgroupProp G k)
  (prop-respects-quot : NormalSubgroupProp.subgrp-prop Q ⊆ᴳ P) where

  private
    module G = Group G
    module Q = NormalSubgroupProp Q
    module P = SubgroupProp P

  prop-over-quot : SubgroupProp (QuotGroup Q) k
  prop-over-quot = record {M; diff = λ {g₁} {g₂} → M.diff' g₁ g₂} where
    module M where
      module QG = Group (QuotGroup Q)
      private
        abstract
          prop'-rel : ∀ {g₁ g₂} (qg₁g₂⁻¹ : quot-group-rel Q g₁ g₂)
            → P.prop g₁ == P.prop g₂
          prop'-rel {g₁} {g₂} qg₁g₂⁻¹ = ua $
            equiv (λ pg₁ → transport P.prop
                    ( ap (λ g → G.comp g g₁) (G.inv-comp g₁ (G.inv g₂))
                    ∙ G.assoc (G.inv (G.inv g₂)) (G.inv g₁) g₁
                    ∙ ap2 G.comp (G.inv-inv g₂) (G.inv-l g₁)
                    ∙ G.unit-r g₂)
                    (P.comp (P.inv pg₁g₂⁻¹) pg₁))
                  (λ pg₂ → transport P.prop
                    ( G.assoc g₁ (G.inv g₂) g₂
                    ∙ ap (G.comp g₁) (G.inv-l g₂)
                    ∙ G.unit-r g₁)
                    (P.comp pg₁g₂⁻¹ pg₂))
                  (λ _ → prop-has-all-paths (P.level g₂) _ _)
                  (λ _ → prop-has-all-paths (P.level g₁) _ _)
            where pg₁g₂⁻¹ : P.prop (G.diff g₁ g₂)
                  pg₁g₂⁻¹ = prop-respects-quot (G.diff g₁ g₂) qg₁g₂⁻¹

        prop' : Group.El (QuotGroup Q) → hProp k
        prop' = SetQuot-rec
          (hProp-is-set k)
          (λ g → P.prop g , P.level g)
          (nType=-out ∘ prop'-rel)

      prop : QG.El → Type k
      prop g' = fst (prop' g')

      abstract
        level : ∀ g' → is-prop (prop g')
        level g' = snd (prop' g')

      ident : prop q[ G.ident ]
      ident = P.ident

      abstract
        diff' : ∀ g₁' g₂' → prop g₁' → prop g₂' → prop (QG.diff g₁' g₂')
        diff' = SetQuot-elim
          {P = λ g₁' → ∀ g₂' → prop g₁' → prop g₂' → prop (QG.diff g₁' g₂')}
          (λ g₁' → Π-is-set λ g₂' → →-is-set $ →-is-set $ raise-level -1 (level (QG.diff g₁' g₂')))
          (λ g₁ → SetQuot-elim (λ g₂' → →-is-set $ →-is-set $ raise-level -1 (level (QG.diff q[ g₁ ] g₂')))
            (λ g₂ pg₁ pg₂ → P.diff pg₁ pg₂)
            (λ {_} {g₂} _ → prop-has-all-paths-↓ (→-is-prop $ →-is-prop $ level q[ G.diff g₁ g₂ ])))
          (λ {_} {g₁} _ → prop-has-all-paths-↓ (Π-is-prop λ g₂' → →-is-prop $ →-is-prop $ level (QG.diff q[ g₁ ] g₂')))

-}

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
-- Issue #2979 reported by Favonia on 2018-02-23

{-# OPTIONS --cubical-compatible --rewriting --confluence-check #-}

data _==_ {A : Set} (a : A) : A → Set where
  idp : a == a

record Marked (A : Set) : Set where
  constructor mark
  field
    unmark : A
open Marked

postulate
  _↦_ : ∀ {A : Set} → A → A → Set
{-# BUILTIN REWRITE _↦_ #-}

postulate
  A : Set
  Q : (I : Marked A → Set) → Set
  q : (I : Marked A → Set) (a : Marked A) → Q I
  Q-elim : (I : Marked A → Set) {P : Q I → Set}
    (q* : (a : Marked A) → P (q I a)) (x : Q I) → P x
  Q-rec : (I : Marked A → Set) {B : Set} (q* : Marked A → B)
    → Q I → B
  Q-rec-β : (I : Marked A → Set) {B : Set} (q* : Marked A → B)
    → (a : Marked A) → Q-rec I {B} q* (q I a) ↦ q* a
{-# REWRITE Q-rec-β #-}

p₀ : Marked A → Set
p₀ (mark a) = A

p₁ : Marked A → Set
p₁ (mark a) = A

q= : ∀ x → Q-rec p₀ (q p₀) x == Q-rec p₁ (q p₁) x
q= = Q-elim p₀ (λ _ → idp)


text:
module Printf where

open import Data.List hiding(_++_)
open import Data.String
open import Data.Unit
open import Data.Empty
open import Data.Char
open import Data.Product
open import Data.Nat.Show renaming (show to showNat)
open import Data.Nat
open import Function using (_∘_)

data ValidFormat : Set₁ where
   argument : (A : Set) → (A → String) → ValidFormat
   literal  : Char      → ValidFormat

data Format : Set₁ where
   valid   : List ValidFormat → Format
   invalid : Format

parse : String → Format
parse s = parse′ [] (toList s)
  where
    parse′ : List ValidFormat → List Char → Format
    parse′ l ('%' ∷ 's' ∷ fmt) = parse′ (argument String (λ x → x) ∷ l) fmt
    parse′ l ('%' ∷ 'c' ∷ fmt) = parse′ (argument Char (λ x → fromList [ x ]) ∷ l) fmt
    parse′ l ('%' ∷ 'd' ∷ fmt) = parse′ (argument ℕ showNat ∷ l) fmt
    parse′ l ('%' ∷ '%' ∷ fmt) = parse′ (literal '%' ∷ l) fmt
    parse′ l ('%' ∷ c   ∷ fmt) = invalid
    parse′ l (c         ∷ fmt) = parse′ (literal c ∷ l) fmt
    parse′ l []                = valid (reverse l)

Args : Format → Set
Args invalid                    = ⊥ → String
Args (valid (argument t _ ∷ r)) = t → (Args (valid r))
Args (valid (literal _ ∷ r))    = Args (valid r)
Args (valid [])                 = String

FormatArgs : String → Set
FormatArgs f = Args (parse f)

sprintf : (f : String) → FormatArgs f
sprintf = sprintf′ "" ∘ parse
  where
    sprintf′ : String → (f : Format) → Args f
    sprintf′ accum invalid                    = λ t → ""
    sprintf′ accum (valid [])                 = accum
    sprintf′ accum (valid (argument _ s ∷ l)) = λ t →  (sprintf′ (accum ++ s t) (valid l))
    sprintf′ accum (valid (literal c ∷ l))    = sprintf′ (accum ++ fromList [ c ]) (valid l)

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
module Imports.Issue958 where

postulate FunctorOps : Set
module FunctorOps (ops : FunctorOps) where
  postulate map : Set

postulate IsFunctor : Set
module IsFunctor (fun : IsFunctor) where
  postulate ops : FunctorOps
  open FunctorOps ops public


text:
module Okasaki where

open import Data.Bool using (Bool; true; false) renaming (T to So; not to ¬)

open import Data.Nat hiding (_<_; _≤_; _≟_; compare)
  renaming (decTotalOrder to ℕ-DTO)

open import Relation.Binary hiding (_⇒_)

module RBTree {a ℓ}(order : StrictTotalOrder a ℓ ℓ) where

  open module sto = StrictTotalOrder order
  A = Carrier

  pattern LT = tri< _ _ _
  pattern EQ = tri≈ _ _ _
  pattern GT = tri> _ _ _
  _≤_ = compare

  data Color : Set where
    R B : Color

  _=ᶜ_ : Color → Color → Bool
  R =ᶜ R = true
  B =ᶜ B = true
  _ =ᶜ _ = false

  Height = ℕ

  data Tree : Set a where
    E : Tree
    T : Color → Tree → A → Tree → Tree

  set = Tree

  empty : set
  empty = E

  member : A → set → Bool
  member x E = false
  member x (T _ a y b) with x ≤ y
  ... | LT = member x a
  ... | EQ = true
  ... | GT = member x b

  insert : A → set → set
  insert x s = makeBlack (ins s)
    where
      balance : Color → set → A → set → set
      balance B (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)
      balance B (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)
      balance B a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)
      balance B a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)
      balance color a x b = T color a x b

      ins : set → set
      ins E = T R E x E
      ins (T color a y b) with x ≤ y
      ... | LT = balance color (ins a) y b
      ... | EQ = T color a y b
      ... | GT = balance color a y (ins b)

      makeBlack : set → set
      makeBlack E = E
      makeBlack (T _ a y b) = T B a y b

max_stars_repo_name: toonn/sciartt

max_issues_repo_name: toonn/sciartt

max_forks_repo_name: toonn/sciartt


text:
module _ where

open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.Unit
open import Agda.Builtin.Equality

variable
  A B : Set
  x y : A
  xs  : List A

infix 3 _∈_
data _∈_ {A : Set} (x : A) : List A → Set where
  zero : x ∈ x ∷ xs
  suc  : x ∈ xs → x ∈ y ∷ xs

pattern vArg x = arg (arg-info visible relevant) x

search : Nat → Term → Term → TC ⊤
search zero i hole = typeError (strErr "Not found" ∷ [])
search (suc n) i hole = do
  catchTC (noConstraints (unify hole i))
          (search n (con (quote _∈_.suc) (vArg i ∷ [])) hole)

findElem : Nat → Term → TC ⊤
findElem depth hole = search depth (con (quote _∈_.zero) []) hole

index : (x : A) (xs : List A) {@(tactic findElem 10) i : x ∈ xs} → Nat
index x xs {zero}  = zero
index x xs {suc i} = suc (index x _ {i})

test₁ : index 3 (1 ∷ 2 ∷ 3 ∷ []) ≡ 2
test₁ = refl

test₂ : index x (y ∷ x ∷ x ∷ []) ≡ 1
test₂ = refl


text:
module Data.List.Proofs.Length where

import Lvl
open import Functional
open import Function.Names as Names using (_⊜_)
open import Data.Boolean
open import Data.List as List
open import Data.List.Functions
open import Logic
open import Logic.Propositional
open import Numeral.Finite
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function.Multi
open import Structure.Operator.Properties
open import Structure.Operator
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₑ : Lvl.Level
private variable T A B : Type{ℓ}
private variable l l₁ l₂ : List(T)
private variable a b x : T
private variable n : ℕ
private variable f : A → B
private variable P : List(T) → Stmt{ℓ}

-- TODO: Almost all of these can use Preserving instead

length-[∅] : (length(∅ {T = T}) ≡ 0)
length-[∅] = [≡]-intro

length-singleton : (length{T = T}(singleton(a)) ≡ 1)
length-singleton = [≡]-intro

instance
  length-preserves-prepend : Preserving₁(length)(a ⊰_)(𝐒)
  Preserving.proof (length-preserves-prepend {a = a}) {x} = [≡]-intro

length-postpend : ((length ∘ postpend a) ⊜ (𝐒 ∘ length))
length-postpend {x = l} = List.elim [≡]-intro (\x l → [≡]-with(𝐒) {length(postpend _ l)}{𝐒(length l)}) l

instance
  length-preserves-postpend : Preserving₁(length)(postpend a)(𝐒)
  Preserving.proof (length-preserves-postpend {a = a}) {x} = length-postpend {a = a}{x = x}

length-[++] : (length{T = T}(l₁ ++ l₂) ≡ length(l₁) + length(l₂))
length-[++] {T = T} {l₁ = l₁} {l₂} = List.elim base next l₁ where
  base : length(∅ ++ l₂) ≡ length{T = T}(∅) + length(l₂)
  base = symmetry(_≡_) (identityₗ(_+_)(0))

  next : ∀(x)(l) → (length(l ++ l₂) ≡ length(l) + length(l₂)) → (length((x ⊰ l) ++ l₂) ≡ length(x ⊰ l) + length(l₂))
  next x l stmt =
    length((x ⊰ l) ++ l₂)      🝖[ _≡_ ]-[]
    length(x ⊰ (l ++ l₂))      🝖[ _≡_ ]-[]
    𝐒(length(l ++ l₂))         🝖[ _≡_ ]-[ [≡]-with(𝐒) stmt ]
    𝐒(length(l) + length(l₂))  🝖[ _≡_ ]-[ [+]-stepₗ {length(l)} {length(l₂)} ]
    𝐒(length(l)) + length(l₂)  🝖[ _≡_ ]-[]
    length(x ⊰ l) + length(l₂) 🝖-end

instance
  length-preserves-[++] : Preserving₂(length{T = T})(_++_)(_+_)
  Preserving.proof length-preserves-[++] {l₁} {l₂} = length-[++] {l₁ = l₁} {l₂ = l₂}

length-reverse : ((length{T = T} ∘ reverse) ⊜ length)
length-reverse {x = ∅}     = [≡]-intro
length-reverse {x = x ⊰ l} = length-postpend{a = x}{x = reverse l} 🝖 [≡]-with(𝐒) (length-reverse {x = l})

instance
  length-preserves-reverse : Preserving₁(length{T = T})(reverse)(id)
  Preserving.proof length-preserves-reverse {l} = length-reverse {x = l}

length-repeat : ((length{T = T} ∘ repeat(a)) ⊜ id)
length-repeat{T = T}{x = 𝟎}    = [≡]-intro
length-repeat{T = T}{x = 𝐒(n)} = [≡]-with(𝐒) (length-repeat{T = T}{x = n})

length-tail : ((length{T = T} ∘ tail) ⊜ (𝐏 ∘ length))
length-tail{x = ∅}     = [≡]-intro
length-tail{x = _ ⊰ l} = [≡]-intro

instance
  length-preserves-tail : Preserving₁(length{T = T})(tail)(𝐏)
  Preserving.proof length-preserves-tail {l} = length-tail {x = l}

length-map : ∀{f : A → B} → ((length ∘ map f) ⊜ length)
length-map {f = f}{x = ∅}     = [≡]-intro
length-map {f = f}{x = x ⊰ l} = [≡]-with(𝐒) (length-map {f = f}{x = l})

instance
  length-preserves-map : Preserving₁(length{T = T})(map f)(id)
  Preserving.proof (length-preserves-map {f = f}) {l} = length-map {f = f}{x = l}

length-foldᵣ : ∀{init}{f}{g} → (∀{x}{l} → (length(f x l) ≡ g x (length l))) → (length{T = T}(foldᵣ f init l) ≡ foldᵣ g (length init) l)
length-foldᵣ {l = ∅}                    _ = [≡]-intro
length-foldᵣ {l = x ⊰ l} {init} {f} {g} p =
  length(foldᵣ f init (x ⊰ l))    🝖[ _≡_ ]-[]
  length(f(x) (foldᵣ f init l))   🝖[ _≡_ ]-[ p ]
  g(x) (length(foldᵣ f init l))   🝖[ _≡_ ]-[ [≡]-with(g(x)) (length-foldᵣ {l = l} {init} {f} {g} p) ]
  g(x) (foldᵣ g (length init) l)  🝖[ _≡_ ]-[]
  foldᵣ g (length init) (x ⊰ l)   🝖-end

length-concatMap : ∀{f} → (length{T = T}(concatMap f l) ≡ foldᵣ((_+_) ∘ length ∘ f) 𝟎 l)
length-concatMap {l = l} {f} = length-foldᵣ{l = l}{init = ∅}{f = (_++_) ∘ f} \{x l} → length-[++] {l₁ = f(x)}{l₂ = l}

length-accumulateIterate₀ : ∀{n}{f}{init : T} → (length(accumulateIterate₀ n f init) ≡ n)
length-accumulateIterate₀ {n = 𝟎}      = [≡]-intro
length-accumulateIterate₀ {n = 𝐒 n}{f} = [≡]-with(𝐒) (length-accumulateIterate₀ {n = n}{f})

length-[++^] : (length(l ++^ n) ≡ length(l) ⋅ n)
length-[++^] {l = l}{𝟎}    = [≡]-intro
length-[++^] {l = l}{𝐒(n)} =
  length-[++] {l₁ = l}{l ++^ n}
  🝖 [≡]-with(expr ↦ length(l) + expr) (length-[++^] {l = l}{n})

length-isEmpty : (length(l) ≡ 0) ↔ (isEmpty(l) ≡ 𝑇)
length-isEmpty {l = ∅}     = [↔]-intro (const [≡]-intro) (const [≡]-intro)
length-isEmpty {l = x ⊰ L} = [↔]-intro (\()) (\())

instance
  length-preserves-insert : Preserving₁(length)(insert n x)(𝐒)
  Preserving.proof (length-preserves-insert {n = n}) = proof{n = n} where
    proof : ∀{n} → (length(insert n x l) ≡ 𝐒(length l))
    proof         {l = _}     {n = 𝟎}   = [≡]-intro
    proof         {l = ∅}     {n = 𝐒 n} = [≡]-intro
    proof {x = x} {l = y ⊰ l} {n = 𝐒 n} rewrite proof {x = x} {l = l} {n = n} = [≡]-intro

length-insertIn : ∀{n} → (length(insertIn x l n) ≡ 𝐒(length l))
length-insertIn         {l = _}     {n = 𝟎}   = [≡]-intro
length-insertIn         {l = ∅}     {n = 𝐒 n} = [≡]-intro
length-insertIn {x = x} {l = y ⊰ l} {n = 𝐒 n} rewrite length-insertIn {x = x} {l = l} {n = n} = [≡]-intro


text:
-- We show Gausssian Integers forms an Euclidean domain. The proofs
-- are straightforward.

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

module GauInt.EucDomain where

-- imports from local.

-- Hiding the usual div and mod function. We will the new instance in
-- Integer.EucDomain2
import Instances hiding (DMℤ)
open Instances

open import Integer.EucDomain2
  renaming (div' to divℤ ; mod' to modℤ ; euc-eq' to euc-eqℤ ; euc-rank' to euc-rankℤ)
open import Integer.Properties

open import GauInt.Base
  using (𝔾 ; _+_i ; _ᶜ ; Re ; Im ; _+0i ; _+0i' ; 0𝔾 ; 1𝔾)
open import GauInt.Properties
open import GauInt.Instances

-- imports from stdlib and Agda.
open import Relation.Nullary using (yes ; no ; ¬_)
open import Relation.Binary.PropositionalEquality

open import Data.Product as P using (_×_ ; _,_ ; proj₁ ; proj₂)
open import Data.Sum as S renaming ([_,_]′ to ⊎-elim)

open import Data.Nat as Nat using (ℕ ; suc ; zero ; z≤n)
import Data.Nat.Properties as NatP
open import Data.Integer as Int
  using (0ℤ ; +0 ; +_ ; _≥_ ; +≤+ ; +[1+_] ; -[1+_] ; ℤ ; ∣_∣)
import Data.Integer.Properties as IntP

import Data.Nat.Solver as NS
import Data.Integer.Solver as IS
import GauInt.Solver as GS
open import Algebra.Properties.Ring +-*-ring
open import Algebra.Definitions (_≡_ {A = 𝔾}) using (AlmostLeftCancellative)

open import Function.Base using (_$_)

-- ----------------------------------------------------------------------
-- Euclidean Structure on 𝔾

-- As explained in the imports part, we will use the div and mod
-- function defined in Integer.EucDomain2.

-- A special case when the divisor is a positive natural number. The proof:
-- Let x = a + b i, and y = d. By integer euc-eq and euc-rank we have
-- step-a : a = ra + qa * d, with rank ra ≤ d / 2.
-- step-b : b = rb + qb * d, with rank rb ≤ d / 2.
-- We let q = qa + qb i, r = ra + rb i. Easy to check that
-- eq : x = r + q y. Slightly harder to check
-- le : rank r ≤ d / 2 (see below).

div' : 𝔾 -> (d : ℕ) -> ¬ d ≡ 0# -> 𝔾
div' n zero n0 with n0 refl
... | ()
div' (a + b i) d@(suc e) n0 = qa + qb i
  where
    qa = a / + d
    qb = b / + d

mod' : 𝔾 -> (d : ℕ) -> ¬ d ≡ 0# -> 𝔾
mod' n zero n0 with n0 refl
... | ()
mod' (a + b i) d@(suc e) n0 = ra + rb i
  where
    ra = a % + d
    rb = b % + d

div : (x y : 𝔾) -> ¬ y ≡ 0# -> 𝔾
div x y n0 = div' (x * y ᶜ) y*yᶜ n0'
  where
    y*yᶜ : ℕ
    y*yᶜ = rank y

    n0' :  ¬ rank y ≡ 0#
    n0' = y≠0#⇒rank≠0 n0

mod : (x y : 𝔾) -> ¬ y ≡ 0# -> 𝔾
mod x y n0 = (x - q * y)
  where
    q = div x y n0

-- ----------------------------------------------------------------------
-- euc-eq and euc-rank property for div' and mod'

-- Dividend = reminder + quotient * divisor.
euc-eq' : ∀ (x : 𝔾) (d : ℕ) (n0 : ¬ d ≡ 0) ->
             let r = mod' x d n0 in let q = div' x d n0 in
             x ≡ r + q * (d +0i)
euc-eq' n zero n0 with n0 refl
... | ()
euc-eq' x@(a + b i) d@(suc e) n0 = eq
  where
    -- setting up q and r.
    n0' : ¬ + d ≡ 0#
    n0' p = n0 (IntP.+-injective p)

    qa = a / + d
    qb = b / + d
    ra = a % + d
    rb = b % + d

    ea : a ≡ ra + qa * + d
    ea = euc-eqℤ a (+ d) n0'
    eb : b ≡ rb + qb * + d
    eb = euc-eqℤ b (+ d) n0'

    q : 𝔾
    q = qa + qb i

    r : 𝔾
    r = ra + rb i

    -- Inject natural number d to Gaussian integer.
    y = d +0i

    -- Proving x = r + q * y.
    eq : x ≡ r + q * y
    eq = begin
        x ≡⟨ refl ⟩
        a + b i ≡⟨ cong (λ x -> x + b i) ea ⟩
        (ra + qa * (+ d)) + b i ≡⟨ cong (λ x -> (ra + qa * (+ d)) + x i) eb ⟩
        (ra + qa * (+ d)) + (rb + qb * (+ d)) i ≡⟨ refl ⟩
        (ra + rb i) + ((qa * (+ d)) + (qb * (+ d)) i) ≡⟨ cong (λ x → (ra + rb i) + ((qa * (+ d)) + x i)) ((solve 3 (λ qa d qb → qb :* d := qa :* con 0ℤ :+ qb :* d) refl) qa (+ d) qb) ⟩
        (ra + rb i) + ((qa * (+ d)) + (qa * 0ℤ + qb * (+ d)) i) ≡⟨ cong (λ x → (ra + rb i) + (x + (qa * 0ℤ + qb * (+ d)) i)) ((solve 3 (λ qa d qb → qa :* d := qa :* d :- qb :* con 0ℤ) refl) qa (+ d) qb) ⟩
        (ra + rb i) + ((qa * (+ d) - qb * 0ℤ) + (qa * 0ℤ + qb * (+ d)) i) ≡⟨ refl ⟩
        (ra + rb i) + (qa + qb i) * y ≡⟨ refl ⟩
        r + q * y ∎
          where
            open IS.+-*-Solver
            open ≡-Reasoning

-- rank r < rank (inj d)
euc-rank' : ∀ (x : 𝔾) (d : ℕ) (n0 : ¬ d ≡ 0) ->
             let r = mod' x d n0 in let q = div' x d n0 in
             rank r < rank (d +0i)
euc-rank' n zero n0 with n0 refl
... | ()
euc-rank' x@(a + b i) d@(suc e) n0 = le
  where
    -- setting up q and r.
    n0' : ¬ + d ≡ 0#
    n0' p = n0 (IntP.+-injective p)

    r : 𝔾
    r = mod' x d n0
    ra = Re r
    rb = Im r

    q : 𝔾
    q = div' x d n0
    qa = Re q
    qb = Im q

    lea : ∣ ra ∣ ≤ d / 2
    lea = euc-rankℤ a (+ d) n0'

    leb : ∣ rb ∣ ≤ d / 2
    leb = euc-rankℤ b (+ d) n0'

    y = d +0i

    -- Proving rank r < rank y.
    -- Some auxillary lemmas.
    lem1 : ∀ {d : ℕ} -> d / 2 + d / 2 ≤ d
    lem1 {d} = begin
      d / 2 + d / 2  ≡⟨ solve 1 (λ x → x :+ x := x :* con 2) refl (d / 2) ⟩
      d / 2 * 2      ≤⟨ NatP.m≤n+m (d / 2 * 2) (d % 2) ⟩
      d % 2 + d / 2 * 2  ≡⟨ (sym $ NatESR.euc-eq d 2 (λ ())) ⟩
      d  ∎
        where
          open NatP.≤-Reasoning
          open NS.+-*-Solver

    lem2 : ∀ {d : Nat.ℕ} -> d / 2 ≤ d
    lem2 {d} = begin
      d / 2  ≤⟨ NatP.m≤n+m (d / 2) (d / 2) ⟩
      d / 2 + d / 2      ≤⟨ lem1 {d} ⟩
      d  ∎
        where
          open NatP.≤-Reasoning
          open NS.+-*-Solver

    lem2-strict : ∀ {d : Nat.ℕ} .{{_ : NonZero d}} -> (d / 2) < d
    lem2-strict {x@(suc d)} with x / 2 Nat.≟ 0
    ... | no ¬p = begin-strict
      x / 2  <⟨ NatP.m<n+m (x / 2) x/2>0 ⟩
      x / 2 + x / 2      ≤⟨ lem1 {x} ⟩
      x  ∎
      where
        open NatP.≤-Reasoning
        open NS.+-*-Solver
        open import Relation.Binary.Definitions
        open import Data.Empty

        x/2>0 : 0 < (x / 2)
        x/2>0 with NatP.<-cmp 0 (x / 2)
        ... | tri< a ¬b ¬c = a
        ... | tri≈ ¬a b ¬c = ⊥-elim (¬p (sym b))
    ... | yes p rewrite p = Nat.s≤s Nat.z≤n

    lem3 : rank y ≡ d * d
    lem3 = begin
      rank y ≡⟨ refl ⟩
      ∣ (+ d) * (+ d) + 0ℤ * 0ℤ ∣  ≡⟨ cong ∣_∣ (solve 1 (λ x → x :* x :+ con 0ℤ :* con 0ℤ := x :* x) refl (+ d)) ⟩
      ∣ (+ d) * (+ d) ∣     ≡⟨ IntP.abs-*-commute (+ d) (+ d) ⟩
      ∣ (+ d) ∣ * ∣ (+ d) ∣     ≡⟨ refl ⟩
      d * d  ∎
        where
          open IS.+-*-Solver
          open ≡-Reasoning

    -- The proof idea:
    -- rank r = ∣ ra * ra + rb * rb ∣ = ∣ ra ∣ * ∣ ra ∣ + ∣ rb ∣ * ∣ rb ∣
    -- ≤ d / 2 * d / 2 + d / 2 * d / 2 by the integer divmod property.
    -- ≤ d * d
    -- = rank y

    le : rank r < rank y
    le = begin-strict
      rank r                ≡⟨ refl ⟩
      let (sa , sae) = (a*a=+b ra) in let (sb , sbe) = a*a=+b rb in
      ∣ ra * ra + rb * rb ∣  ≡⟨ tri-eq' ra rb ⟩
      ∣ ra * ra ∣ + ∣ rb * rb ∣ ≡⟨ cong₂ _+_ (IntP.abs-*-commute ra ra) (IntP.abs-*-commute rb rb) ⟩
      ∣ ra ∣ * ∣ ra ∣ + ∣ rb ∣ * ∣ rb ∣  ≤⟨ NatP.+-mono-≤ (NatP.*-mono-≤ lea lea) (NatP.*-mono-≤ leb leb) ⟩
      (d / 2) * (d / 2) + (d / 2) * (d / 2) ≡⟨ solve 1 (λ x → (x :* x) :+ (x :* x) := x :* (x :+ x)) refl (d / 2) ⟩
      (d / 2) * ((d / 2) + (d / 2)) ≤⟨ NatP.*-monoʳ-≤ (d / 2) lem1 ⟩
      (d / 2) * d <⟨ NatP.*-monoˡ-< d (lem2-strict {d}) ⟩
      d * d                ≡⟨ sym lem3 ⟩
      rank y  ∎
        where
          open NatP.≤-Reasoning
          open NS.+-*-Solver

-- ----------------------------------------------------------------------
-- euc-eq and euc-rank property for div and mod

-- This is the case when the divisor y = c + d i is an arbitrary
-- non-zero Gaussian integer. Easy to see rank y ᶜ = rank y = y * y
-- ᶜ = ∣ c * c + d * d ∣ ≠ 0. Notice that by the previous spcial
-- case (when the divisor is a positive natural number) we have

-- eq' : x * y ᶜ = r' + q' * (y * y ᶜ), and
-- le' : rank r' < rank (y * y ᶜ) = rank y * rank y ᶜ
-- (eq') ⇒ r' = x * y ᶜ - q' * (y * y ᶜ) = (x - q' * y) * y ᶜ
-- ⇒ eqr: rank r' = rank (x - q' * y) * rank y ᶜ
-- (le') & (eqr) ⇒ rank (x - q' * y) < rank y since rank y ᶜ ≠ 0.

-- So setting q = q', and r = x - q' * y as div and mod functions do,
-- then check the euc-rank property holds.

-- Dividend = reminder + quotient * divisor.
euc-eq : ∀ (x y : 𝔾) (n0 : ¬ y ≡ 0𝔾) ->
             let r = mod x y n0 in let q = div x y n0 in
             x ≡ r + q * y
euc-eq x y n0 = claim
  where
    -- Setting up r and q.
    r : 𝔾
    r = mod x y n0
    q : 𝔾
    q = div x y n0

    claim : x ≡ (x - q * y) + q * y
    claim = begin
      x ≡⟨ solve 2 (\ x qy -> x := (x :- qy) :+ qy) refl x (q * y) ⟩
      (x - q * y) + q * y  ∎
      where
        open GS.+-*-Solver
        open ≡-Reasoning

-- rank r < rank y.
euc-rank : ∀ (x y : 𝔾) (n0 : ¬ y ≡ 0#) ->
             let r = mod x y n0 in let q = div x y n0 in
             rank r < rank y
euc-rank x y n0 = claim
  where
    n0' : ¬ rank y ≡ 0#
    n0' = y≠0#⇒rank≠0 n0

    r : 𝔾
    r = mod x y n0
    q : 𝔾
    q = div x y n0

    eq : x ≡ r + q * y
    eq = euc-eq x y n0

    r' : 𝔾
    r' = mod' (x * y ᶜ) (rank y) n0'
    q' : 𝔾
    q' = div' (x * y ᶜ) (rank y) n0'

    eq' : x * y ᶜ ≡ r' + q' * (rank y +0i)
    eq' = euc-eq' (x * y ᶜ) (rank y) n0'

    le' : rank r' < rank (rank y +0i)
    le' = euc-rank' (x * y ᶜ) (rank y) n0'

    q=q' : q ≡ q'
    q=q' = refl

    -- eqr : rank r' = rank (x - q' * y) * rank y ᶜ ---- (3)
    eqr : rank r' ≡ rank (x - q' * y) * rank (y ᶜ)
    eqr = begin
      rank r' ≡⟨ cong rank step ⟩
      rank ((x - q' * y) * y ᶜ) ≡⟨ rank-*-commute (x - q * y) (y ᶜ) ⟩
      rank (x - q' * y) * rank (y ᶜ) ∎
        where
          open ≡-Reasoning
          step : r' ≡ (x - q' * y) * y ᶜ
          step = begin
            r' ≡⟨ solve 2 (λ r x → r := r :+ x :- x) refl r' (q' * (rank y +0i)) ⟩
            r' + q' * (rank y +0i) - q' * (rank y +0i) ≡⟨ cong (_- q' * (rank y +0i)) (sym eq') ⟩
            x * y ᶜ - q' * (rank y +0i) ≡⟨ cong (λ z → x * y ᶜ - q' * z) (sym $ y*yᶜ=rank {y}) ⟩
            x * y ᶜ - q' * (y * y ᶜ) ≡⟨ solve 4 (\ x yc q y -> x :* yc :- q :* ( y :* yc) := (x :- q :* y) :* yc) refl x (y ᶜ) q' y ⟩
            (x - q' * y) * y ᶜ ∎
              where
                open GS.+-*-Solver
                open ≡-Reasoning

    -- (le') & (eqr) ⇒ rank (x - q' * y) < rank y since rank y ᶜ ≠ 0.
    claim : rank (x - q' * y) < rank y
    claim = NatP.*-cancelʳ-< {rank (y ᶜ)} (rank (x - q * y)) (rank y) eqr'
      where
        eqr' : rank (x - q' * y) * rank (y ᶜ) < rank y * rank (y ᶜ)
        eqr' = begin-strict
            rank (x - q' * y) * rank (y ᶜ) ≡⟨ sym eqr ⟩
            rank r' <⟨ le' ⟩
            rank (rank y +0i) ≡⟨ cong rank (sym $ y*yᶜ=rank {y}) ⟩
            rank (y * y ᶜ) ≡⟨ rank-*-commute y (y ᶜ) ⟩
            rank y * rank (y ᶜ) ∎
              where
                open GS.+-*-Solver
                open NatP.≤-Reasoning

-- ----------------------------------------------------------------------
-- 𝔾 is an Euclidean Domain.

import EuclideanDomain
open   EuclideanDomain.Structures (_≡_ {A = 𝔾}) using (IsEuclideanDomain)
open   EuclideanDomain.Bundles using (EuclideanDomainBundle)

+-*-isEuclideanDomain : IsEuclideanDomain _+_ _*_ -_ 0𝔾 1𝔾
+-*-isEuclideanDomain = record
                              { isCommutativeRing = +-*-isCommutativeRing
                              ; *-alc = *-alc-𝔾
                              ; div = div
                              ; mod = mod
                              ; rank = rank
                              ; euc-eq = euc-eq
                              ; euc-rank = euc-rank
                              }

-- Bundle.
+-*-euclideanDomain : EuclideanDomainBundle _ _
+-*-euclideanDomain = record
  { isEuclideanDomain = +-*-isEuclideanDomain'
  }

-- ----------------------------------------------------------------------
-- Making 𝔾 an DivMod instance, overloading div and mod.

-- Translation between two nonzeros.
nz𝔾 : ∀ (x : 𝔾) -> .{{NonZero x}} -> ¬ x ≡ 0#
nz𝔾 (+_ zero + +[1+ n ] i) {{n0}} i0 with i0
... | ()

instance
  g-divmod : DivMod 𝔾
  DivMod.NZT g-divmod = NZT𝔾
  (g-divmod DivMod./ n) d = div n d (nz𝔾 d)
  (g-divmod DivMod.% n) d = mod n d (nz𝔾 d)

max_stars_repo_name: onestruggler/EucDomain

max_issues_repo_name: onestruggler/EucDomain

max_forks_repo_name: onestruggler/EucDomain


text:
{-
  Definition of various kinds of categories.

  This library follows the UniMath terminology, that is:

  Concept              Ob C   Hom C  Univalence

  Precategory          Type   Type   No
  Category             Type   Set    No
  Univalent Category   Type   Set    Yes

  This file also contains
    - pathToIso : Turns a path between two objects into an isomorphism between them
    - opposite categories

-}

{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Categories.Category where

open import Cubical.Core.Glue
open import Cubical.Foundations.Prelude

-- Precategories

record Precategory ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  no-eta-equality
  field
    ob : Type ℓ
    hom : ob → ob → Type ℓ'
    idn : ∀ x → hom x x
    seq : ∀ {x y z} (f : hom x y) (g : hom y z) → hom x z
    seq-λ : ∀ {x y : ob} (f : hom x y) → seq (idn x) f ≡ f
    seq-ρ : ∀ {x y} (f : hom x y) → seq f (idn y) ≡ f
    seq-α : ∀ {u v w x} (f : hom u v) (g : hom v w) (h : hom w x) → seq (seq f g) h ≡ seq f (seq g h)

open Precategory public

-- Categories

record isCategory {ℓ ℓ'} (𝒞 : Precategory ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
  field
    homIsSet : ∀ {x y} → isSet (𝒞 .hom x y)

open isCategory public

-- Isomorphisms and paths in precategories

record CatIso {ℓ ℓ' : Level} {𝒞 : Precategory ℓ ℓ'} (x y : 𝒞 .ob) : Type ℓ' where
  constructor catiso
  field
    h : 𝒞 .hom x y
    h⁻¹ : 𝒞 .hom y x
    sec : 𝒞 .seq h⁻¹ h ≡ 𝒞 .idn y
    ret : 𝒞 .seq h h⁻¹ ≡ 𝒞 .idn x

pathToIso : {ℓ ℓ' : Level} {𝒞 : Precategory ℓ ℓ'} (x y : 𝒞 .ob) (p : x ≡ y) → CatIso {𝒞 = 𝒞} x y
pathToIso {𝒞 = 𝒞} x y p = J (λ z _ → CatIso x z) (catiso (𝒞 .idn x) idx (𝒞 .seq-λ idx) (𝒞 .seq-λ idx)) p
  where
    idx = 𝒞 .idn x

-- Univalent Categories

record isUnivalent {ℓ ℓ'} (𝒞 : Precategory ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
  field
    univ : (x y : 𝒞 .ob) → isEquiv (pathToIso {𝒞 = 𝒞} x y)

open isUnivalent public

-- Opposite Categories

_^op : ∀ {ℓ ℓ'} → Precategory ℓ ℓ' → Precategory ℓ ℓ'
(𝒞 ^op) .ob = 𝒞 .ob
(𝒞 ^op) .hom x y = 𝒞 .hom y x
(𝒞 ^op) .idn = 𝒞 .idn
(𝒞 ^op) .seq f g = 𝒞 .seq g f
(𝒞 ^op) .seq-λ = 𝒞 .seq-ρ
(𝒞 ^op) .seq-ρ = 𝒞 .seq-λ
(𝒞 ^op) .seq-α f g h = sym (𝒞 .seq-α _ _ _)

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


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

open import lib.Basics
open import lib.NType2
open import lib.types.Nat
open import lib.types.TLevel
open import lib.types.Empty
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Truncation
open import lib.types.Pointed
open import lib.types.Group
open import lib.types.LoopSpace
open import lib.groups.TruncationGroup
open import lib.groups.GroupProduct
open import lib.groups.Homomorphisms
open import lib.groups.Unit

module lib.groups.HomotopyGroup where

{- Higher homotopy groups -}
module _ {i} where

  π : (n : ℕ) (t : n ≠ O) (X : Ptd i) → Group i
  π n t X = Trunc-Group (Ω^-group-structure n t X)

  fundamental-group : (X : Ptd i) → Group i
  fundamental-group X = π 1 (ℕ-S≠O _) X

{- π_(n+1) of a space is π_n of its loop space -}
abstract
  π-inner-iso : ∀ {i} (n : ℕ) (tn : n ≠ 0) (tsn : S n ≠ 0) (X : Ptd i)
    → π (S n) tsn X == π n tn (⊙Ω X)
  π-inner-iso O tn tsn X = ⊥-rec (tn idp)
  π-inner-iso (S n') tn' tn X = group-ua
    (record {
       f = Trunc-fmap (Ω^-inner-out n X);
       pres-comp =
         Trunc-elim (λ _ → Π-level (λ _ → =-preserves-level _ Trunc-level))
           (λ p → Trunc-elim (λ _ → =-preserves-level _ Trunc-level)
              (λ q → ap [_] (Ω^-inner-out-conc^ n tn' X p q)))} ,
     is-equiv-Trunc ⟨0⟩ (Ω^-inner-out n X) (Ω^-inner-is-equiv n X))
    where
    n : ℕ
    n = S n'

{- We can shift the truncation inside the loop in the definition of π -}
module _ {i} where

  private
    record Ω^Ts-PreIso (m : ℕ₋₂) (n : ℕ) (k : ℕ₋₂) (t : n ≠ O) (X : Ptd i)
      : Type i where
      field
        F : fst (⊙Ω^ n (⊙Trunc k X) ⊙→ ⊙Trunc m (⊙Ω^ n X))
        pres-comp : ∀ (p q : Ω^ n (⊙Trunc k X))
          → fst F (conc^ n t p q) == Trunc-fmap2 (conc^ n t) (fst F p) (fst F q)
        e : is-equiv (fst F)

    Ω^-Trunc-shift-preiso : (n : ℕ) (m : ℕ₋₂) (t : n ≠ O) (X : Ptd i)
      → Ω^Ts-PreIso m n ((n -2) +2+ m) t X
    Ω^-Trunc-shift-preiso O m t X = ⊥-rec (t idp)
    Ω^-Trunc-shift-preiso (S O) m _ X =
      record { F = (–> (Trunc=-equiv [ snd X ] [ snd X ]) , idp);
               pres-comp = Trunc=-∙-comm;
               e = snd (Trunc=-equiv [ snd X ] [ snd X ]) }
    Ω^-Trunc-shift-preiso (S (S n)) m t X =
      let
        r : Ω^Ts-PreIso (S m) (S n) ((S n -2) +2+ S m) (ℕ-S≠O _) X
        r = Ω^-Trunc-shift-preiso (S n) (S m) (ℕ-S≠O _) X

        H = (–> (Trunc=-equiv [ idp^ (S n) ] [ idp^ (S n) ]) , idp)
        G = ap^ 1 (Ω^Ts-PreIso.F r)
      in
      transport (λ k → Ω^Ts-PreIso m (S (S n)) k t X)
        (+2+-βr (S n -2) m)
        (record {
           F = H ⊙∘ G;
           pres-comp = λ p q →
             ap (fst H) (ap^-conc^ 1 (ℕ-S≠O _) (Ω^Ts-PreIso.F r) p q)
             ∙ (Trunc=-∙-comm (fst G p) (fst G q));
           e = snd (Trunc=-equiv [ idp^ (S n) ] [ idp^ (S n) ]
                    ∘e equiv-ap^ 1 (Ω^Ts-PreIso.F r) (Ω^Ts-PreIso.e r))})

  π-Trunc-shift-iso : (n : ℕ) (t : n ≠ O) (X : Ptd i)
    → Ω^-Group n t (⊙Trunc ⟨ n ⟩ X) Trunc-level == π n t X
  π-Trunc-shift-iso n t X = group-ua (group-hom (fst F) pres-comp , e)
    where
    n-eq : ∀ (n : ℕ) → (n -2) +2+ ⟨0⟩ == ⟨ n ⟩
    n-eq O = idp
    n-eq (S n) = ap S (n-eq n)

    r = transport (λ k → Ω^Ts-PreIso ⟨0⟩ n k t X)
                  (n-eq n) (Ω^-Trunc-shift-preiso n ⟨0⟩ t X)
    open Ω^Ts-PreIso r

abstract
  π-below-trunc : ∀ {i} (n : ℕ) (t : n ≠ O) (m : ℕ₋₂) (X : Ptd i)
    → (⟨ n ⟩ ≤T m) → π n t (⊙Trunc m X) == π n t X
  π-below-trunc n t m X lte =
    π n t (⊙Trunc m X)
      =⟨ ! (π-Trunc-shift-iso n t (⊙Trunc m X)) ⟩
    Ω^-Group n t (⊙Trunc ⟨ n ⟩ (⊙Trunc m X)) Trunc-level
      =⟨ lemma ⟩
    Ω^-Group n t (⊙Trunc ⟨ n ⟩ X) Trunc-level
      =⟨ π-Trunc-shift-iso n t X ⟩
    π n t X ∎
    where
    lemma : Ω^-Group n t (⊙Trunc ⟨ n ⟩ (⊙Trunc m X)) Trunc-level
         ==  Ω^-Group n t (⊙Trunc ⟨ n ⟩ X) Trunc-level
    lemma = ap (uncurry $ Ω^-Group n t) $
      pair=
        (⊙ua (fuse-Trunc (fst X) ⟨ n ⟩ m) idp ∙
         ap (λ k → ⊙Trunc k X) (minT-out-l lte))
        (prop-has-all-paths-↓ has-level-is-prop)

  π-above-trunc : ∀ {i} (n : ℕ) (t : n ≠ O) (m : ℕ₋₂) (X : Ptd i)
    → (m <T ⟨ n ⟩) → π n t (⊙Trunc m X) == 0ᴳ
  π-above-trunc n t m X lt =
    π n t (⊙Trunc m X)
      =⟨ ! (π-Trunc-shift-iso n t (⊙Trunc m X)) ⟩
    Ω^-Group n t (⊙Trunc ⟨ n ⟩ (⊙Trunc m X)) Trunc-level
      =⟨ contr-is-0ᴳ _ $ inhab-prop-is-contr
           (Group.ident (Ω^-Group n t (⊙Trunc ⟨ n ⟩ (⊙Trunc m X)) Trunc-level))
           (Ω^-level-in ⟨-1⟩ n _ $ Trunc-preserves-level ⟨ n ⟩ $
             raise-level-≤T
               (transport (λ k → m ≤T k) (+2+-comm ⟨-1⟩ (n -2)) (<T-to-≤T lt))
               (Trunc-level {n = m})) ⟩
    0ᴳ ∎

  π-above-level : ∀ {i} (n : ℕ) (t : n ≠ O) (m : ℕ₋₂) (X : Ptd i)
    → (m <T ⟨ n ⟩) → has-level m (fst X)
    → π n t X == 0ᴳ
  π-above-level n t m X lt pX =
    ap (π n t) (! (⊙ua (unTrunc-equiv _ pX) idp))
    ∙ π-above-trunc n t m X lt

{- πₙ(X × Y) == πₙ(X) × πₙ(Y) -}
module _ {i j} (n : ℕ) (t : n ≠ O) (X : Ptd i) (Y : Ptd  j) where

  π-× : π n t (X ⊙× Y) == π n t X ×ᴳ π n t Y
  π-× =
    group-ua (Trunc-Group-iso f pres-comp (is-eq f g f-g g-f))
    ∙ Trunc-Group-× _ _
    where
    f : Ω^ n (X ⊙× Y) → Ω^ n X × Ω^ n Y
    f r = (fst (ap^ n ⊙fst) r , fst (ap^ n ⊙snd) r)

    g : Ω^ n X × Ω^ n Y → Ω^ n (X ⊙× Y)
    g = fst (ap2^ n (⊙idf _))

    f-g : (s : Ω^ n X × Ω^ n Y) → f (g s) == s
    f-g (p , q) = pair×=
      (app= (ap fst (ap^-ap2^ n ⊙fst (⊙idf _) ∙ ap2^-fst n)) (p , q))
      (app= (ap fst (ap^-ap2^ n ⊙snd (⊙idf _) ∙ ap2^-snd n)) (p , q))

    g-f : (r : Ω^ n (X ⊙× Y)) → g (f r) == r
    g-f = app= $ ap fst $
      ap (λ h → h ⊙∘ ⊙diag) (ap2^-ap^ n (⊙idf _) ⊙fst ⊙snd)
      ∙ ap2^-diag n (⊙idf _ ⊙∘ pair⊙→ ⊙fst ⊙snd)
      ∙ ap^-idf n

    pres-comp : (p q : Ω^ n (X ⊙× Y))
      → f (conc^ n t p q) == (conc^ n t (fst (f p)) (fst (f q)) ,
                              conc^ n t (snd (f p)) (snd (f q)))
    pres-comp p q = pair×= (ap^-conc^ n t ⊙fst p q) (ap^-conc^ n t ⊙snd p q)

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
module Issue2579.Import where

record Wrap (A : Set) : Set where
  constructor wrap
  field wrapped : A