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

-- Properties of F<:⁻
--
-- This file shows several structural properties of F<:⁻, including weakening,
-- narrowing and transitivity. They are not used anywhere, but just serve as a
-- reference to compare the complexity with the corresponding proofs of D<:.
module FsubMinus2 where

open import Data.List as List
open import Data.Nat
open import Data.Maybe as Maybe
open import Data.Product
open import Data.Sum
open import Function
open import Data.Empty renaming (⊥ to False)

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as ≡

open import Data.Nat.Properties as ℕₚ
open import Data.Maybe.Properties as Maybeₚ
open import Utils
open import FsubMinus
open import Data.List.Properties as Listₚ

open import Induction.Nat

open FsubMinus.FsubMinus

infixl 7 _⇑

Γ-⇑ : Env → Ftyp → Ftyp
Γ-⇑ Γ = _↑ length Γ

_⇑ : Env → Env
[] ⇑      = []
(T ∷ Γ) ⇑ = Γ-⇑ Γ T ∷ Γ ⇑

↑-↑-comm : ∀ T m n → m ≤ n → T ↑ m ↑ suc n ≡ T ↑ n ↑ m
↑-↑-comm ⊤ m n m≤n                                  = refl
↑-↑-comm (var x) m n m≤n with n ≤? x
... | yes n≤x
  rewrite ≤?-yes $ ≤-step $ ≤-trans m≤n n≤x
        | ≤?-yes $ ≤-trans m≤n n≤x
        | ≤?-yes n≤x                                = refl
... | no x<n with m ≤? x
...             | yes m≤x rewrite proj₂ $ ≤?-no x<n = refl
...             | no x<m with suc n ≤? x
...                         | yes 1+n≤x             = ⊥-elim $ x<m (≤-trans (≤-step m≤n) 1+n≤x)
...                         | no x<1+n              = refl
↑-↑-comm (Π<: S ∙ U) m n m≤n
  rewrite ↑-↑-comm S m n m≤n
        | ↑-↑-comm U (suc m) (suc n) (s≤s m≤n)      = refl

<:∈-weakening-≤ : ∀ {x T Γ} →
                  x <: T ∈ Γ →
                  ∀ Γ₁ Γ₂ T′ →
                  Γ ≡ Γ₁ ‣ Γ₂ →
                  length Γ₂ ≤ x →
                  suc x <: Γ-⇑ Γ₂ T ∈ Γ₁ ‣ T′ ! ‣ Γ₂ ⇑
<:∈-weakening-≤ hd Γ₁ [] T′ refl l≤x       = tl hd
<:∈-weakening-≤ hd Γ₁ (_ ∷ Γ₂) T′ eq ()
<:∈-weakening-≤ (tl <:∈) Γ₁ [] T′ refl l≤x = tl (tl <:∈)
<:∈-weakening-≤ (tl {T = T} <:∈) Γ₁ (_ ∷ Γ₂) T′ refl (s≤s l≤x)
  rewrite ↑-↑-comm T 0 (length Γ₂) z≤n     = tl $ <:∈-weakening-≤ <:∈ Γ₁ Γ₂ T′ refl l≤x

<:∈-weakening-> : ∀ {x T Γ} →
                  x <: T ∈ Γ →
                  ∀ Γ₁ Γ₂ T′ →
                  Γ ≡ Γ₁ ‣ Γ₂ →
                  length Γ₂ > x →
                  x <: Γ-⇑ Γ₂ T ∈ Γ₁ ‣ T′ ! ‣ Γ₂ ⇑
<:∈-weakening-> hd Γ₁ [] T′ eq ()
<:∈-weakening-> hd Γ₁ (T ∷ Γ₂) T′ refl l>x
  rewrite ↑-↑-comm T 0 (length Γ₂) z≤n = hd
<:∈-weakening-> (tl <:∈) Γ₁ [] T′ eq ()
<:∈-weakening-> (tl {T = T} <:∈) Γ₁ (_ ∷ Γ₂) T′ refl (s≤s l>x)
  rewrite ↑-↑-comm T 0 (length Γ₂) z≤n = tl $ <:∈-weakening-> <:∈ Γ₁ Γ₂ T′ refl l>x

<:∈-weakening : ∀ {x T Γ} →
                  x <: T ∈ Γ →
                  ∀ Γ₁ Γ₂ T′ →
                  Γ ≡ Γ₁ ‣ Γ₂ →
                  ↑-idx x (length Γ₂) <: Γ-⇑ Γ₂ T ∈ Γ₁ ‣ T′ ! ‣ Γ₂ ⇑
<:∈-weakening {x} <:∈ Γ₁ Γ₂ T′ eq with length Γ₂ ≤? x
... | yes p = <:∈-weakening-≤ <:∈ Γ₁ Γ₂ T′ eq p
... | no ¬p = <:∈-weakening-> <:∈ Γ₁ Γ₂ T′ eq (≰⇒> ¬p)

<:-weakening-gen : ∀ {Γ S U} →
              Γ ⊢F S <: U →
              ∀ Γ₁ Γ₂ T →
                Γ ≡ Γ₁ ‣ Γ₂ →
                Γ₁ ‣ T ! ‣ Γ₂ ⇑ ⊢F Γ-⇑ Γ₂ S <: Γ-⇑ Γ₂ U
<:-weakening-gen ftop Γ₁ Γ₂ T eq = ftop
<:-weakening-gen (fvrefl {_} {x}) Γ₁ Γ₂ T eq
  rewrite ↑-var x (length Γ₂)    = fvrefl
<:-weakening-gen (fbinds {_} {x} T∈Γ D) Γ₁ Γ₂ T eq
  rewrite ↑-var x (length Γ₂)    = fbinds (<:∈-weakening T∈Γ Γ₁ Γ₂ T eq)
                                          (<:-weakening-gen D Γ₁ Γ₂ T eq)
<:-weakening-gen (fall {S₂ = S₂} Dp Db) Γ₁ Γ₂ T eq
  = fall (<:-weakening-gen Dp Γ₁ Γ₂ T eq)
         (<:-weakening-gen Db Γ₁ (Γ₂ ‣ S₂ !) T (cong (S₂ ∷_) eq))

<:-weakening : ∀ {S U} Γ₁ Γ₂ T →
              Γ₁ ‣ Γ₂ ⊢F S <: U →
              Γ₁ ‣ T ! ‣ Γ₂ ⇑ ⊢F Γ-⇑ Γ₂ S <: Γ-⇑ Γ₂ U
<:-weakening _ _ T D = <:-weakening-gen D _ _ T refl

<:-weakening-hd : ∀ {Γ S U} T →
                 Γ ⊢F S <: U →
                 Γ ‣ T ! ⊢F S ↑ 0 <: U ↑ 0
<:-weakening-hd T D = <:-weakening _ [] T D

<:-weakening′ : ∀ {Γ S U} Γ′ →
               Γ ⊢F S <: U →
               Γ ‣ Γ′ ⊢F repeat (length Γ′) (_↑ 0) S <: repeat (length Γ′) (_↑ 0) U
<:-weakening′ [] D       = D
<:-weakening′ (T ∷ Γ′) D = <:-weakening-hd T $ <:-weakening′ Γ′ D

<:-refl : ∀ Γ T → Γ ⊢F T <: T
<:-refl Γ ⊤           = ftop
<:-refl Γ (var x)     = fvrefl
<:-refl Γ (Π<: S ∙ U) = fall (<:-refl Γ S) (<:-refl (S ∷ Γ) U)

module TransProof where
  open ≤-Reasoning

  <:∈-find : ∀ {x T Γ} →
               x <: T ∈ Γ →
               ∀ T₁ T₂ Γ₁ Γ₂ →
                 Γ ≡ Γ₁ ‣ T₁ ! ‣ Γ₂ →
                 x ≢ length Γ₂ × x <: T ∈ Γ₁ ‣ T₂ ! ‣ Γ₂ ⊎
                 x ≡ length Γ₂ × T ≡ repeat (suc (length Γ₂)) (_↑ 0) T₁ ×
                 x <: repeat (suc (length Γ₂)) (_↑ 0) T₂ ∈ Γ₁ ‣ T₂ ! ‣ Γ₂
  <:∈-find hd T₁ T₂ Γ₁ [] refl       = inj₂ (refl , refl , hd)
  <:∈-find hd T₁ T₂ Γ₁ (_ ∷ Γ₂) refl = inj₁ ((λ ()) , hd)
  <:∈-find (tl <:∈) T₁ T₂ Γ₁ [] refl = inj₁ ((λ ()) , tl <:∈)
  <:∈-find (tl <:∈) T₁ T₂ Γ₁ (_ ∷ Γ₂) refl with <:∈-find <:∈ T₁ T₂ Γ₁ Γ₂ refl
  ... | inj₁ (n≢l , r)               = inj₁ ((λ n≡l → n≢l (suc-injective n≡l)) , tl r)
  ... | inj₂ (n≡l , e , r)           = inj₂ (cong suc n≡l , cong (_↑ 0) e , tl r)

  infix 4 _≺:[_]_
  data _≺:[_]_ : Env → ℕ → Env → Set where
    ≺[_,_] : ∀ {Γ U} S → Γ ⊢F S <: U → Γ ‣ S ! ≺:[ 0 ] Γ ‣ U !
    _∷_    : ∀ {Γ₁ n Γ₂} T → Γ₁ ≺:[ n ] Γ₂ → Γ₁ ‣ T ! ≺:[ suc n ] Γ₂ ‣ T !

  <:∈-find′ : ∀ {x T Γ Γ′ n} →
               x <: T ∈ Γ →
               Γ′ ≺:[ n ] Γ →
               x ≡ n × (∃ λ T′ → n <: T′ ∈ Γ′ × Γ′ ⊢F T′ <: T) ⊎ x ≢ n × x <: T ∈ Γ′
  <:∈-find′ hd ≺[ T′ , T′<:T ]          = inj₁ (refl , T′ ↑ 0 , hd , <:-weakening-hd T′ T′<:T)
  <:∈-find′ hd (T ∷ Γ′≺:Γ)              = inj₂ ((λ ()) , hd)
  <:∈-find′ (tl T∈Γ) ≺[ T′ , T′<:T ]    = inj₂ ((λ ()) , tl T∈Γ)
  <:∈-find′ (tl T∈Γ) (S ∷ Γ′≺:Γ) with <:∈-find′ T∈Γ Γ′≺:Γ
  ... | inj₁ (x≡n , T′ , T′∈Γ′ , T′<:T) = inj₁ (cong suc x≡n , T′ ↑ 0 , tl T′∈Γ′ , <:-weakening-hd S T′<:T)
  ... | inj₂ (x≢n , T∈Γ′)               = inj₂ (x≢n ∘ suc-injective , tl T∈Γ′)

  trans-on : Ftyp → Set
  trans-on T = ∀ {Γ S U} → Γ ⊢F S <: T → Γ ⊢F T <: U → Γ ⊢F S <: U

  narrow-on : Ftyp → Set
  narrow-on T = ∀ {Γ Γ′ n S U} →
                  Γ ⊢F S <: U →
                  Γ′ ≺:[ n ] Γ →
                  n <: T ∈ Γ →
                  Γ′ ⊢F S <: U

  <:-trans-rec : ∀ T → (∀ T′ → Ftyp-measure T′ < Ftyp-measure T → trans-on T′ × narrow-on T′) → trans-on T
  <:-trans-rec ⊤ rec S<:T ftop                                 = S<:T
  <:-trans-rec (var x) rec S<:T ftop                           = ftop
  <:-trans-rec (var x) rec S<:T fvrefl                         = S<:T
  <:-trans-rec (var x) rec fvrefl (fbinds T∈Γ T<:U)            = fbinds T∈Γ T<:U
  <:-trans-rec (var x) rec (fbinds S∈Γ S<:T) (fbinds T∈Γ T<:U) = fbinds S∈Γ (<:-trans-rec (var x) rec S<:T (fbinds T∈Γ T<:U))
  <:-trans-rec (Π<: S ∙ U) rec S<:T ftop                       = ftop
  <:-trans-rec (Π<: S ∙ U) rec (fbinds S∈Γ S<:T) (fall Db Dp)  = fbinds S∈Γ (<:-trans-rec (Π<: S ∙ U) rec S<:T (fall Db Dp))
  <:-trans-rec (Π<: S ∙ U) rec (fall Dp₁ Db₁) (fall Dp₂ Db₂)   = fall (<:-trans-rec S (λ T′ T′<:S → rec T′ (≤-stepsʳ _ T′<:S)) Dp₂ Dp₁)
                                                                      (<:-trans-rec U
                                                                                (λ T′ T′<U → rec T′ (≤-trans T′<U (≤-stepsˡ _ ≤-refl)))
                                                                                (proj₂ (rec (S ↑ 0) S↑0<SU) Db₁ ≺[ _ , Dp₂ ] hd)
                                                                                Db₂)
    where S↑0<SU : Ftyp-measure (S ↑ 0) < Ftyp-measure S + Ftyp-measure U
          S↑0<SU = begin-strict
            Ftyp-measure (S ↑ 0)            ≡⟨ Ftyp-measure-↑ S 0 ⟩
            Ftyp-measure S                  <⟨ ≤-refl ⟩
            1 + Ftyp-measure S              ≡⟨ sym (+-comm _ 1) ⟩
            Ftyp-measure S + 1              ≤⟨ +-monoʳ-≤ _ (Ftyp-measure≥1 U) ⟩
            Ftyp-measure S + Ftyp-measure U ∎

  <:-narrowing-rec : ∀ T → (∀ T′ → Ftyp-measure T′ ≤ Ftyp-measure T → trans-on T′) → narrow-on T
  <:-narrowing-rec T trans ftop Γ′≺:Γ T∈Γ         = ftop
  <:-narrowing-rec T trans fvrefl Γ′≺:Γ T∈Γ       = fvrefl
  <:-narrowing-rec T trans (fbinds S∈Γ S<:U) Γ′≺:Γ T∈Γ with <:∈-find′ S∈Γ Γ′≺:Γ
  ... | inj₁ (refl , T′ , T′∈Γ′ , T′<:T)
    rewrite <:∈-func S∈Γ T∈Γ                      = fbinds T′∈Γ′ (trans T ≤-refl
                                                                          T′<:T
                                                                          (<:-narrowing-rec T trans S<:U Γ′≺:Γ T∈Γ))
  ... | inj₂ (x≢n , T′∈Γ′)                        = fbinds T′∈Γ′ (<:-narrowing-rec T trans S<:U Γ′≺:Γ T∈Γ)
  <:-narrowing-rec T trans (fall Dp Db) Γ′≺:Γ T∈Γ = fall (<:-narrowing-rec T trans Dp Γ′≺:Γ T∈Γ)
                                                         (<:-narrowing-rec (T ↑ 0)
                                                                           (λ T′ → trans T′ ∘ T′≤T T′)
                                                                           Db (_ ∷ Γ′≺:Γ) (tl T∈Γ))
    where T′≤T : ∀ T′ → Ftyp-measure T′ ≤ Ftyp-measure (T ↑ 0) → Ftyp-measure T′ ≤ Ftyp-measure T
          T′≤T T′ T′≤T↑0 = begin
            Ftyp-measure T′      ≤⟨ T′≤T↑0 ⟩
            Ftyp-measure (T ↑ 0) ≡⟨ Ftyp-measure-↑ T 0 ⟩
            Ftyp-measure T       ∎

  <:-trans-narrow : ∀ T → trans-on T × narrow-on T
  <:-trans-narrow = wfRec (λ T → trans-on T × narrow-on T)
                          λ T rec →
                            <:-trans-rec T rec ,
                            <:-narrowing-rec T λ T′ T′≤T →
                                                 <:-trans-rec T′ λ T″ T″<T′ →
                                                                   rec T″ (≤-trans T″<T′ T′≤T)
    where open Measure <-wellFounded Ftyp-measure

  <:-trans : ∀ {T} → trans-on T
  <:-trans {T} = proj₁ $ <:-trans-narrow T

  <:-narrow : ∀ {T} → narrow-on T
  <:-narrow {T} = proj₂ $ <:-trans-narrow T

<:-weakening-size-gen : ∀ {Γ S U} →
                          (S<:U : Γ ⊢F S <: U) →
                          ∀ Γ₁ Γ₂ T →
                            (eq : Γ ≡ Γ₁ ‣ Γ₂) →
                            F-measure S<:U ≡ F-measure (<:-weakening-gen S<:U Γ₁ Γ₂ T eq)
<:-weakening-size-gen ftop Γ₁ Γ₂ T eq = refl
<:-weakening-size-gen (fvrefl {_} {x}) Γ₁ Γ₂ T eq
  rewrite ↑-var x (length Γ₂)         = refl
<:-weakening-size-gen (fbinds {_} {x} S∈Γ D) Γ₁ Γ₂ T eq
  rewrite ↑-var x (length Γ₂)         = cong suc (<:-weakening-size-gen D Γ₁ Γ₂ T eq)
<:-weakening-size-gen (fall {S₂ = S} Dp Db) Γ₁ Γ₂ T eq
  = cong suc (cong₂ _+_ (<:-weakening-size-gen Dp Γ₁ Γ₂ T eq)
                        (<:-weakening-size-gen Db Γ₁ (S ∷ Γ₂) T (cong (S ∷_) eq)))

open TransProof using (<:-trans ; <:-narrow) public


text:
module Categories where

infix 10 _≡_

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

trans : forall {A B C}{a : A}{b : B}{c : C} -> a ≡ b -> b ≡ c -> a ≡ c
trans refl p = p

sym : forall {A B}{a : A}{b : B} -> a ≡ b -> b ≡ a
sym refl = refl

resp : forall {A}{B : A -> Set}{a a' : A} ->
       (f : (a : A) -> B a) -> a ≡ a' -> f a ≡ f a'
resp f refl = refl

record Cat : Set1 where
  field Obj : Set
        Hom : Obj -> Obj -> Set
        id : forall X -> Hom X X
        _○_ : forall {X Y Z} -> Hom Y Z -> Hom X Y -> Hom X Z
        idl : forall {X Y}{f : Hom X Y} -> id Y ○ f ≡ f
        idr : forall {X Y}{f : Hom X Y} -> f ○ id X ≡ f
        assoc : forall {W X Y Z}{f : Hom W X}{g : Hom X Y}{h : Hom Y Z} ->
                (h ○ g) ○ f ≡ h ○ (g ○ f)

open Cat

record Functor (C D : Cat) : Set where
  field Fun : Obj C -> Obj D
        map : forall {X Y} -> (Hom C X Y) -> Hom D (Fun X) (Fun Y)
        mapid : forall {X} -> map (id C X) ≡ id D (Fun X)
        map○ : forall {X Y Z}{f : Hom C X Y}{g : Hom C Y Z} ->
               map (_○_ C g f) ≡ _○_ D (map g) (map f)

open Functor

idF : forall C -> Functor C C
idF C = record {Fun = \x -> x; map = \x -> x; mapid = refl; map○ = refl}

_•_ : forall {C D E} -> Functor D E -> Functor C D -> Functor C E
F • G = record {Fun = \X -> Fun F (Fun G X);
                 map = \f -> map F (map G f);
                 mapid = trans (resp (\x -> map F x) (mapid G)) (mapid F);
                 map○ = trans (resp (\x -> map F x) (map○ G)) (map○ F)}

record Nat {C D : Cat} (F G : Functor C D) : Set where
  field η : (X : Obj C) -> Hom D (Fun F X) (Fun G X)
        law : {X Y : Obj C}{f : Hom C X Y} ->
              _○_ D (η Y) (map F f) ≡ _○_ D (map G f) (η X)

open Nat

_▪_ : forall {C D : Cat}{F G H : Functor C D} -> Nat G H -> Nat F G -> Nat F H
_▪_ {D = D} A B =
  record {
    η = \X -> _○_ D (η A X) (η B X);
    law = \{X}{Y} ->
      trans (assoc D)
            (trans (resp (\f -> _○_ D (η A Y) f) (law B))
                   (trans (sym (assoc D))
                          (trans (resp (\g -> _○_ D g (η B X)) (law A))
                                 (assoc D))))
  }

ext: agda

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
------------------------------------------------------------------------
-- Pointers to results from the paper
------------------------------------------------------------------------

-- Note that this is a version of the code that does not quite match
-- the description in the paper. See README for some discussion of the
-- changes.

{-# OPTIONS --cubical --sized-types #-}

module README.Pointers-to-results-from-the-paper where

-- Library code.

import Delay-monad
import Delay-monad.Bisimilarity
import Delay-monad.Bisimilarity.Alternative
import Delay-monad.Monad
import Delay-monad.Partial-order
import Delay-monad.Termination
import Equality.Propositional as Equality
import Interval
import H-level.Truncation.Propositional as Truncation
import Quotient
import Univalence-axiom

-- Code from this development.

import Delay-monad.Alternative
import Delay-monad.Alternative.Equivalence
import Delay-monad.Alternative.Partial-order
import Delay-monad.Alternative.Termination
import Delay-monad.Alternative.Weak-bisimilarity
import Lifting
import Partiality-algebra
import Partiality-algebra.Category
import Partiality-algebra.Eliminators
import Partiality-algebra.Fixpoints
import Partiality-algebra.Pi
import Partiality-monad.Coinductive.Alternative
import Partiality-monad.Inductive as Partiality-monad
import Partiality-monad.Inductive.Alternative-order as Alternative-order
import Partiality-monad.Inductive.Eliminators
import Partiality-monad.Inductive.Fixpoints
import Partiality-monad.Inductive.Monad as Monad
import Partiality-monad.Inductive.Monad.Adjunction as Adjunction
import Partiality-monad.Equivalence
import README.Lambda
import Search

------------------------------------------------------------------------
-- Section 2

-- Note that most of the following definitions are taken from a
-- library.

-- Extensionality for functions.

Extensionality = Equality.Extensionality
ext            = Interval.ext

-- Strong bisimilarity implies equality for the delay monad.

Delay-ext = Delay-monad.Bisimilarity.Extensionality

-- The property of being a set.

Is-set = Equality.Is-set

-- The property of being a proposition.

Is-proposition = Equality.Is-proposition

-- Propositional extensionality.

Propositional-extensionality =
  Univalence-axiom.Propositional-extensionality

-- The univalence axiom.

Univalence = Univalence-axiom.Univalence

-- Quotient types.

import Quotient

-- Countable choice.

Countable-choice = Truncation.Axiom-of-countable-choice

------------------------------------------------------------------------
-- Section 3.1

-- Definition 1: Partiality algebras and partiality algebra morphisms.
-- The function η is called now and ⊥ is called never.

Partiality-algebra = Partiality-algebra.Partiality-algebra
Morphism           = Partiality-algebra.Morphism

-- An identity morphism.

id = Partiality-algebra.id

-- Composition of morphisms.

_∘_ = Partiality-algebra._∘_

-- Partiality algebras form a category.

category = Partiality-algebra.Category.category

-- The partiality monad, defined as a QIIT. (The proof α is called
-- antisymmetry.)

_⊥ = Partiality-monad._⊥

-- A partiality algebra for the partiality monad.

partiality-monad = Partiality-monad.partiality-algebra

-- Initiality.

Initial = Partiality-algebra.Eliminators.Initial

-- Theorem 2.

Induction-principle =
  Partiality-algebra.Eliminators.Elimination-principle
universality-to-induction =
  Partiality-algebra.Eliminators.∀initiality→∀eliminators
induction-to-universality =
  Partiality-algebra.Eliminators.∀eliminators→∀initiality

-- The partiality monad's induction principle.

induction-principle = Partiality-monad.eliminators

-- A proof that shows that A ⊥ is a set without making use of the
-- set-truncation "constructor".

T-is-set = Partiality-algebra.Partiality-algebra-with.T-is-set

-- Lemma 3.

lemma-3 = Partiality-monad.Inductive.Eliminators.⊥-rec-⊥

------------------------------------------------------------------------
-- Section 3.2

-- Definition 4: The category ω-CPO of pointed ω-cpos.

ω-CPO = Adjunction.ω-CPPO
ω-cpo = Adjunction.ω-cppo

-- The forgetful functor U from ω-CPO (and in fact Part_A for any A)
-- to SET.

U = Adjunction.Forget

-- The functor F from SET to ω-CPO.

F = Adjunction.Partial

-- Theorem 5.

theorem-5 = Adjunction.Partial⊣Forget

-- Corollary 6.

corollary-6 = Adjunction.Partiality-monad

-- A direct construction of a monad structure on _⊥.

μ                 = Monad.join
module Monad-laws = Monad.Monad-laws

------------------------------------------------------------------------
-- Section 3.3

-- Lemma 7. For the second part the code uses a propositional
-- truncation that is not present in the paper: the result proved in
-- the code is more general, and works even if the type "A" is not a
-- set.

lemma-7-part-1 = Alternative-order.now⊑never≃⊥
lemma-7-part-2 = Alternative-order.now⊑now≃∥≡∥
lemma-7-part-3 = Alternative-order.now⊑⨆≃∥∃now⊑∥

-- Corollary 8. For the second part the code uses a propositional
-- truncation that is not present in the paper: the result proved in
-- the code is more general, and works even if the type "A" is not a
-- set.

corollary-8-part-1 = Alternative-order.now⊑→⇓
corollary-8-part-2 = Alternative-order.now≡now≃∥≡∥
corollary-8-part-3 = Alternative-order.now≢never

-- The order is flat.

flat-order = Alternative-order.flat-order

------------------------------------------------------------------------
-- Section 4, not including Sections 4.1 and 4.2

-- Definition 9: The delay monad and weak bisimilarity. The definition
-- of _↓_ is superficially different from the one in the paper. The
-- first definition of weak bisimilarity, _∼D_, is different from the
-- one in the paper, but is logically equivalent to the second one,
-- _∼D′_, which is closer to the paper's definition.

Delay  = Delay-monad.Delay
_↓D_   = Delay-monad.Termination._⇓_
_∼D_   = Delay-monad.Bisimilarity._≈_
_∼D′_  = Delay-monad.Bisimilarity.Alternative._≈₂_
∼D⇔∼D′ = Delay-monad.Partial-order.≈⇔≈₂

-- The delay monad is a monad.

Delay-monad = Delay-monad.Monad.delay-monad

-- The relation _↓D_ is pointwise propositional (when the type "A" is
-- a set).

↓D-propositional = Delay-monad.Termination.Terminates-propositional

-- The relation _∼D′_ is pointwise propositional (when the type "A" is
-- a set).

∼D′-propositional =
  Delay-monad.Bisimilarity.Alternative.≈₂-propositional

-- _∼D_ is an equivalence relation.

∼D-reflexive  = Delay-monad.Bisimilarity.reflexive
∼D-symmetric  = Delay-monad.Bisimilarity.symmetric
∼D-transitive = Delay-monad.Bisimilarity.transitive-≈

------------------------------------------------------------------------
-- Section 4.1

-- The predicate is-mon.

is-mon = Delay-monad.Alternative.Increasing

-- Monotone sequences.

Seq = Delay-monad.Alternative.Delay

-- Lemma 10.

lemma-10 = Delay-monad.Alternative.Equivalence.Delay↔Delay

-- The relation ↓_Seq.

_↓-Seq_ = Delay-monad.Alternative.Termination._⇓_

-- This relation is pointwise logically equivalent to a
-- propositionally truncated variant (when the type "A" is a set).

↓-Seq⇔∥↓-Seq∥ = Delay-monad.Alternative.Termination.⇓⇔∥⇓∥

-- The relation ⊑_Seq.

_⊑-Seq_ = Delay-monad.Alternative.Partial-order._∥⊑∥_

-- This relation is pointwise propositional.

⊑-Seq-propositional =
  Delay-monad.Alternative.Partial-order.∥⊑∥-propositional

-- The relation ∼_Seq.

_∼-Seq_ = Delay-monad.Alternative.Weak-bisimilarity._≈_

-- This relation is pointwise propositional.

≈-Seq-propositional =
  Delay-monad.Alternative.Weak-bisimilarity.≈-propositional

-- Lemma 11.

lemma-11 = Partiality-monad.Coinductive.Alternative.⊥↔⊥

------------------------------------------------------------------------
-- Section 4.2

-- The function w.

w = Partiality-monad.Equivalence.Delay→⊥

-- Lemma 12.

w-monotone = Partiality-monad.Equivalence.Delay→⊥-mono
w̃          = Partiality-monad.Equivalence.⊥→⊥

-- Lemma 13.

lemma-13 = Partiality-monad.Equivalence.⊥→⊥-injective

-- Lemma 14.

lemma-14 = Partiality-monad.Equivalence.Delay→⊥-surjective

-- The function w̃ is surjective.

w̃-surjective = Partiality-monad.Equivalence.⊥→⊥-surjective

-- Theorem 15.

theorem-15-part-1 = Partiality-monad.Equivalence.⊥→⊥-equiv
theorem-15-part-2 = Partiality-monad.Equivalence.⊥≃⊥′
theorem-15-part-3 = Partiality-monad.Equivalence.⊥≃⊥

------------------------------------------------------------------------
-- Section 5.1

-- A fixpoint combinator.

fix = Partiality-algebra.Fixpoints.fix

-- If the argument is ω-continuous, then the result is a least fixed
-- point.

fixed-point = Partiality-algebra.Fixpoints.fix-is-fixpoint-combinator
least       = Partiality-algebra.Fixpoints.fix-is-least

-- A kind of dependent function space with a type as the domain and a
-- family of partiality algebras as the codomain. The result is a
-- partiality algebra.

Π = Partiality-algebra.Pi.Π

-- The search function.

module The-search-function = Search.Direct

------------------------------------------------------------------------
-- Section 5.3

-- Operational semantics.

module Operational-semantics = README.Lambda

------------------------------------------------------------------------
-- Section 6

-- A quotient inductive-inductive definition of the lifting
-- construction on ω-cpos. (This construction is based on a suggestion
-- from Paolo Capriotti.)

module Lifting-construction = Lifting

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module Cats.Category.Cones where

open import Relation.Binary using (Rel ; IsEquivalence ; _Preserves₂_⟶_⟶_)
open import Level using (_⊔_)

open import Cats.Category.Base
open import Cats.Functor using (Functor) renaming (_∘_ to _∘F_)
open import Cats.Util.Conv

import Relation.Binary.PropositionalEquality as ≡

import Cats.Category.Constructions.Iso as Iso
import Cats.Util.Function as Fun

module _ {lo la l≈ lo′ la′ l≈′}
  {J : Category lo la l≈}
  {Z : Category lo′ la′ l≈′}
  (D : Functor J Z)
  where

  infixr 9 _∘_
  infixr 4 _≈_

  private
    module Z = Category Z
    module J = Category J
    module D = Functor D

  -- We could define cones in terms of wedges (and limits in terms of ends).
  record Cone : Set (lo ⊔ la ⊔ la′ ⊔ lo′ ⊔ l≈′) where
    field
      Apex : Z.Obj
      arr : ∀ j → Apex Z.⇒ D.fobj j
      commute : ∀ {i j} (α : i J.⇒ j) → arr j Z.≈ D.fmap α Z.∘ arr i

  instance
    HasObj-Cone : HasObj Cone lo′ la′ l≈′
    HasObj-Cone = record { Cat = Z ; _ᴼ = Cone.Apex }

  Obj = Cone

  record _⇒_ (A B : Obj) : Set (lo ⊔ la′ ⊔ l≈′) where
    private
      module A = Cone A ; module B = Cone B

    field
      θ : A.Apex Z.⇒ B.Apex
      commute : ∀ j → B.arr j Z.∘ θ Z.≈ A.arr j

  instance
    HasArrow-⇒ : ∀ {A B} → HasArrow (A ⇒ B) lo′ la′ l≈′
    HasArrow-⇒ = record { Cat = Z ; _⃗ = _⇒_.θ }

  _≈_ : ∀ {A B} → Rel (A ⇒ B) l≈′
  _≈_ = Z._≈_ Fun.on _⇒_.θ

  equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
  equiv = Fun.on-isEquivalence _⇒_.θ Z.equiv

  id : ∀ {A} → A ⇒ A
  id = record
      { θ = Z.id
      ; commute = λ j → Z.id-r
      }

  _∘_ : ∀ {A B C} → B ⇒ C → A ⇒ B → A ⇒ C
  _∘_ {A} {B} {C} f g = record
      { θ = f ⃗ Z.∘ g ⃗
      ; commute = λ j →
          begin
            arr C j Z.∘ f ⃗ Z.∘ g ⃗
          ≈⟨ Z.unassoc ⟩
            (arr C j Z.∘ f ⃗) Z.∘ g ⃗
          ≈⟨ Z.∘-resp-l (commute f j) ⟩
            arr B j Z.∘ g ⃗
          ≈⟨ commute g j ⟩
            arr A j
          ∎
      }
    where
      open Cone using (arr)
      open _⇒_ using (commute)
      open Z.≈-Reasoning

  Cones : Category (lo ⊔ la ⊔ lo′ ⊔ la′ ⊔ l≈′) (lo ⊔ la′ ⊔ l≈′) l≈′
  Cones = record
      { Obj = Obj
      ; _⇒_ = _⇒_
      ; _≈_ = _≈_
      ; id = id
      ; _∘_ = _∘_
      ; equiv = equiv
      ; ∘-resp = Z.∘-resp
      ; id-r = Z.id-r
      ; id-l = Z.id-l
      ; assoc = Z.assoc
      }

  open Iso.Build Cones using (_≅_)
  open Iso.Build Z using () renaming (_≅_ to _≅Z_)

  cone-iso→obj-iso : ∀ {c d : Cone}
    → c ≅ d
    → c ᴼ ≅Z d ᴼ
  cone-iso→obj-iso i = record
      { forth = forth i ⃗
      ; back = back i ⃗
      ; back-forth = back-forth i
      ; forth-back = forth-back i
      }
    where
      open _≅_

apFunctor : ∀ {lo la l≈ lo′ la′ l≈′ lo″ la″ l≈″}
  → {Y : Category lo la l≈}
  → {Z : Category lo′ la′ l≈′}
  → (F : Functor Y Z)
  → {J : Category lo″ la″ l≈″}
  → {D : Functor J Y}
  → Cone D
  → Cone (F ∘F D)
apFunctor {Y = Y} {Z} F {J} {D} c = record
    { Apex = fobj F Apex
    ; arr = λ j → fmap F (arr j)
    ; commute = λ {i} {j} α → Z.≈.sym (
        begin
          fmap (F ∘F D) α Z.∘ fmap F (arr i)
        ≡⟨ ≡.refl ⟩
          fmap F (fmap D α) Z.∘ fmap F (arr i)
        ≈⟨ fmap-∘ F ⟩
          fmap F (fmap D α Y.∘ arr i)
        ≈⟨ fmap-resp F (Y.≈.sym (commute α)) ⟩
          fmap F (arr j)
        ∎
      )
    }
  where
    module Y = Category Y
    module Z = Category Z
    open Cone c
    open Z.≈-Reasoning
    open Functor

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


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

module Dodo.Nullary.Disjoint where

-- Stdlib imports
open import Level using (Level)
open import Data.Product using (_×_)
open import Relation.Nullary using (¬_)

-- # Definitions

Disjoint : ∀ {a b : Level} (A : Set a) (B : Set b) → Set _
Disjoint A B = ¬ (A × B)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to Linked
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.Linked.Properties where

open import Data.List hiding (any)
open import Data.List.Relation.Unary.AllPairs as AllPairs
  using (AllPairs; []; _∷_)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.Linked as Linked
  using (Linked; []; [-]; _∷_)
open import Data.Fin.Base using (Fin)
open import Data.Fin.Properties using (suc-injective)
open import Data.Nat.Base using (zero; suc; _<_; z≤n; s≤s)
open import Data.Nat.Properties using (≤-refl; ≤-pred; ≤-step)
open import Level using (Level)
open import Function using (_∘_; flip)
open import Relation.Binary using (Rel; Transitive; DecSetoid)
open import Relation.Binary.PropositionalEquality using (_≢_)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Nullary using (yes; no)

private
  variable
    a b p ℓ : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- Relationship to other predicates
------------------------------------------------------------------------

module _ {R : Rel A ℓ} where

  AllPairs⇒Linked : ∀ {xs} → AllPairs R xs → Linked R xs
  AllPairs⇒Linked []                    = []
  AllPairs⇒Linked (px ∷ [])             = [-]
  AllPairs⇒Linked ((px ∷ _) ∷ py ∷ pxs) =
    px ∷ (AllPairs⇒Linked (py ∷ pxs))

module _ {R : Rel A ℓ} (trans : Transitive R) where

  Linked⇒All : ∀ {v x xs} → R v x →
               Linked R (x ∷ xs) → All (R v) (x ∷ xs)
  Linked⇒All Rvx [-]         = Rvx ∷ []
  Linked⇒All Rvx (Rxy ∷ Rxs) = Rvx ∷ Linked⇒All (trans Rvx Rxy) Rxs

  Linked⇒AllPairs : ∀ {xs} → Linked R xs → AllPairs R xs
  Linked⇒AllPairs []          = []
  Linked⇒AllPairs [-]         = [] ∷ []
  Linked⇒AllPairs (Rxy ∷ Rxs) = Linked⇒All Rxy Rxs ∷ Linked⇒AllPairs Rxs

------------------------------------------------------------------------
-- Introduction (⁺) and elimination (⁻) rules for list operations
------------------------------------------------------------------------
-- map

module _ {R : Rel A ℓ} {f : B → A} where

  map⁺ : ∀ {xs} → Linked (λ x y → R (f x) (f y)) xs →
         Linked R (map f xs)
  map⁺ []           = []
  map⁺ [-]          = [-]
  map⁺ (Rxy ∷ Rxs)  = Rxy ∷ map⁺ Rxs

------------------------------------------------------------------------
-- applyUpTo

module _ {R : Rel A ℓ} where

  applyUpTo⁺₁ : ∀ f n → (∀ {i} → suc i < n → R (f i) (f (suc i))) →
                Linked R (applyUpTo f n)
  applyUpTo⁺₁ f zero          Rf = []
  applyUpTo⁺₁ f (suc zero)    Rf = [-]
  applyUpTo⁺₁ f (suc (suc n)) Rf =
    Rf (s≤s (s≤s z≤n)) ∷ (applyUpTo⁺₁ (f ∘ suc) (suc n) (Rf ∘ s≤s))

  applyUpTo⁺₂ : ∀ f n → (∀ i → R (f i) (f (suc i))) →
                Linked R (applyUpTo f n)
  applyUpTo⁺₂ f n Rf = applyUpTo⁺₁ f n (λ _ → Rf _)

------------------------------------------------------------------------
-- applyDownFrom

module _ {R : Rel A ℓ} where

  applyDownFrom⁺₁ : ∀ f n → (∀ {i} → suc i < n → R (f (suc i)) (f i)) →
                    Linked R (applyDownFrom f n)
  applyDownFrom⁺₁ f zero          Rf = []
  applyDownFrom⁺₁ f (suc zero)    Rf = [-]
  applyDownFrom⁺₁ f (suc (suc n)) Rf =
    Rf ≤-refl ∷ applyDownFrom⁺₁ f (suc n) (Rf ∘ ≤-step)

  applyDownFrom⁺₂ : ∀ f n → (∀ i → R (f (suc i)) (f i)) →
                    Linked R (applyDownFrom f n)
  applyDownFrom⁺₂ f n Rf = applyDownFrom⁺₁ f n (λ _ → Rf _)


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

open import HoTT
open import groups.Cokernel

{-
                 K
                 ↑
                 ╎ ψ₁
            q[_] ╎    ψ₂
   Coker ψ₂ ↞--- G ←------ L
      ↑          ↑
   φ₁ ╎          ╎ inject
      ↑          ↑
      H ↞------- Ker ψ₁
           φ₂

     Then, H ≃ᴳ Ker/Im.
-}

module groups.KernelImageUniqueFactorization {i j k l}
  {G : Group i} {H : Group j} {K : Group k} {L : Group l}
  (ψ₁ : G →ᴳ K) (ψ₂ : L →ᴳ G) (G-ab : is-abelian G)
  (φ₁ : Ker ψ₁ →ᴳ H) (φ₁-is-surj : is-surjᴳ φ₁)
  (φ₂ : H →ᴳ Coker ψ₂ G-ab) (φ₂-is-inj : is-injᴳ φ₂)
  (φ-comm : ∀ ker → GroupHom.f (φ₂ ∘ᴳ φ₁) ker == q[ fst ker ])
  where

  private
    module G = Group G
    module H = Group H
    module K = Group K
    module L = Group L
    module ψ₁ = GroupHom ψ₁
    module ψ₂ = GroupHom ψ₂
    module φ₁ = GroupHom φ₁
    module φ₂ = GroupHom φ₂

    φ₂' : H →ᴳ QuotGroup (im-npropᴳ ψ₂ G-ab)
    φ₂' = GroupIso.f-hom (Coker-β ψ₂ G-ab) ∘ᴳ φ₂

    abstract
      φ₂'-is-inj : is-injᴳ φ₂'
      φ₂'-is-inj = ∘-is-inj (–>-is-inj (GroupIso.f-equiv (Coker-β ψ₂ G-ab))) φ₂-is-inj

  open import groups.PropQuotUniqueFactorization
    (ker-propᴳ ψ₁) (im-npropᴳ ψ₂ G-ab) φ₁ φ₁-is-surj φ₂' φ₂'-is-inj φ-comm
  open import groups.KernelImage ψ₁ ψ₂ G-ab

  H-iso-Ker/Im : H ≃ᴳ Ker/Im
  H-iso-Ker/Im = Ker/Im-β ⁻¹ᴳ ∘eᴳ H-iso-P/Q

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
{-# OPTIONS --experimental-irrelevance  #-}
--{-# OPTIONS -v tc.lhs.unify:65 -v tc.irr:50 #-}
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

data D : ..(b : Bool) → Set where
  c : (b : Bool) → D b

test : ..(a : Bool) → D a → Bool
test a (c b) = b

data ⊥ : Set where
record ⊤ : Set where constructor tt

case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

-- Not so shape-irrelevant type!
T : ..(n : Bool) → Set
T n = case test n (c _) of λ where
        true  → ⊤
        false → ⊥

data Foo : Set where
  foo : .(b : Bool) → T b → Foo

bad : (b : ⊥) → foo true tt ≡ foo false b → ⊥
bad b _ = b

jackpot : ⊥
jackpot = bad _ refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Numeral.Natural.Combinatorics where

open import Numeral.Natural
open import Numeral.Natural.Oper

-- Counting combinations.
-- `𝑐𝐶 n k` is the number of ways one can pick `k` number of distinct objects from a set of `n` number of distinct objects.
-- Equivalently, it is the number of `k`-sized subsets of an `n`-sized set.
-- Also called: Binomial coefficients
-- Formulated using sets:
--   𝐶: Set → ℕ → Set
--   𝐶 S k = {(K∊℘(S)). #K = k}
--   𝑐𝐶(n) = #𝐶(𝕟(n))
𝑐𝐶 : ℕ → ℕ → ℕ
𝑐𝐶 _     𝟎     = 𝐒 𝟎
𝑐𝐶 𝟎     (𝐒 k) = 𝟎
𝑐𝐶 (𝐒 n) (𝐒 k) = 𝑐𝐶 n k + 𝑐𝐶 n (𝐒 k)

-- Counting partial permutations.
-- `𝑐𝑃 n k` is the number of arrangements for a list of `n` number of distinct objects into `k` number of objects.
-- Equivalently, it is the number of injective functions (function equality by the standard function extensionality) of type `𝕟(k) → 𝕟(n)`.
-- Also called: Falling factorial
-- Formulated using sets:
--   𝑃: Set → ℕ → Set
--   𝑃 S k = {(π: 𝕟(k) → S). Injective(π)}
--   𝑐𝑃(n) = #𝑃(𝕟(n))
𝑐𝑃 : ℕ → ℕ → ℕ
𝑐𝑃 _     𝟎     = 𝐒 𝟎
𝑐𝑃 𝟎     (𝐒 k) = 𝟎
𝑐𝑃 (𝐒 n) (𝐒 k) = 𝑐𝑃 n k ⋅ (𝐒 n)

-- Counting derangements.
-- `𝑐𝐷(n)` is the number of permutations of a list of `n` number of distinct objects such that in every permutation, no object is permuted with itself.
-- Formulated using sets:
--   𝐷: Set → Set
--   𝐷(S) = {(π∊𝑃(S)). ∀(s∊S). π(s) ≠ s}
--   𝑐𝐷(n) = #𝐷(𝕟(n))
𝑐𝐷 : ℕ → ℕ
𝑐𝐷(𝟎)      = 𝐒 𝟎
𝑐𝐷(𝐒 𝟎)    = 𝟎
𝑐𝐷(𝐒(𝐒 n)) = 𝐒(n) ⋅ (𝑐𝐷 (𝐒 n) + 𝑐𝐷 n)

-- Stirling numbers of the first kind.
stir₁ : ℕ → ℕ → ℕ
stir₁ 𝟎      𝟎      = 𝐒(𝟎)
stir₁ (𝐒(n)) 𝟎      = 𝟎
stir₁ 𝟎      (𝐒(k)) = 𝟎
stir₁ (𝐒(n)) (𝐒(k)) = (n ⋅ stir₁ n (𝐒(k))) + stir₁ n k

-- Stirling numbers of the second kind.
stir₂ : ℕ → ℕ → ℕ
stir₂ 𝟎      𝟎      = 𝐒(𝟎)
stir₂ (𝐒(n)) 𝟎      = 𝟎
stir₂ 𝟎      (𝐒(k)) = 𝟎
stir₂ (𝐒(n)) (𝐒(k)) = (𝐒(k) ⋅ stir₂ n (𝐒(k))) + stir₂ n k

-- Counting injective functions.
𝑐𝐼𝑛𝑗 : ℕ → ℕ → ℕ
𝑐𝐼𝑛𝑗 = 𝑐𝑃

-- Counting surjective functions.
𝑐𝑆𝑢𝑟𝑗 : ℕ → ℕ → ℕ
𝑐𝑆𝑢𝑟𝑗 a b = stir₂ a b ⋅ (b !)

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 LTC-PCF base
------------------------------------------------------------------------------

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

{-
LTC-PCF                               The logical framework (Agda)

* Logical constants                   * Curry-Howard isomorphism
* Equality                            * Identity type
* Term language and conversion rules  * Postulates
* Inductively defined predicates      * Inductive families
-}

module LTC-PCF.Base where

-- First-order logic with equality.
open import Common.FOL.FOL-Eq public

-- Common definitions.
open import Common.DefinitionsI public

infixl 7 _·_
infix  0 if_then_else_

------------------------------------------------------------------------------
-- The term language of LTC-PCF correspond to the PCF terms.

--   t ::= x
--      | t · t
--      | λ x.t
--      | fix x.t
--      | true | false | if
--      | zero | succ  | pred | iszero

-- NB. We define the PCF terms as constants. After that, we will
-- define some function symbols based on these constants for
-- convenience in writing.

postulate
  _·_                   : D → D → D    -- LTC-PCF application.
  lam                   : (D → D) → D  -- LTC-PCF λ-abstraction.
  fix                   : (D → D) → D  -- LTC-PCF fixed-point operator.
  true false if         : D            -- LTC-PCF partial Booleans.
  zero succ pred iszero : D            -- LTC-PCF partial natural numbers.

------------------------------------------------------------------------------
-- Definitions

-- We define some function symbols for convenience in writing.
abstract
  if_then_else_ : D → D → D → D
  if b then t else t' = if · b · t · t'

  succ₁ : D → D
  succ₁ n = succ · n

  pred₁ : D → D
  pred₁ n = pred · n

  iszero₁ : D → D
  iszero₁ n = iszero · n

------------------------------------------------------------------------------
-- Conversion rules

-- The conversion relation _conv_ satifies (Aczel 1977. The strength
-- of Martin-Löf's intuitionistic type theory with one universe,
-- p. 8).
--
-- x conv y <=> FOTC ⊢ x ≡ y,
--
-- therefore, we introduce the conversion rules as non-logical axioms.

-- N.B. We write the conversion rules on the defined function symbols
-- instead of on the PCF constants.

-- Conversion rule for the λ-abstraction and the application.
postulate beta : ∀ f a → lam f · a ≡ f a

-- Conversion rule for the fixed-pointed operator.
postulate fix-eq : ∀ f → fix f ≡ f (fix f)

-- Conversion rules for Booleans.
postulate
  -- if-true  : ∀ t {t'} → if · true  · t · t' ≡ t
  -- if-false : ∀ {t} t' → if · false · t · t' ≡ t'
  if-true  : ∀ t {t'} → (if true then t else t')  ≡ t
  if-false : ∀ {t} t' → (if false then t else t') ≡ t'

-- Conversion rules for pred.
postulate
  -- pred-0 : pred · zero ≡ zero
  -- pred-S : ∀ d → pred · (succ · d) ≡ d

 -- N.B. We don't need this equation in FOTC.
  pred-0 : pred₁ zero            ≡ zero
  pred-S : ∀ n → pred₁ (succ₁ n) ≡ n

-- Conversion rules for iszero.
postulate
  -- iszero-0 :       iszero · zero       ≡ true
  -- iszero-S : ∀ d → iszero · (succ · d) ≡ false
  iszero-0 : iszero₁ zero            ≡ true
  iszero-S : ∀ n → iszero₁ (succ₁ n) ≡ false

------------------------------------------------------------------------------
-- Discrimination rules

postulate
  t≢f : true ≢ false
  -- 0≢S : ∀ {d} → zero ≢ succ · d
  0≢S : ∀ {n} → zero ≢ succ₁ n

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Data.Product using ( proj₁ ; proj₂ )
open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ )
open import Relation.Binary.PropositionalEquality using ( refl )
open import Web.Semantic.DL.ABox.Interp using ( ⌊_⌋ ; ind ; _*_ )
open import Web.Semantic.DL.ABox.Interp.Morphism using ( _,_ )
open import Web.Semantic.DL.ABox.Model using
  ( _⊨a_ ; on-bnode ; bnodes ; _,_ ; ⊨a-resp-≲ )
open import Web.Semantic.DL.Category.Composition using ( _∙_ )
open import Web.Semantic.DL.Category.Properties.Composition.Lemmas using
  ( compose-left ; compose-right ; compose-resp-⊨a )
open import Web.Semantic.DL.Category.Properties.Tensor.Lemmas using
  ( tensor-up ; tensor-down ; tensor-resp-⊨a )
open import Web.Semantic.DL.Category.Object using ( Object ; IN ; fin )
open import Web.Semantic.DL.Category.Morphism using
  ( _⇒_ ; BN ; impl ; _⊑_ ; _≣_ ; _,_ )
open import Web.Semantic.DL.Category.Tensor using ( _⊗_ ; _⟨⊗⟩_ )
open import Web.Semantic.DL.Category.Unit using ( I )
open import Web.Semantic.DL.Category.Wiring using
  ( wires-≈ ; wires-≈⁻¹ ; symm )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.DL.TBox.Interp using ( Δ ; _⊨_≈_ ; ≈-refl ; ≈-sym )
open import Web.Semantic.DL.TBox.Interp.Morphism using ( ≲-refl )
open import Web.Semantic.Util using
  ( _∘_ ; False ; ⊎-swap
  ; _⊕_⊕_ ; inode ; bnode ; enode ; left ; right ; up ; down )

module Web.Semantic.DL.Category.Properties.Tensor.SymmNatural
  {Σ : Signature} {S T : TBox Σ} where

symm-natural : ∀ {A₁ A₂ B₁ B₂ : Object S T} (F₁ : A₁ ⇒ B₁) (F₂ : A₂ ⇒ B₂) →
  ((F₁ ⟨⊗⟩ F₂) ∙ symm B₁ B₂ ≣ symm A₁ A₂ ∙ (F₂ ⟨⊗⟩ F₁))
symm-natural {A₁} {A₂} {B₁} {B₂} F₁ F₂ = (LHS⊑RHS , RHS⊑LHS) where

  LHS⊑RHS : (F₁ ⟨⊗⟩ F₂) ∙ symm B₁ B₂ ⊑ symm A₁ A₂ ∙ (F₂ ⟨⊗⟩ F₁)
  LHS⊑RHS J J⊨STA J⊨LHS = (f , J⊨RHS) where

    f : False ⊕ (IN A₂ ⊎ IN A₁) ⊕ (BN F₂ ⊎ BN F₁) → Δ ⌊ J ⌋
    f (inode ())
    f (bnode (inj₁ x)) = ind J (inode (inj₂ x))
    f (bnode (inj₂ x)) = ind J (inode (inj₁ x))
    f (enode (inj₁ v)) = ind J (bnode (inode (inj₂ v)))
    f (enode (inj₂ v)) = ind J (bnode (inode (inj₁ v)))

    lemma₀ : ∀ x →
      ⌊ J ⌋ ⊨ ind J (inode (⊎-swap x)) ≈ f (bnode x)
    lemma₀ (inj₁ x) = ≈-refl ⌊ J ⌋
    lemma₀ (inj₂ y) = ≈-refl ⌊ J ⌋

    lemma₁ : ∀ x →
      ⌊ J ⌋ ⊨ ind J (left (up x)) ≈ on-bnode f (ind J) (right (down x))
    lemma₁ (inode x) = ≈-refl ⌊ J ⌋
    lemma₁ (bnode v) = ≈-refl ⌊ J ⌋
    lemma₁ (enode y) = wires-≈ ⊎-swap (proj₂ (fin (B₂ ⊗ B₁)) (inj₂ y))
      (compose-right (F₁ ⟨⊗⟩ F₂) (symm B₁ B₂) J J⊨LHS)

    lemma₂ : ∀ x →
      ⌊ J ⌋ ⊨ ind J (left (down x)) ≈ on-bnode f (ind J) (right (up x))
    lemma₂ (inode x) = ≈-refl ⌊ J ⌋
    lemma₂ (bnode v) = ≈-refl ⌊ J ⌋
    lemma₂ (enode y) = wires-≈ ⊎-swap (proj₂ (fin (B₂ ⊗ B₁)) (inj₁ y))
      (compose-right (F₁ ⟨⊗⟩ F₂) (symm B₁ B₂) J J⊨LHS)

    J⊨RHS : bnodes J f ⊨a impl (symm A₁ A₂ ∙ (F₂ ⟨⊗⟩ F₁))
    J⊨RHS = compose-resp-⊨a (symm A₁ A₂) (F₂ ⟨⊗⟩ F₁) (bnodes J f)
      (wires-≈⁻¹ ⊎-swap lemma₀ (proj₁ (fin (A₂ ⊗ A₁))))
      (tensor-resp-⊨a F₂ F₁ (right * bnodes J f)
        (⊨a-resp-≲ (≲-refl ⌊ J ⌋ , lemma₂) (impl F₂)
          (tensor-down F₁ F₂ (left * J)
            (compose-left (F₁ ⟨⊗⟩ F₂) (symm B₁ B₂) J J⊨LHS)))
        (⊨a-resp-≲ (≲-refl ⌊ J ⌋ , lemma₁) (impl F₁)
          (tensor-up F₁ F₂ (left * J)
            (compose-left (F₁ ⟨⊗⟩ F₂) (symm B₁ B₂) J J⊨LHS))))

  RHS⊑LHS : symm A₁ A₂ ∙ (F₂ ⟨⊗⟩ F₁) ⊑ (F₁ ⟨⊗⟩ F₂) ∙ symm B₁ B₂
  RHS⊑LHS J J⊨STA J⊨RHS = (f , J⊨LHS) where

    f : ((BN F₁ ⊎ BN F₂) ⊕ (IN B₁ ⊎ IN B₂) ⊕ False) → Δ ⌊ J ⌋
    f (inode (inj₁ v)) = ind J (bnode (enode (inj₂ v)))
    f (inode (inj₂ v)) = ind J (bnode (enode (inj₁ v)))
    f (bnode (inj₁ y)) = ind J (enode (inj₂ y))
    f (bnode (inj₂ y)) = ind J (enode (inj₁ y))
    f (enode ())

    lemma₀ : ∀ x → ⌊ J ⌋ ⊨ f (bnode (⊎-swap x)) ≈ ind J (enode x)
    lemma₀ (inj₁ y) = ≈-refl ⌊ J ⌋
    lemma₀ (inj₂ y) = ≈-refl ⌊ J ⌋

    lemma₁ : ∀ x →
      ⌊ J ⌋ ⊨ ind J (right (down x)) ≈ on-bnode f (ind J) (left (up x))
    lemma₁ (inode x) = ≈-sym ⌊ J ⌋
      (wires-≈ ⊎-swap (proj₂ (fin (A₂ ⊗ A₁)) (inj₂ x))
        (compose-left (symm A₁ A₂) (F₂ ⟨⊗⟩ F₁) J J⊨RHS))
    lemma₁ (bnode v) = ≈-refl ⌊ J ⌋
    lemma₁ (enode y) = ≈-refl ⌊ J ⌋

    lemma₂ : ∀ x →
      ⌊ J ⌋ ⊨ ind J (right (up x)) ≈ on-bnode f (ind J) (left (down x))
    lemma₂ (inode x) = ≈-sym ⌊ J ⌋
      (wires-≈ ⊎-swap (proj₂ (fin (A₂ ⊗ A₁)) (inj₁ x))
        (compose-left (symm A₁ A₂) (F₂ ⟨⊗⟩ F₁) J J⊨RHS))
    lemma₂ (bnode v) = ≈-refl ⌊ J ⌋
    lemma₂ (enode y) = ≈-refl ⌊ J ⌋

    J⊨LHS : bnodes J f ⊨a impl ((F₁ ⟨⊗⟩ F₂) ∙ symm B₁ B₂)
    J⊨LHS = compose-resp-⊨a (F₁ ⟨⊗⟩ F₂) (symm B₁ B₂) (bnodes J f)
      (tensor-resp-⊨a F₁ F₂ (left * bnodes J f)
        (⊨a-resp-≲ (≲-refl ⌊ J ⌋ , lemma₁) (impl F₁)
          (tensor-down F₂ F₁ (right * J)
            (compose-right (symm A₁ A₂) (F₂ ⟨⊗⟩ F₁) J J⊨RHS)))
        (⊨a-resp-≲ (≲-refl ⌊ J ⌋ , lemma₂) (impl F₂)
          (tensor-up F₂ F₁ (right * J)
            (compose-right (symm A₁ A₂) (F₂ ⟨⊗⟩ F₁) J J⊨RHS))))
      (wires-≈⁻¹ ⊎-swap lemma₀ (proj₁ (fin (B₂ ⊗ B₁))))

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
-- Andreas, 2017-04-26
-- Allow more flexible size assignment.

module _ where

open import Agda.Builtin.Size

module ZeroZero where

  data Nat : Size → Set where
    zero : ∀{i}         → Nat i   -- does not have to be ↑ i
    suc  : ∀{i} → Nat i → Nat (↑ i)

  mon : ∀{i}{j : Size< i} → Nat j → Nat i
  mon x = x

  minus : ∀{i} → Nat i → Nat ∞ → Nat i
  minus x       zero    = x
  minus zero    (suc y) = zero
  minus (suc x) (suc y) = minus x y

  div : ∀{i} → Nat i → Nat ∞ → Nat i
  div zero y = zero
  div (suc x) y = suc (div (minus x y) y)

module DSuc where

  -- Here, the upper least bound for the size is the number itself.

  data Nat : Size → Set where
    zero : ∀{i}         → Nat i
    suc  : ∀{i} → Nat i → Nat (↑ i)
    dsuc : ∀{i} → Nat i → Nat (↑ ↑ i)

  -- Testing subtyping.

  mon : ∀{i}{j : Size< i} → Nat j → Nat i
  mon x = x

  minus : ∀{i} → Nat i → Nat ∞ → Nat i
  minus x        zero     = x
  minus zero     y        = zero
  minus (suc x)  (suc y)  = minus x y
  minus (suc x)  (dsuc y) = minus x (suc y)
  minus (dsuc x) (suc y)  = minus (suc x) y
  minus (dsuc x) (dsuc y) = minus x y

  div : ∀{i} → Nat i → Nat ∞ → Nat i
  div zero     y = zero
  div (suc x)  y = suc (div (minus x y) y)
  div (dsuc x) y = suc (div (minus (suc x) y) y)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import HoTT
import homotopy.HopfConstruction
open import homotopy.CircleHSpace
open import homotopy.SuspensionJoin using () renaming (e to suspension-join)
import homotopy.JoinAssocCubical

module homotopy.Hopf where

module Hopf = homotopy.HopfConstruction S¹ S¹-connected S¹-hSpace

Hopf : S² → Type₀
Hopf = Hopf.H.f

Hopf-fiber : Hopf north == S¹
Hopf-fiber = idp

Hopf-total : Σ _ Hopf == S³
Hopf-total =
  Σ _ Hopf       =⟨ Hopf.theorem ⟩
  S¹ * S¹        =⟨ ua (suspension-join S⁰) |in-ctx (λ u → u * S¹) ⟩
  (S⁰ * S⁰) * S¹ =⟨ homotopy.JoinAssocCubical.*-assoc ⟩
  S⁰ * (S⁰ * S¹) =⟨ ! (ua (suspension-join S¹)) |in-ctx (λ u → S⁰ * u) ⟩
  S⁰ * S²        =⟨ ! (ua (suspension-join S²)) ⟩
  S³ ∎

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


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

{-# BUILTIN NATURAL Nat #-}

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

pred : Nat → Nat
pred zero = zero
pred (suc n) = n

{-# NON_TERMINATING #-}
loop : Nat → Nat
loop zero = zero
loop n = loop (pred n)

-- Non-terminating functions reduce when evaluated at top-level,
-- but not in a hole.
hole : Set
hole = {!!}


text:
module z01-fp-with-booleans where

open import bool

{-
data 𝔹 : Set where
  tt : 𝔹
  ff : 𝔹

˜_ : 𝔹 → 𝔹
˜ tt = ff
˜ ff = tt

if_then_else_ : ∀ {ℓ} {A : Set ℓ} → 𝔹 → A → A → A
if tt then t else f = t
if ff then t else f = f
-}

-- load / type-check file
-- C-c, C-l

-- check type of expression
-- C-c, C-d ; then prompt for expression

------------------------------------------------------------------------------
-- p 24 1.8 Exercises

z01-1-8-01a : 𝔹
z01-1-8-01a = tt && (ff xor ~ ff)

z01-1-8-01b : 𝔹
z01-1-8-01b = ~ tt && (ff imp ff)

z01-1-8-01c : 𝔹
z01-1-8-01c = if tt xor tt then ff else ff

-- 1-8-4
data day : Set where
 mon : day
 tue : day
 wed : day
 thu : day
 fri : day
 sat : day
 sun : day

-- 1-8-5
nextday : day → day
nextday mon = tue
nextday tue = wed
nextday wed = thu
nextday thu = fri
nextday fri = sat
nextday sat = sun
nextday sun = mon

-- 1-8-6
data suit : Set where
  hearts   : suit
  spades   : suit
  diamonds : suit
  clubs    : suit

-- 1-8-7
is-red : suit → 𝔹
is-red hearts   = tt
is-red spades   = ff
is-red diamonds = tt
is-red clubs    = ff

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

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

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


text:
------------------------------------------------------------------------------
-- Propositional equality
------------------------------------------------------------------------------

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

-- This module is re-exported by (some) "base" modules.

module Common.FOL.Relation.Binary.PropositionalEquality where

open import Common.FOL.FOL using ( D )

infix 4 _≡_

------------------------------------------------------------------------------
-- The identity type on the universe of discourse.
data _≡_ (x : D) : D → Set where
  refl : x ≡ x

-- Elimination rule.
subst : (A : D → Set) → ∀ {x y} → x ≡ y → A x → A y
subst A refl Ax = Ax

-- Identity properties

sym : ∀ {x y} → x ≡ y → y ≡ x
sym refl = refl

trans : ∀ {x y z} → x ≡ y → y ≡ z → x ≡ z
trans refl h = h

trans₂ : ∀ {w x y z} → w ≡ x → x ≡ y → y ≡ z → w ≡ z
trans₂ refl refl h = h

subst₂ : (A : D → D → Set) → ∀ {x x' y y'} →
         x ≡ y → x' ≡ y' →
         A x x' →
         A y y'
subst₂ A refl refl Axs = Axs

subst₃ : (A : D → D → D → Set) → ∀ {x₁ x₂ x₃ y₁ y₂ y₃} →
         x₁ ≡ y₁ → x₂ ≡ y₂ → x₃ ≡ y₃ →
         A x₁ x₂ x₃ →
         A y₁ y₂ y₃
subst₃ A refl refl refl Axs = Axs

subst₄ : (A : D → D → D → D → Set) → ∀ {x₁ x₂ x₃ x₄ y₁ y₂ y₃ y₄} →
         x₁ ≡ y₁ → x₂ ≡ y₂ → x₃ ≡ y₃ → x₄ ≡ y₄ →
         A x₁ x₂ x₃ x₄ →
         A y₁ y₂ y₃ y₄
subst₄ A refl refl refl refl Axs = Axs


text:
-- Needs the --injective-type-constructors option enabled to type check.
module InjectiveTypeConstructors where

data D (A : Set) : Set where

data _==_ (A : Set) : Set → Set where
  refl : A == A

injD : ∀ {A B} → D A == D B → A == B
injD refl = refl


text:
module Cats.Category.Product.Binary.Facts where

open import Cats.Category
open import Cats.Category.Product.Binary using (_×_)
open import Cats.Functor
open import Cats.Util.Logic.Constructive using (_∧_ ; _,_ ; ∧-eliml ; ∧-elimr)

module _ {lo la l≈ lo′ la′ l≈′}
  {C : Category lo la l≈}
  {D : Category lo′ la′ l≈′}
  where

  private
    module C = Category C
    module D = Category D
    module × = Category (C × D)

  open Category._≅_

  iso-intro : ∀ {A A′ B B′} → A C.≅ A′ → B D.≅ B′ → (A , B) ×.≅ (A′ , B′)
  iso-intro f g = record
      { forth = forth f , forth g
      ; back = back f , back g
      ; back-forth = back-forth f , back-forth g
      ; forth-back = forth-back f , forth-back g
      }

  iso-elim : ∀ {A A′ B B′} → (A , B) ×.≅ (A′ , B′) → A C.≅ A′ ∧ B D.≅ B′
  iso-elim f
      = record
      { forth = ∧-eliml (forth f)
      ; back = ∧-eliml (back f)
      ; back-forth = ∧-eliml (back-forth f)
      ; forth-back = ∧-eliml (forth-back f)
      }
      , record
      { forth = ∧-elimr (forth f)
      ; back = ∧-elimr (back f)
      ; back-forth = ∧-elimr (back-forth f)
      ; forth-back = ∧-elimr (forth-back f)
      }


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

open import Data.Unit
open import Data.Empty
open import Data.Nat
open import Data.Sum as Sum
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality
open import Relation.Unary
open import Relation.Binary
open import Relation.Binary using (module IsEquivalence; Setoid; module Setoid)
open ≡-Reasoning
import Relation.Binary.HeterogeneousEquality as HE
open import Relation.Binary.HeterogeneousEquality using (_≅_; refl)

-- | Polynomials
data Poly : Set₁ where
  _▹_ : (A : Set) (B : A → Set) → Poly

-- | Interpretation of polynomials as functor, object part.
⟦_⟧ : Poly → Set → Set
⟦ A ▹ B ⟧ X = Σ[ a ∈ A ] (B a → X)

-- | Interpretation of polynomials as functor, morphism part.
⟦_⟧₁ : (P : Poly) → ∀{X Y} → (X → Y) → (⟦ P ⟧ X → ⟦ P ⟧ Y)
⟦ A ▹ B ⟧₁ f (a , α) = (a , (λ x → f (α x)))

-- | Finite trees over the signature determined by P with one free variable.
data _* (P : Poly) : Set where
  sup : ⟦ P ⟧ (P *) ⊎ ⊤ → P *

-- | Inverse of sup.
sup⁻¹ : ∀{P} → P * → ⟦ P ⟧ (P *) ⊎ ⊤
sup⁻¹ (sup x) = x

_extends_ : ∀{P} → P * → P * → Set
_extends_ {A ▹ B} (sup (inj₁ (a' , β))) (sup (inj₁ (a , α)))
  = Σ[ e ∈ a' ≡ a ] (∀ (b : B a') → (β b) extends α (subst B e b))
sup (inj₂ _) extends sup (inj₁ _) = ⊥
sup (inj₁ x) extends sup (inj₂ _) = ⊤
sup (inj₂ _) extends sup (inj₂ _) = ⊥

PreApprox : Poly → Set
PreApprox P = ℕ → P *

converges : ∀{P} → PreApprox P → Set
converges u = ∀ n → u (1 + n) extends u n

non-empty : ∀{P} → P * → Set
non-empty (sup (inj₁ x)) = ⊤
non-empty (sup (inj₂ _)) = ⊥

root : ∀{A B} → (t : (A ▹ B) *) → non-empty t → A
root (sup (inj₁ x)) p = proj₁ x
root (sup (inj₂ y)) ()

branch : ∀{A B} → (t : (A ▹ B) *) → (p : non-empty t) → B (root t p) → (A ▹ B) *
branch (sup (inj₁ x)) p  b = proj₂ x b
branch (sup (inj₂ y)) () b

_∞ : Poly → Set
P ∞ = Σ[ u ∈ PreApprox P ] (non-empty (u 0) × converges u)

-- | If u₀ is non-empty and u converges, then uₙ is non-empty for every n.
ne₀→all-ne : ∀{P} →
  (u : PreApprox P) → non-empty (u 0) → converges u →
  ∀ n → non-empty (u n)
ne₀→all-ne u ne₀ conv zero = ne₀
ne₀→all-ne {A ▹ B} u ne₀ conv (suc n)
  with u (suc n)   | u n          | conv n
... | sup (inj₁ x) | y            | z       = tt
... | sup (inj₂ x) | sup (inj₁ y) | ()
... | sup (inj₂ x) | sup (inj₂ y) | ()

-- | If t₂ extends t₁ and they are both non-empty, then they have the same
-- root labels.
ext→root≡ : ∀{A B} →
            (t₁ t₂ : (A ▹ B) *)
            (ne₁ : non-empty t₁)
            (ne₂ : non-empty t₂)
            (e : t₂ extends t₁) →
            root t₁ ne₁ ≡ root t₂ ne₂
ext→root≡ (sup (inj₁ (a , α))) (sup (inj₁ (b , β))) ne₁ ne₂ e = sym (proj₁ e)
ext→root≡ (sup (inj₁ x))       (sup (inj₂ tt))      ne₁ ()  e
ext→root≡ (sup (inj₂ tt))      (sup (inj₁ y))       ()  ne₂ e
ext→root≡ (sup (inj₂ tt))      (sup (inj₂ tt))      ne₁ ne₂ ()

-- | The roots of the first two trees in a converging sequence have the same
-- label. This is used as base case in conv→suc-roots≡.
conv→roots-0-1≡ : ∀{A B} →
  (u : PreApprox (A ▹ B))
  (ne : non-empty (u 0))
  (c : converges u) →
  root (u 0) ne ≡ root (u 1) (ne₀→all-ne u ne c 1)
conv→roots-0-1≡ {A} {B} u ne c
  = ext→root≡ (u 0) (u 1) ne (ne₀→all-ne u ne c 1) (c 0)

-- | The roots of two successive trees in a converging sequence have the same
-- label. We use this in the induction step in conv→roots≡.
conv→suc-roots≡ : ∀{A B} →
  (u : PreApprox (A ▹ B))
  (ne : non-empty (u 0))
  (c : converges u) →
  ∀ n → root (u n) (ne₀→all-ne u ne c n)
        ≡ root (u (1 + n)) (ne₀→all-ne u ne c (1 + n))
conv→suc-roots≡ u ne c zero = conv→roots-0-1≡ u ne c
conv→suc-roots≡ u ne c (suc n)
  = ext→root≡ (u (1 + n))
              (u (2 + n))
              (ne₀→all-ne u ne c (1 + n))
              (ne₀→all-ne u ne c (2 + n))
              (c (suc n))

-- | The root of any tree in a converging sequence has the same label as
-- the root of the first tree.
conv→roots≡ : ∀{A B} →
  (u : PreApprox (A ▹ B))
  (ne : non-empty (u 0))
  (c : converges u) →
  ∀ n → root (u 0) ne ≡ root (u n) (ne₀→all-ne u ne c n)
conv→roots≡ u ne c zero = refl
conv→roots≡ u ne c (suc n)
  = trans (conv→roots≡ u ne c n) (conv→suc-roots≡ u ne c n)

-- | All trees in a converging sequence have the same root label.
conv→all-roots≡ : ∀{A B} →
  (u : PreApprox (A ▹ B))
  (ne : non-empty (u 0))
  (c : converges u) →
  ∀ n m → root (u n) (ne₀→all-ne u ne c n) ≡ root (u m) (ne₀→all-ne u ne c m)
conv→all-roots≡ u ne c n m =
  begin
    root (u n) (ne₀→all-ne u ne c n)
  ≡⟨ sym (conv→roots≡ u ne c n) ⟩
    root (u 0) ne
  ≡⟨ conv→roots≡ u ne c m ⟩
    root (u m) (ne₀→all-ne u ne c m)
  ∎

-- | If t₁ is non-empty and t₂ extends t₁, then all branches of t₂ are
-- non-empty. This shows that _extends_ defines a strict order.
conv+ne₀→ne-branch : ∀{A B} →
  (t₁ t₂ : (A ▹ B)*)
  (ne₁ : non-empty t₁)
  (ne₂ : non-empty t₂)
  (e : t₂ extends t₁) →
  ∀ b → non-empty (branch t₂ ne₂ b)
conv+ne₀→ne-branch (sup (inj₁ (a , α))) (sup (inj₁ (.a , β))) ne₁ ne₂ (refl , q) b
  with α b          | β b           | q b
... | sup (inj₁ x)  | sup (inj₁ y)  | z  = tt
... | sup (inj₁ x)  | sup (inj₂ tt) | ()
... | sup (inj₂ tt) | sup (inj₁ y)  | z  = tt
... | sup (inj₂ tt) | sup (inj₂ tt) | ()
conv+ne₀→ne-branch (sup (inj₁ x)) (sup (inj₂ tt)) ne₁ () e b
conv+ne₀→ne-branch (sup (inj₂ tt)) t₂             () ne₂ e b

-- | If t₂ extends t₂, then all branches of t₂ extend the corresponding one
-- of t₁.
conv→branch-conv : ∀{A B} →
  (t₁ t₂ : (A ▹ B)*)
  (ne₁ : non-empty t₁)
  (ne₂ : non-empty t₂)
  (e : t₂ extends t₁) →
  ∀ b b' → b ≅ b' →
  (branch t₂ ne₂ b) extends
  (branch t₁ ne₁ b')
conv→branch-conv (sup (inj₁ (a'' , α)))
                 (sup (inj₁ (.a'' , β))) ne₁ ne₂ (refl , t) b .b refl = t b
conv→branch-conv (sup (inj₁ x)) (sup (inj₂ tt)) ne₁ () e b b' p
conv→branch-conv (sup (inj₂ tt)) (sup y) () ne₂ e b b' p

-- | Technical lemma:
-- The equality proofs for substitution by root equality are the same.
root-conv≡ : ∀ {A B} →
  (u : PreApprox (A ▹ B))
  (ne : non-empty (u 0))
  (c : converges u) →
  ∀ b n → (subst B (conv→roots≡ u ne c (1 + n)) b)
          ≅ (subst B (conv→roots≡ u ne c n) b)
root-conv≡ {A} {B} u ne c b n =
  HE.trans (HE.≡-subst-removable B (conv→roots≡ u ne c (1 + n)) b)
           (HE.sym (HE.≡-subst-removable B (conv→roots≡ u ne c n) b))

-- | Coalgebra structure on P∞.
out : ∀{P} → P ∞ → ⟦ P ⟧ (P ∞)
out {A ▹ B} (u , ne , conv) = (a , α)
  where
    a : A
    a = root (u 0) ne

    u' : B a → PreApprox (A ▹ B)
    u' b n = branch (u (1 + n))
                    (ne₀→all-ne u ne conv (1 + n))
                    (subst B (conv→roots≡ u ne conv (1 + n)) b)

    ne' : (b : B a) → non-empty (u' b 0)
    ne' b =
      conv+ne₀→ne-branch (u 0) (u 1) ne
                            (ne₀→all-ne u ne conv 1)
                            (conv 0)
                            (subst B (conv→roots≡ u ne conv 1) b)

    conv' : (b : B a) → converges (u' b)
    conv' b n = conv→branch-conv (u (1 + n)) (u (2 + n))
                                  (ne₀→all-ne u ne conv (1 + n))
                                  (ne₀→all-ne u ne conv (2 + n))
                                  (conv (1 + n))
                                  (subst B (conv→roots≡ u ne conv (2 + n)) b)
                                  (subst B (conv→roots≡ u ne conv (1 + n)) b)
                                  (root-conv≡ u ne conv b (suc n))

    α : B a → (A ▹ B) ∞
    α b = (u' b , ne' b , conv' b)

-- | Get root label.
root∞ : ∀{A B} → (A ▹ B) ∞ → A
root∞ t = proj₁ (out t)

-- | Get branches below root.
branch∞ : ∀{A B} → (t : (A ▹ B) ∞) → B (root∞ t) → (A ▹ B) ∞
branch∞ t = proj₂ (out t)

-- | Corecursion principle for P∞.
corec : ∀{P} {C : Set} → (C → ⟦ P ⟧ C) → (C → P ∞)
corec {A ▹ B} {C} f c = (u , ne , conv)
  where
    u-aux : C → PreApprox (A ▹ B)
    u-aux c zero =
      let (a , α) = f c
      in sup (inj₁ (a , (λ x → sup (inj₂ tt))))
    u-aux c (suc n) =
      let (a , α) = f c
      in sup (inj₁ (a , (λ b → u-aux (α b) n)))

    u : PreApprox (A ▹ B)
    u = u-aux c

    ne : non-empty (u 0)
    ne = tt

    conv-aux : (c : C) → converges (u-aux c)
    conv-aux c zero    = (refl , (λ b → tt))
    conv-aux c (suc n) = (refl , (λ b → conv-aux (proj₂ (f c) b) n))

    conv : converges u
    conv = conv-aux c

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module Tactic.Nat.Auto where

open import Prelude
open import Builtin.Reflection
open import Tactic.Reflection.Quote
open import Tactic.Reflection

open import Tactic.Nat.NF
open import Tactic.Nat.Exp
open import Tactic.Nat.Reflect
open import Tactic.Nat.Auto.Lemmas

open Tactic.Nat.Reflect public using (cantProve; invalidGoal)

module _ {Atom : Set} {{_ : Eq Atom}} {{_ : Ord Atom}} where
  liftNFEq : ∀ (e₁ : Exp Atom) e₂ ρ → ⟦ norm e₁ ⟧n ρ ≡ ⟦ norm e₂ ⟧n ρ → ⟦ e₁ ⟧e ρ ≡ ⟦ e₂ ⟧e ρ
  liftNFEq e₁ e₂ ρ H = eraseEquality $
    ⟦ e₁      ⟧e ρ ≡⟨ sound e₁ ρ ⟩
    ⟦ norm e₁ ⟧n ρ ≡⟨ H ⟩
    ⟦ norm e₂ ⟧n ρ ≡⟨ sound e₂ ρ ⟩ʳ
    ⟦ e₂      ⟧e ρ ∎

  unliftNFEq : ∀ (e₁ : Exp Atom) e₂ ρ → ⟦ e₁ ⟧e ρ ≡ ⟦ e₂ ⟧e ρ → ⟦ norm e₁ ⟧n ρ ≡ ⟦ norm e₂ ⟧n ρ
  unliftNFEq e₁ e₂ ρ H =
    ⟦ norm e₁ ⟧n ρ ≡⟨ sound e₁ ρ ⟩ʳ
    ⟦ e₁      ⟧e ρ ≡⟨ H ⟩
    ⟦ e₂      ⟧e ρ ≡⟨ sound e₂ ρ ⟩
    ⟦ norm e₂ ⟧n ρ ∎

  auto-proof : ∀ e₁ e₂ → norm e₁ ≡ norm e₂ → ∀ ρ → ⟦ e₁ ⟧e ρ ≡ ⟦ e₂ ⟧e ρ
  auto-proof e₁ e₂ nfeq ρ = liftNFEq e₁ e₂ ρ (cong (λ n → ⟦ n ⟧n ρ) nfeq)

auto-tactic : Type → Tactic
auto-tactic t hole = do
  just ((e₁ , e₂) , Γ) ← termToEq t
    where nothing → unify hole $ failedProof (quote invalidGoal) t
  prf ← newMeta!
  unify hole (def₄ (quote auto-proof) (` e₁) (` e₂) prf (quotedEnv Γ))
  unify prf (con₀ (quote refl)) <|> do
    def (quote _≡_) (_ ∷ _ ∷ vArg lnf ∷ vArg rnf ∷ []) ← normalise =<< inferType prf
      where sgoal → typeError $ strErr "Huh? This is a weird equality goal:" ∷ termErr sgoal ∷ []
    typeError $ strErr "Normal forms are not equal:" ∷ termErr lnf ∷ strErr "≠" ∷ termErr rnf ∷ []

macro
  auto : Tactic
  auto = on-goal auto-tactic

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
import      Lvl
open import Structure.Setoid
open import Type

module Automaton.TuringMachine where

open import Data.Boolean
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Programming
open import Data.Either as Either using (_‖_)
open import Data.Either.Setoid
open import Data.Option as Option
open import Data.Option.Functions as Option
open import Data.Option.Setoid
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Data.Tuple.Equivalence
open import Data.List renaming (∅ to ε ; _⊰_ to _·_)
open import Data.List.Setoid
open import Functional
open import Logic
open import Relator.Equals.Proofs.Equivalence
open import Structure.Operator
open import Structure.Relator
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type.Size.Finite

private variable ℓₚ ℓₛ ℓₐ ℓₑₛ ℓₑₐ : Lvl.Level
private variable Alphabet : Type{ℓₐ}

data Direction : Type{Lvl.𝟎} where
  Backward : Direction
  Stay     : Direction
  Forward  : Direction
private instance _ = [≡]-equiv {T = Direction}

record Tape (Alphabet : Type{ℓₐ}) : Type{ℓₐ} where
  coinductive
  field
    back    : Tape(Alphabet)
    current : Alphabet
    front   : Tape(Alphabet)

  update : (Alphabet → Alphabet) → Tape(Alphabet)
  back   (update _) = back
  current(update f) = f(current)
  front  (update _) = front

stepBackward : Tape(Alphabet) → Tape(Alphabet)
Tape.back   (stepBackward t) = Tape.back(Tape.back t)
Tape.current(stepBackward t) = Tape.current(Tape.back t)
Tape.front  (stepBackward t) = t

stepForward : Tape(Alphabet) → Tape(Alphabet)
Tape.back   (stepForward t) = t
Tape.current(stepForward t) = Tape.current(Tape.front t)
Tape.front  (stepForward t) = Tape.front(Tape.front t)

stepInDirection : Direction → Tape(Alphabet) → Tape(Alphabet)
stepInDirection Backward = stepBackward
stepInDirection Stay     = id
stepInDirection Forward  = stepForward

module _ ⦃ equiv-alphabet : Equiv{ℓₑₐ}(Alphabet) ⦄ where
  step-inverseₗᵣ : ∀{t : Tape(Alphabet)} → (Tape.current(stepBackward(stepForward(t))) ≡ Tape.current(t))
  step-inverseₗᵣ = reflexivity(_≡_ ⦃ equiv-alphabet ⦄)

  step-inverseᵣₗ : ∀{t : Tape(Alphabet)} → (Tape.current(stepBackward(stepForward(t))) ≡ Tape.current(t))
  step-inverseᵣₗ = reflexivity(_≡_ ⦃ equiv-alphabet ⦄)

module _
  (State : Type{ℓₛ})    ⦃ equiv-state : Equiv{ℓₑₛ}(State) ⦄
  (Alphabet : Type{ℓₐ}) ⦃ equiv-alphabet : Equiv{ℓₑₐ}(Alphabet) ⦄
  where

  private instance _ = [≡]-equiv {T = Bool}

  -- Turing machine
  -- `State`      (Q)  is the set of states.
  -- `Alphabet`   (Σ)  is the set of symbols/the alphabet.
  -- `transition` (δ)  is the transition function.
  -- `start`      (q₀) is the start state.
  -- `Final`      (F)  is the subset of State which are the final/accepting states.
  record TuringMachine : Type{ℓₛ Lvl.⊔ ℓₑₐ Lvl.⊔ ℓₑₛ Lvl.⊔ ℓₐ Lvl.⊔ Lvl.𝐒(ℓₚ)} where
    constructor turingMachine
    field
      ⦃ State-finite ⦄              : Finite(State)
      ⦃ Alphabet-finite ⦄           : Finite(Alphabet)
      transition                    : State → Option(Alphabet) → Option(State ⨯ Alphabet ⨯ Direction)
      ⦃ transition-binaryOperator ⦄ : BinaryOperator(transition)
      start                         : State
      Final                         : State → Type{ℓₚ}
      ⦃ Final-unaryRelator ⦄        : UnaryRelator(Final)

    -- isFinal : State → Bool

  -- TODO: Not sure what the best (most easy to use) formalization of a TM would be or if this is correct
  Configuration = State ⨯ Tape(Option(Alphabet))
  module Configuration where
    step : TuringMachine{ℓₚ} → (Configuration → Option(Configuration))
    step tm (s , t) = Option.map (\(ns , nx , dir) → (ns , stepInDirection dir (Tape.update t (Some ∘ const nx)))) (TuringMachine.transition tm s (Tape.current t))


text:
module Data.QuadTree.LensProofs.Valid-LensBCD where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Lens.Lens
open import Data.Logic
open import Data.QuadTree.InternalAgda
open import Agda.Primitive
open import Data.Lens.Proofs.LensLaws
open import Data.Lens.Proofs.LensPostulates
open import Data.Lens.Proofs.LensComposition
open import Data.QuadTree.Implementation.QuadrantLenses
open import Data.QuadTree.Implementation.Definition
open import Data.QuadTree.Implementation.ValidTypes
open import Data.QuadTree.Implementation.SafeFunctions
open import Data.QuadTree.Implementation.PublicFunctions
open import Data.QuadTree.Implementation.DataLenses

-- The lens laws have been proven for LensA, and the proof is quite long.
-- The implementation of lens b/c/d is basically identical, so I won't bother to proof them for now

--- Lens laws for lensB

postulate
    ValidLens-LensB-ViewSet :
        {t : Set} {{eqT : Eq t}} {dep : Nat}
        -> ViewSet (lensB {t} {dep})
    ValidLens-LensB-SetView :
        {t : Set} {{eqT : Eq t}} {dep : Nat}
        -> SetView (lensB {t} {dep})
    ValidLens-LensB-SetSet :
        {t : Set} {{eqT : Eq t}} {dep : Nat}
        -> SetSet (lensB {t} {dep})

ValidLens-LensB : {t : Set} {{eqT : Eq t}} {dep : Nat}
    -> ValidLens (VQuadrant t {S dep}) (VQuadrant t {dep})
ValidLens-LensB {t} {dep} = CValidLens lensB (ValidLens-LensB-ViewSet) (ValidLens-LensB-SetView) (ValidLens-LensB-SetSet)

--- Lens laws for lensC

postulate
    ValidLens-LensC-ViewSet :
        {t : Set} {{eqT : Eq t}} {dep : Nat}
        -> ViewSet (lensC {t} {dep})
    ValidLens-LensC-SetView :
        {t : Set} {{eqT : Eq t}} {dep : Nat}
        -> SetView (lensC {t} {dep})
    ValidLens-LensC-SetSet :
        {t : Set} {{eqT : Eq t}} {dep : Nat}
        -> SetSet (lensC {t} {dep})

ValidLens-LensC : {t : Set} {{eqT : Eq t}} {dep : Nat}
    -> ValidLens (VQuadrant t {S dep}) (VQuadrant t {dep})
ValidLens-LensC {t} {dep} = CValidLens lensC (ValidLens-LensC-ViewSet) (ValidLens-LensC-SetView) (ValidLens-LensC-SetSet)

--- Lens laws for lensD

postulate
    ValidLens-LensD-ViewSet :
        {t : Set} {{eqT : Eq t}} {dep : Nat}
        -> ViewSet (lensD {t} {dep})
    ValidLens-LensD-SetView :
        {t : Set} {{eqT : Eq t}} {dep : Nat}
        -> SetView (lensD {t} {dep})
    ValidLens-LensD-SetSet :
        {t : Set} {{eqT : Eq t}} {dep : Nat}
        -> SetSet (lensD {t} {dep})

ValidLens-LensD : {t : Set} {{eqT : Eq t}} {dep : Nat}
    -> ValidLens (VQuadrant t {S dep}) (VQuadrant t {dep})
ValidLens-LensD {t} {dep} = CValidLens lensD (ValidLens-LensD-ViewSet) (ValidLens-LensD-SetView) (ValidLens-LensD-SetSet)

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
{-#  OPTIONS --type-in-type #-}
module Bias where

open import AgdaPrelude

myFun : (a : Set) -> a -> a -> a -> a
myFun a x y z = x

--myApp1 = myFun _ Zero Zero (Nil Nat)

myApp2 = myFun _ (Nil Nat) Zero Zero

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint


text:
module Test2 where
   open import MiniHoTT

   A : Set
   A = ℕ

--  a, b : A

  {-
   [ a, b ] : List A
   [ a, b ] := inr ( a , ?)
    -- inr ((a, inr ( b, inl(unit))
    -}

   T : {A : Set} → (X : Set) → Set
   T {A} X = 𝟙 lzero + A × X -- This is an example of a polynomial functor.

   data
     List (A : Set)
      : Set
     where
     [] : List A
     cons : A → List A → List A

   data Vec (A : Set) : ℕ → Set
    where
    nil : ∀ n → Vec A n
    cons : ∀ n → A → Vec A n → Vec A (succ n)

   data Fin : ℕ →  Set
    where
    cero : ∀ {n} → Fin n
    succ : ∀ {n} → Fin n → Fin (succ n)

   at : ∀ {n : ℕ} {A : Set}
    → Vec A (succ n)
    → Fin (succ n)
    → A
   at v n = {!   !}

   go' : ∀ {n} {A : Set}
    → (Fin 0n → A) → Fin n → Vec A n
   go' pick cero     = nil _
   go' pick (succ n) = cons {!   !} (pick {! n  !})
    (go' {! pick    !} {!   !})

   record
     Algebra
      (A : Set)
      (T : Set → Set)
      : Set (lsuc lzero)
     where
     constructor algebra
     field
      X : Set
      μ : T X → X

   -- Objects: (X, μ)
   -- morphisms f : (X, μ) --> (Y, ν)
   --   this is given by α : X → Y, that makes the diagram commutes.
   -- Initial object: Object  (X, μ) + initiallity condition:
   --   Any other (Y, ν), there exists unique α : X → Y such that...

   list-is-an-algebra : (A : Set) → Algebra A (λ X → 𝟙 lzero + A × X)
   list-is-an-algebra A =
    algebra (List A) λ { (inl x) → []
                       ; (inr (a , xs)) → cons a xs
                       }

   -- where (T X -> X) is the type of list with elements of type A.
   -- elements? is TA a set?
   -- Yes, assuming A is a set. Let's find that.

   list-of-nats-is-set
     : A is-set
     → isSet (T A)
   list-of-nats-is-set A-is-set
    = +-set
        (prop-is-set 𝟙-is-prop)
        (∑-set
          A-is-set
          λ _ → A-is-set)

  -- T(X) = 1+X + (X ×X) a

max_stars_repo_name: jonaprieto/mini-hott

max_issues_repo_name: jonaprieto/mini-hott

max_forks_repo_name: jonaprieto/mini-hott


text:
open import Level
open import Ordinals
open import logic
open import Relation.Nullary
module LEMC {n : Level } (O : Ordinals {n} ) (p∨¬p : ( p : Set n) → p ∨ ( ¬ p )) where

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

open import nat
import OD

open inOrdinal O
open OD O
open OD.OD
open OD._==_
open ODAxiom odAxiom
import OrdUtil
import ODUtil
open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
open OrdUtil O
open ODUtil O

open import zfc

open HOD

open _⊆_

decp : ( p : Set n ) → Dec p   -- assuming axiom of choice
decp  p with p∨¬p p
decp  p | case1 x = yes x
decp  p | case2 x = no x

∋-p : (A x : HOD ) → Dec ( A ∋ x )
∋-p A x with p∨¬p ( A ∋ x)  -- LEM
∋-p A x | case1 t  = yes t
∋-p A x | case2 t  = no (λ x → t x)

double-neg-eilm : {A : Set n} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
double-neg-eilm  {A} notnot with decp  A                         -- assuming axiom of choice
... | yes p = p
... | no ¬p = ⊥-elim ( notnot ¬p )

power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (λ not → t1 t∋x (λ x → not x) ) } where
   t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
   t1 = power→ A t PA∋t

--- With assuption of HOD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
---
record choiced  ( X : Ordinal ) : Set n where
  field
     a-choice : Ordinal
     is-in : odef (* X) a-choice

open choiced

-- ∋→d : ( a : HOD  ) { x : HOD } → * (& a) ∋ x → X ∋ * (a-choice (choice-func X not))
-- ∋→d a lt = subst₂ (λ j k → odef j k) *iso (sym &iso) lt

oo∋ : { a : HOD} {  x : Ordinal } → odef (* (& a)) x → a ∋ * x
oo∋ lt = subst₂ (λ j k → odef j k) *iso (sym &iso) lt

∋oo : { a : HOD} {  x : Ordinal } → a ∋ * x → odef (* (& a)) x
∋oo lt = subst₂ (λ j k → odef j k ) (sym *iso) &iso lt

OD→ZFC : ZFC
OD→ZFC   = record {
    ZFSet = HOD
    ; _∋_ = _∋_
    ; _≈_ = _=h=_
    ; ∅  = od∅
    ; Select = Select
    ; isZFC = isZFC
 } where
    -- infixr  200 _∈_
    -- infixr  230 _∩_ _∪_
    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select
    isZFC = record {
       choice-func = λ A {X} not A∋X → * (a-choice (choice-func X not) );
       choice = λ A {X} A∋X not → oo∋ (is-in (choice-func X not))
     } where
         --
         -- the axiom choice from LEM and OD ordering
         --
         choice-func :  (X : HOD ) → ¬ ( X =h= od∅ ) → choiced (& X)
         choice-func  X not = have_to_find where
                 ψ : ( ox : Ordinal ) → Set n
                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ odef X x )) ∨ choiced (& X)
                 lemma-ord : ( ox : Ordinal  ) → ψ ox
                 lemma-ord  ox = TransFinite0 {ψ} induction ox where
                    ∀-imply-or :  {A : Ordinal  → Set n } {B : Set n }
                        → ((x : Ordinal ) → A x ∨ B) →  ((x : Ordinal ) → A x) ∨ B
                    ∀-imply-or  {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM
                    ∀-imply-or  {A} {B} ∀AB | case1 t = case1 t
                    ∀-imply-or  {A} {B} ∀AB | case2 x  = case2 (lemma (λ not → x not )) where
                         lemma : ¬ ((x : Ordinal ) → A x) →  B
                         lemma not with p∨¬p B
                         lemma not | case1 b = b
                         lemma not | case2 ¬b = ⊥-elim  (not (λ x → dont-orb (∀AB x) ¬b ))
                    induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
                    induction x prev with ∋-p X ( * x)
                    ... | yes p = case2 ( record { a-choice = x ; is-in = ∋oo  p } )
                    ... | no ¬p = lemma where
                         lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (& X)
                         lemma1 y with ∋-p X (* y)
                         lemma1 y | yes y<X = case2 ( record { a-choice = y ; is-in = ∋oo y<X } )
                         lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (d→∋ X y<X) )
                         lemma :  ((y : Ordinal) → y o< x → odef X y → ⊥) ∨ choiced (& X)
                         lemma = ∀-imply-or lemma1
                 odef→o< :  {X : HOD } → {x : Ordinal } → odef X x → x o< & X
                 odef→o<  {X} {x} lt = o<-subst  {_} {_} {x} {& X} ( c<→o< ( subst₂ (λ j k → odef j k )  (sym *iso) (sym &iso)  lt )) &iso &iso
                 have_to_find : choiced (& X)
                 have_to_find = dont-or  (lemma-ord (& X )) ¬¬X∋x where
                     ¬¬X∋x : ¬ ((x : Ordinal) → x o< (& X) → odef X x → ⊥)
                     ¬¬X∋x nn = not record {
                            eq→ = λ {x} lt → ⊥-elim  (nn x (odef→o< lt)  lt)
                          ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
                        }

         --
         --  axiom regurality from ε-induction (using axiom of choice above)
         --
         --  from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only
         --
         -- FIXME : don't use HOD make this level n, so we can remove ε-induction1
         record Minimal (x : HOD)  : Set (suc n) where
           field
               min : HOD
               x∋min :   x ∋ min
               min-empty :  (y : HOD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
         open Minimal
         open _∧_
         induction : {x : HOD} → ({y : HOD} → x ∋ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u )
              →  (u : HOD ) → (u∋x : u ∋ x) → Minimal u
         induction {x} prev u u∋x with p∨¬p ((y : Ordinal ) → ¬ (odef x y) ∧ (odef u y))
         ... | case1 P =
              record { min = x
                ;     x∋min = u∋x
                ;     min-empty = λ y → P (& y)
              }
         ... | case2 NP =  min2 where
              p : HOD
              p  = record { od = record { def = λ y1 → odef x  y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where
                 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u)
                 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt))
              np : ¬ (p =h= od∅)
              np p∅ =  NP (λ y p∋y → ∅< {p} {_} (d→∋ p p∋y) p∅ )
              y1choice : choiced (& p)
              y1choice = choice-func p np
              y1 : HOD
              y1 = * (a-choice y1choice)
              y1prop : (x ∋ y1) ∧ (u ∋ y1)
              y1prop = oo∋ (is-in y1choice)
              min2 : Minimal u
              min2 = prev (proj1 y1prop) u (proj2 y1prop)
         Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u
         Min2 x u u∋x = (ε-induction {λ y →  (u : HOD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x )
         cx : {x : HOD} →  ¬ (x =h= od∅ ) → choiced (& x )
         cx {x} nx = choice-func x nx
         minimal : (x : HOD  ) → ¬ (x =h= od∅ ) → HOD
         minimal x ne = min (Min2 (* (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) )
         x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )
         x∋minimal x ne = x∋min (Min2 (* (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) )
         minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (&  y) )
         minimal-1 x ne y = min-empty (Min2 (* (a-choice (cx ne) )) x ( oo∋ (is-in (cx ne)))) y

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
module Data.QuadTree.Implementation.Definition where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Lens.Lens
open import Data.Logic

{-# FOREIGN AGDA2HS
{-# LANGUAGE Safe #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Rank2Types #-}
import Data.Nat
import Data.Lens.Lens
import Data.Logic
#-}

---- Quadrants
-- A quadrant is either a leaf or a node with 4 sub-quadrants

data Quadrant (t : Set) : Set where
  Leaf : t -> Quadrant t
  Node : Quadrant t -> Quadrant t -> Quadrant t -> Quadrant t -> Quadrant t
{-# COMPILE AGDA2HS Quadrant deriving (Show, Eq) #-}

---- QuadTree
-- A quadtree is the width/height + the root quadrant

data QuadTree (t : Set) : Set where
  Wrapper : (Nat × Nat) -> Quadrant t -> QuadTree t
{-# COMPILE AGDA2HS QuadTree deriving (Show, Eq) #-}


text:
{-# OPTIONS --type-in-type #-}
open import Data.Unit
open import Data.Product hiding ( curry ; uncurry )
open import Data.List hiding ( concat )
open import Data.String
open import Relation.Binary.PropositionalEquality
open import Function
module GenericElim.Desc where

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

Label : Set
Label = String

Enum : Set
Enum = List Label

data Tag : Enum → Set where
  here : ∀{l E} → Tag (l ∷ E)
  there : ∀{l E} → Tag E → Tag (l ∷ E)

Branches : (E : Enum) (P : Tag E → Set) → Set
Branches [] P = ⊤
Branches (l ∷ E) P = P here × Branches E (λ t → P (there t))

case : {E : Enum} (P : Tag E → Set) (cs : Branches E P) (t : Tag E) → P t
case P (c , cs) here = c
case P (c , cs) (there t) = case (λ t → P (there t)) cs t

UncurriedBranches : (E : Enum) (P : Tag E → Set) (X : Set)
  → Set
UncurriedBranches E P X = Branches E P → X

CurriedBranches : (E : Enum) (P : Tag E → Set) (X : Set)
  → Set
CurriedBranches [] P X = X
CurriedBranches (l ∷ E) P X = P here → CurriedBranches E (λ t → P (there t)) X

curryBranches : {E : Enum} {P : Tag E → Set} {X : Set}
  → UncurriedBranches E P X → CurriedBranches E P X
curryBranches {[]} f = f tt
curryBranches {l ∷ E} f = λ c → curryBranches (λ cs → f (c , cs))

uncurryBranches : {E : Enum} {P : Tag E → Set} {X : Set}
  → CurriedBranches E P X → UncurriedBranches E P X
uncurryBranches {[]} x tt = x
uncurryBranches {l ∷ E} f (c , cs) = uncurryBranches (f c) cs

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

data Desc (I : Set) : Set₁ where
  End : (i : I) → Desc I
  Rec : (i : I) (D : Desc I) → Desc I
  Arg : (A : Set) (B : A → Desc I) → Desc I

ISet : Set → Set₁
ISet I = I → Set

El : {I : Set} (D : Desc I) → ISet I → ISet I
El (End j) X i = j ≡ i
El (Rec j D) X i = X j × El D X i
El (Arg A B) X i = Σ A (λ a → El (B a) X i)

Hyps : {I : Set} (D : Desc I) (X : ISet I) (P : (i : I) → X i → Set) (i : I) (xs : El D X i) → Set
Hyps (End j) X P i q = ⊤
Hyps (Rec j D) X P i (x , xs) = P j x × Hyps D X P i xs
Hyps (Arg A B) X P i (a , b) = Hyps (B a) X P i b

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

BranchesD : (I : Set) (E : Enum) → Set
BranchesD I E = Branches E (λ _ → Desc I)

caseD : {I : Set} {E : Enum} (cs : BranchesD I E) (t : Tag E) → Desc I
caseD = case (λ _ → Desc _)

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

UncurriedEl : {I : Set} (D : Desc I) (X : ISet I) → Set
UncurriedEl D X = ∀{i} → El D X i → X i

CurriedEl : {I : Set} (D : Desc I) (X : ISet I) → Set
CurriedEl (End i) X = X i
CurriedEl (Rec i D) X = (x : X i) → CurriedEl D X
CurriedEl (Arg A B) X = (a : A) → CurriedEl (B a) X

CurriedEl' : {I : Set} (D : Desc I) (X : ISet I) (i : I) → Set
CurriedEl' (End j) X i = j ≡ i → X i
CurriedEl' (Rec j D) X i = (x : X j) → CurriedEl' D X i
CurriedEl' (Arg A B) X i = (a : A) → CurriedEl' (B a) X i

curryEl : {I : Set} (D : Desc I) (X : ISet I)
  → UncurriedEl D X → CurriedEl D X
curryEl (End i) X cn = cn refl
curryEl (Rec i D) X cn = λ x → curryEl D X (λ xs → cn (x , xs))
curryEl (Arg A B) X cn = λ a → curryEl (B a) X (λ xs → cn (a , xs))

uncurryEl : {I : Set} (D : Desc I) (X : ISet I)
  → CurriedEl D X → UncurriedEl D X
uncurryEl (End i) X cn refl = cn
uncurryEl (Rec i D) X cn (x , xs) = uncurryEl D X (cn x) xs
uncurryEl (Arg A B) X cn (a , xs) = uncurryEl (B a) X (cn a) xs

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

UncurriedHyps : {I : Set} (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedEl D X)
  → Set
UncurriedHyps D X P cn =
  ∀ i (xs : El D X i) (ihs : Hyps D X P i xs) → P i (cn xs)

CurriedHyps : {I : Set} (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedEl D X)
  → Set
CurriedHyps (End i) X P cn =
  P i (cn refl)
CurriedHyps (Rec i D) X P cn =
  (x : X i) → P i x → CurriedHyps D X P (λ xs → cn (x , xs))
CurriedHyps (Arg A B) X P cn =
  (a : A) → CurriedHyps (B a) X P (λ xs → cn (a , xs))

CurriedHyps' : {I : Set} (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (i : I)
  (cn : El D X i → X i)
  → Set
CurriedHyps' (End j) X P i cn = (q : j ≡ i) → P i (cn q)
CurriedHyps' (Rec j D) X P i cn =
  (x : X j) → P j x → CurriedHyps' D X P i (λ xs → cn (x , xs))
CurriedHyps' (Arg A B) X P i cn =
  (a : A) → CurriedHyps' (B a) X P i (λ xs → cn (a , xs))

curryHyps : {I : Set} (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedEl D X)
  → UncurriedHyps D X P cn
  → CurriedHyps D X P cn
curryHyps (End i) X P cn pf =
  pf i refl tt
curryHyps (Rec i D) X P cn pf =
  λ x ih → curryHyps D X P (λ xs → cn (x , xs)) (λ i xs ihs → pf i (x , xs) (ih , ihs))
curryHyps (Arg A B) X P cn pf =
  λ a → curryHyps (B a) X P (λ xs → cn (a , xs)) (λ i xs ihs → pf i (a , xs) ihs)

uncurryHyps : {I : Set} (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedEl D X)
  → CurriedHyps D X P cn
  → UncurriedHyps D X P cn
uncurryHyps (End .i) X P cn pf i refl tt =
  pf
uncurryHyps (Rec j D) X P cn pf i (x , xs) (ih , ihs) =
  uncurryHyps D X P (λ ys → cn (x , ys)) (pf x ih) i xs ihs
uncurryHyps (Arg A B) X P cn pf i (a , xs) ihs =
  uncurryHyps (B a) X P (λ ys → cn (a , ys)) (pf a) i xs ihs

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

data μ {I : Set} (D : Desc I) : ISet I where
  init : UncurriedEl D (μ D)

inj : {I : Set} (D : Desc I) → CurriedEl D (μ D)
inj D = curryEl D (μ D) init

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

ind :
  {I : Set}
  (D : Desc I)
  (P : (i : I) → μ D i → Set)
  (α : UncurriedHyps D (μ D) P init)
  (i : I)
  (x : μ D i)
  → P i x

hyps :
  {I : Set}
  (D₁ : Desc I)
  (P : (i : I) → μ D₁ i → Set)
  (α : UncurriedHyps D₁ (μ D₁) P init)
  (D₂ : Desc I)
  (i : I)
  (xs : El D₂ (μ D₁) i)
  → Hyps D₂ (μ D₁) P i xs

ind D P α i (init xs) = α i xs (hyps D P α D i xs)

hyps D P α (End j) i q = tt
hyps D P α (Rec j A) i (x , xs) = ind D P α j x , hyps D P α A i xs
hyps D P α (Arg A B) i (a , b) = hyps D P α (B a) i b

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

indCurried : {I : Set} (D : Desc I)
  (P : (i : I) → μ D i → Set)
  (f : CurriedHyps D (μ D) P init)
  (i : I)
  (x : μ D i)
  → P i x
indCurried D P f i x = ind D P (uncurryHyps D (μ D) P init f) i x

Summer : {I : Set} (E : Enum) (C : Tag E → Desc I)
  → let D = Arg (Tag E) C in
  (X  : ISet I) (cn : UncurriedEl D X)
  (P : (i : I) → X i → Set)
  → Tag E → Set
Summer E C X cn P t =
  let D = Arg (Tag E) C in
  CurriedHyps (C t) X P (λ xs → cn (t , xs))

SumCurriedHyps : {I : Set} (E : Enum) (C : Tag E → Desc I)
  → let D = Arg (Tag E) C in
  (P : (i : I) → μ D i → Set)
  → Tag E → Set
SumCurriedHyps E C P t =
  let D = Arg (Tag E) C in
  Summer E C (μ D) init P t

elimUncurried : {I : Set} (E : Enum) (C : Tag E → Desc I)
  → let D = Arg (Tag E) C in
  (P : (i : I) → μ D i → Set)
  → Branches E (SumCurriedHyps E C P)
  → (i : I) (x : μ D i) → P i x
elimUncurried E C P cs i x =
  let D = Arg (Tag E) C in
  indCurried D P
    (case (SumCurriedHyps E C P) cs)
    i x

elim : {I : Set} (E : Enum) (C : Tag E → Desc I)
  → let D = Arg (Tag E) C in
  (P : (i : I) → μ D i → Set)
  → CurriedBranches E
      (SumCurriedHyps E C P)
      ((i : I) (x : μ D i) → P i x)
elim E C P = curryBranches (elimUncurried E C P)

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

Soundness : Set₁
Soundness = {I : Set} (E : Enum) (C : Tag E → Desc I)
  → let D = Arg (Tag E) C in
  (P : (i : I) → μ D i → Set)
  (cs : Branches E (SumCurriedHyps E C P))
  (i : I) (x : μ D i)
  → ∃ λ α
  → elimUncurried E C P cs i x ≡ ind D P α i x

sound : Soundness
sound E C P cs i x =
  let D = Arg (Tag E) C in
  (uncurryHyps D (μ D) P init (case (SumCurriedHyps E C P) cs)) , refl

Completeness : Set₁
Completeness = {I : Set} (E : Enum) (C : Tag E → Desc I)
  → let D = Arg (Tag E) C in
  (P : (i : I) → μ D i → Set)
  (α : UncurriedHyps D (μ D) P init)
  (i : I) (x : μ D i)
  → ∃ λ cs
  → ind D P α i x ≡ elimUncurried E C P cs i x

uncurryHypsIdent : {I : Set} (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedEl D X)
  (α : UncurriedHyps D X P cn)
  (i : I) (xs : El D X i) (ihs : Hyps D X P i xs)
  → α i xs ihs ≡ uncurryHyps D X P cn (curryHyps D X P cn α) i xs ihs
uncurryHypsIdent (End .i) X P cn α i refl tt = refl
uncurryHypsIdent (Rec j D) X P cn α i (x , xs) (p , ps) =
  uncurryHypsIdent D X P (λ xs → cn (x , xs)) (λ k ys rs → α k (x , ys) (p , rs)) i xs ps
uncurryHypsIdent (Arg A B) X P cn α i (a , xs) ps =
  uncurryHypsIdent (B a) X P (λ xs → cn (a , xs)) (λ j ys → α j (a , ys)) i xs ps

postulate
  ext3 : {A : Set} {B : A → Set} {C : (a : A) → B a → Set} {Z : (a : A) (b : B a) → C a b → Set}
    (f g : (a : A) (b : B a) (c : C a b) → Z a b c)
    → ((a : A) (b : B a) (c : C a b) → f a b c ≡ g a b c)
    → f ≡ g

toBranches : {I : Set} (E : Enum) (C : Tag E → Desc I)
  → let D = Arg (Tag E) C in
  (X  : ISet I) (cn : UncurriedEl D X)
  (P : (i : I) → X i → Set)
  (α : UncurriedHyps D X P cn)
  → Branches E (Summer E C X cn P)
toBranches [] C X cn P α = tt
toBranches (l ∷ E) C X cn P α =
    curryHyps (C here) X P (λ xs → cn (here , xs)) (λ i xs → α i (here , xs))
  , toBranches E (λ t → C (there t)) X
     (λ xs → cn (there (proj₁ xs) , proj₂ xs))
     P (λ i xs ih → α i (there (proj₁ xs) , proj₂ xs) ih)

ToBranches : {I : Set} {E : Enum} (C : Tag E → Desc I)
  → let D = Arg (Tag E) C in
  (X  : ISet I) (cn : UncurriedEl D X)
  (P : (i : I) → X i → Set)
  (α : UncurriedHyps D X P cn)
  (t : Tag E)
  → let β = toBranches E C X cn P α in
  case (Summer E C X cn P) β t ≡ curryHyps D X P cn α t
ToBranches C X cn P α here = refl
ToBranches C X cn P α (there t)
  with ToBranches (λ t → C (there t)) X
    (λ xs → cn (there (proj₁ xs) , proj₂ xs))
    P (λ i xs ih → α i (there (proj₁ xs) , proj₂ xs) ih) t
... | ih rewrite ih = refl

completeα : {I : Set} (E : Enum) (C : Tag E → Desc I)
  → let D = Arg (Tag E) C in
  (P : (i : I) → μ D i → Set)
  (α : UncurriedHyps D (μ D) P init)
  (i : I) (xs : El D (μ D) i) (ihs : Hyps D (μ D) P i xs)
  → let β = toBranches E C (μ D) init P α in
  α i xs ihs ≡ uncurryHyps D (μ D) P init (case (SumCurriedHyps E C P) β) i xs ihs
completeα E C P α i (t , xs) ihs
  with ToBranches C (μ D) init P α t where D = Arg (Tag E) C
... | q rewrite q = uncurryHypsIdent D (μ D) P init α i (t , xs) ihs where D = Arg (Tag E) C

complete' : {I : Set} (E : Enum) (C : Tag E → Desc I)
  → let D = Arg (Tag E) C in
  (P : (i : I) → μ D i → Set)
  (α : UncurriedHyps D (μ D) P init)
  (i : I) (x : μ D i)
  → let β = toBranches E C (μ D) init P α in
  ind D P α i x ≡ elimUncurried E C P β i x
complete' E C P α i (init (t , xs)) = cong
  (λ f → ind D P f i (init (t , xs)))
  (ext3 α
    (uncurryHyps D (μ D) P init (case (SumCurriedHyps E C P) β))
    (completeα E C P α))
  where
  D = Arg (Tag E) C
  β = toBranches E C (μ D) init P α

complete : Completeness
complete E C P α i x =
  let D = Arg (Tag E) C in
    toBranches E C (μ D) init P α
  , complete' E C P α i x

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

ℕE : Enum
ℕE = "zero" ∷ "suc" ∷ []

VecE : Enum
VecE = "nil" ∷ "cons" ∷ []

ℕT : Set
ℕT = Tag ℕE

VecT : Set
VecT = Tag VecE

zeroT : ℕT
zeroT = here

sucT : ℕT
sucT = there here

nilT : VecT
nilT = here

consT : VecT
consT = there here

ℕC : ℕT → Desc ⊤
ℕC = caseD $
    End tt
  , Rec tt (End tt)
  , tt

ℕD : Desc ⊤
ℕD = Arg ℕT ℕC

ℕ : ⊤ → Set
ℕ = μ ℕD

zero : ℕ tt
zero = init (zeroT , refl)

suc : ℕ tt → ℕ tt
suc n = init (sucT , n , refl)

VecC : (A : Set) → VecT → Desc (ℕ tt)
VecC A = caseD $
    End zero
  , Arg (ℕ tt) (λ n → Arg A λ _ → Rec n (End (suc n)))
  , tt

nilD : (A : Set) → Desc (ℕ tt)
nilD A = End zero

consD : (A : Set) → Desc (ℕ tt)
consD A = Arg (ℕ tt) (λ n → Arg A (λ _ → Rec n (End (suc n))))

VecD : (A : Set) → Desc (ℕ tt)
VecD A = Arg VecT (VecC A)

Vec : (A : Set) → ℕ tt → Set
Vec A = μ (VecD A)

NilEl : (A : Set) (n : ℕ tt) → Set
NilEl A n = El (nilD A) (Vec A) n

ConsEl : (A : Set) → ℕ tt → Set
ConsEl A n = El (consD A) (Vec A) n

VecEl : (A : Set) → ℕ tt → Set
VecEl A n = El (VecD A) (Vec A) n

NilHyps : (A : Set) (P : (n : ℕ tt) → Vec A n → Set) (n : ℕ tt) (xs : NilEl A n) → Set
NilHyps A P n xs = Hyps (nilD A) (Vec A) P n xs

ConsHyps : (A : Set) (P : (n : ℕ tt) → Vec A n → Set) (n : ℕ tt) (xs : ConsEl A n) → Set
ConsHyps A P n xs = Hyps (consD A) (Vec A) P n xs

VecHyps : (A : Set) (P : (n : ℕ tt) → Vec A n → Set) (n : ℕ tt) (xs : VecEl A n) → Set
VecHyps A P n xs = Hyps (VecD A) (Vec A) P n xs

ConsUncurriedHyps : (A : Set)
  (P : (n : ℕ tt) → Vec A n → Set)
  (cn : UncurriedEl (consD A) (Vec A)) → Set
ConsUncurriedHyps A P cn = UncurriedHyps (consD A) (Vec A) P cn

nil : (A : Set) → Vec A zero
nil A = init (nilT , refl)

cons : (A : Set) (n : ℕ tt) (x : A) (xs : Vec A n) → Vec A (suc n)
cons A n x xs = init (consT , n , x , xs , refl)

nil2 : (A : Set) → Vec A zero
nil2 A = inj (VecD A) nilT

cons2 : (A : Set) (n : ℕ tt) (x : A) (xs : Vec A n) → Vec A (suc n)
cons2 A = inj (VecD A) consT

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

module Induction where

  add : ℕ tt → ℕ tt → ℕ tt
  add = ind ℕD (λ _ _ → ℕ tt → ℕ tt)
    (λ u t,c → case
      (λ t → (c : El (ℕC t) ℕ u)
             (ih : Hyps ℕD ℕ (λ u n → ℕ u → ℕ u) u (t , c))
             → ℕ u → ℕ u
      )
      ( (λ q ih n → n)
      , (λ m,q ih,tt n → suc (proj₁ ih,tt n))
      , tt
      )
      (proj₁ t,c)
      (proj₂ t,c)
    )
    tt

  mult : ℕ tt → ℕ tt → ℕ tt
  mult = ind ℕD (λ _ _ → ℕ tt → ℕ tt)
    (λ u t,c → case
      (λ t → (c : El (ℕC t) ℕ u)
             (ih : Hyps ℕD ℕ (λ u n → ℕ u → ℕ u) u (t , c))
             → ℕ u → ℕ u
      )
      ( (λ q ih n → zero)
      , (λ m,q ih,tt n → add n (proj₁ ih,tt n))
      , tt
      )
      (proj₁ t,c)
      (proj₂ t,c)
    )
    tt

  append : (A : Set) (m : ℕ tt) (xs : Vec A m) (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)
  append A = ind (VecD A) (λ m xs → (n : ℕ tt) (ys : Vec A n) → Vec A (add m n))
    (λ m t,c → case
      (λ t → (c : El (VecC A t) (Vec A) m)
             (ih : Hyps (VecD A) (Vec A) (λ m xs → (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)) m (t , c))
             (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)
      )
      ( (λ q ih n ys → subst (λ m → Vec A (add m n)) q ys)
      , (λ m',x,xs,q ih,tt n ys →
          let m' = proj₁ m',x,xs,q
              x = proj₁ (proj₂ m',x,xs,q)
              q = proj₂ (proj₂ (proj₂ m',x,xs,q))
              ih = proj₁ ih,tt
          in
          subst (λ m → Vec A (add m n)) q (cons A (add m' n) x (ih n ys))
        )
      , tt
      )
      (proj₁ t,c)
      (proj₂ t,c)
    )

  Concat : (A : Set) (m n : ℕ tt) (xss : Vec (Vec A m) n) → Set
  Concat A m n xss = Vec A (mult n m)

  ConsBranch : (A : Set) (m : ℕ tt)
    → Set
  ConsBranch A m = UncurriedHyps (consD (Vec A m)) (Vec (Vec A m)) (Concat A m)
    (λ xs → init (consT , xs))

  ConsElimBranch : (A : Set) (m : ℕ tt)
    → Set
  ConsElimBranch A m = CurriedHyps (consD (Vec A m)) (Vec (Vec A m)) (Concat A m)
    (λ xs → init (consT , xs))

  ElimBranch : (t : VecT) (A : Set) (m : ℕ tt)
    → Set
  ElimBranch t A m = SumCurriedHyps VecE (VecC (Vec A m)) (Concat A m) t

  nilBranch : (A : Set) (m n : ℕ tt)
    (xss : NilEl (Vec A m) n)
    (ihs : NilHyps (Vec A m) (Concat A m) n xss)
    → Vec A (mult n m)
  nilBranch A m n q u = subst
    (λ n → Vec A (mult n m))
    q (nil A)

  consBranch : (A : Set) (m : ℕ tt) → ConsBranch A m
  consBranch A m n n',xs,xss,q ih,u =
    let n' = proj₁ n',xs,xss,q
        xs = proj₁ (proj₂ n',xs,xss,q)
        q = proj₂ (proj₂ (proj₂ n',xs,xss,q))
        ih = proj₁ ih,u
    in subst
      (λ n → Vec A (mult n m))
      q (append A m xs (mult n' m) ih)

  ConcatConvoy : (A : Set) (m n : ℕ tt) (t : VecT) → Set
  ConcatConvoy A m n t =
    (xss : El (VecC (Vec A m) t) (Vec (Vec A m)) n)
    (ihs : VecHyps (Vec A m) (Concat A m) n (t , xss))
    → Vec A (mult n m)

  concatα : (A : Set) (m n : ℕ tt)
    (xss : VecEl (Vec A m) n)
    (ihs : VecHyps (Vec A m) (Concat A m) n xss)
    → Vec A (mult n m)
  concatα A m n xss = case (ConcatConvoy A m n)
    (nilBranch A m n , consBranch A m n , tt)
    (proj₁ xss)
    (proj₂ xss)

  concat : (A : Set) (m n : ℕ tt) (xss : Vec (Vec A m) n) → Concat A m n xss
  concat A m = ind
    (VecD (Vec A m))
    (Concat A m)
    (concatα A m)

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

module GenericElim where

  add : ℕ tt → ℕ tt → ℕ tt
  add = elim ℕE ℕC _
    (λ n → n)
    (λ m ih n → suc (ih n))
    tt

  mult : ℕ tt → ℕ tt → ℕ tt
  mult = elim ℕE ℕC _
    (λ n → zero)
    (λ m ih n → add n (ih n))
    tt

  append : (A : Set) (m : ℕ tt) (xs : Vec A m) (n : ℕ tt) (ys : Vec A n) → Vec A (add m n)
  append A = elim VecE (VecC A) (λ m xs → (n : ℕ tt) (ys : Vec A n) → Vec A (add m n))
    (λ n ys → ys)
    (λ m x xs ih n ys → cons A (add m n) x (ih n ys))

  concat : (A : Set) (m n : ℕ tt) (xss : Vec (Vec A m) n) → Vec A (mult n m)
  concat A m = elim VecE (VecC (Vec A m)) (λ n xss → Vec A (mult n m))
    (nil A)
    (λ n xs xss ih → append A m xs (mult n m) ih)

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

max_stars_repo_name: larrytheliquid/generic-elim

max_issues_repo_name: larrytheliquid/generic-elim

max_forks_repo_name: larrytheliquid/generic-elim


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bounded vectors (inefficient, concrete implementation)
------------------------------------------------------------------------

-- Vectors of a specified maximum length.

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

module Data.BoundedVec.Inefficient where

open import Data.Nat.Base
open import Data.List.Base

------------------------------------------------------------------------
-- The type

infixr 5 _∷_

data BoundedVec {a} (A : Set a) : ℕ → Set a where
  []  : ∀ {n} → BoundedVec A n
  _∷_ : ∀ {n} (x : A) (xs : BoundedVec A n) → BoundedVec A (suc n)

------------------------------------------------------------------------
-- Increasing the bound

-- Note that this operation is linear in the length of the list.

↑ : ∀ {a n} {A : Set a} → BoundedVec A n → BoundedVec A (suc n)
↑ []       = []
↑ (x ∷ xs) = x ∷ ↑ xs

------------------------------------------------------------------------
-- Conversions

fromList : ∀ {a} {A : Set a} → (xs : List A) → BoundedVec A (length xs)
fromList []       = []
fromList (x ∷ xs) = x ∷ fromList xs

toList : ∀ {a n} {A : Set a} → BoundedVec A n → List A
toList []       = []
toList (x ∷ xs) = x ∷ toList xs