text:
-- Properties of Fibonacci nunmbers

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

module Math.NumberTheory.Fibonacci.Nat.Properties where

-- agda-stdlib
open import Data.Unit using (tt)
open import Data.Sum
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Function.Base

-- agda-misc
open import Math.NumberTheory.Fibonacci.Nat
open import Math.NumberTheory.Summation.Nat

open ≤-Reasoning

1≤fib[1+n] : ∀ n → 1 ≤ fib (suc n)
1≤fib[1+n] zero    = ≤-refl
1≤fib[1+n] (suc n) = begin
  1                   ≤⟨ 1≤fib[1+n] n ⟩
  fib (suc n)         ≤⟨ m≤m+n (fib (suc n)) (fib n) ⟩
  fib (suc n) + fib n ≡⟨ fib[1+n]+fib[n]≡fib[2+n] n ⟩
  fib (suc (suc n))   ∎

fib[n]<fib[1+n] : ∀ n {_ : True (2 ≤? n)} → fib n < fib (suc n)
fib[n]<fib[1+n] (suc (suc zero))    {wit} = s≤s (s≤s z≤n)
fib[n]<fib[1+n] (suc (suc (suc n))) {wit} = begin-strict
  fib (3 + n)               <⟨ ≤-refl ⟩
  1 + fib (3 + n)           ≡⟨ +-comm 1 (fib (3 + n)) ⟩
  fib (3 + n) + 1           ≤⟨ +-monoʳ-≤ (fib (3 + n)) (1≤fib[1+n] (suc n)) ⟩
  fib (3 + n) + fib (2 + n) ≡⟨ fib[1+n]+fib[n]≡fib[2+n] (2 + n) ⟩
  fib (4 + n)               ∎

private
  fib-mono-<-lemma : ∀ m n {_ : True (2 ≤? n)} → fib n < fib (suc m + n)
  fib-mono-<-lemma zero    n               {wit} = fib[n]<fib[1+n] n {wit}
  fib-mono-<-lemma (suc m) n@(suc (suc _)) {wit} = begin-strict
    fib n                           <⟨ fib-mono-<-lemma m n {tt} ⟩
    fib (1 + (m + n))               ≤⟨ m≤m+n (fib (1 + (m + n))) (fib (m + n)) ⟩
    fib (1 + (m + n)) + fib (m + n) ≡⟨ fib[1+n]+fib[n]≡fib[2+n] (m + n) ⟩
    fib (2 + (m + n))               ∎

fib-mono-< : ∀ m n {_ : True (2 ≤? m)} → m < n → fib m < fib n
fib-mono-< m n {wit} m<n = begin-strict
  fib m           <⟨ fib-mono-<-lemma o m {wit} ⟩
  fib (1 + o + m) ≡⟨ cong fib (sym $ n≡1+o+m) ⟩
  fib n           ∎
  where
  o = n ∸ suc m
  n≡1+o+m : n ≡ 1 + o + m
  n≡1+o+m = trans (sym $ m+[n∸m]≡n m<n) (cong suc (+-comm m o))

private
  ≤⇒≡∨< : ∀ {m n} → m ≤ n → (m ≡ n) ⊎ (m < n)
  ≤⇒≡∨< {m} {n} m≤n with m ≟ n
  ... | yes m≡n = inj₁ m≡n
  ... | no  m≢n = inj₂ (≤∧≢⇒< m≤n m≢n)

fib-mono-≤ : ∀ m n → m ≤ n → fib m ≤ fib n
fib-mono-≤ zero            n       m≤n = z≤n
fib-mono-≤ (suc zero)      (suc n) m≤n = 1≤fib[1+n] n
fib-mono-≤ m@(suc (suc _)) n       m≤n with ≤⇒≡∨< m≤n
... | inj₁ m≡n = ≤-reflexive (cong fib m≡n)
... | inj₂ m<n = <⇒≤ $ fib-mono-< m n {tt} m<n

sum-of-fib : ∀ n → Σ[ k ≤ n ] fib k ≡ fib (2 + n) ∸ 1
sum-of-fib zero    = refl
sum-of-fib (suc n) = begin-equality
  Σ[ k ≤ n ] fib k + fib (suc n)
    ≡⟨ cong (_+ fib (suc n)) $ sum-of-fib n ⟩
  (fib (2 + n) ∸ 1) + fib (1 + n)
    ≡⟨ +-comm (fib (2 + n) ∸ 1) (fib (1 + n)) ⟩
  fib (1 + n) + (fib (2 + n) ∸ 1)
    ≡⟨ sym $ +-∸-assoc (fib (1 + n)) (1≤fib[1+n] (suc n)) ⟩
  (fib (1 + n) + fib (2 + n)) ∸ 1
    ≡⟨ cong (_∸ 1) $ fib[n]+fib[1+n]≡fib[2+n] (suc n) ⟩
  fib (3 + n) ∸ 1
    ∎


text:
open import Nat
open import Prelude
open import core
open import contexts
open import lemmas-consistency
open import lemmas-disjointness
open import weakening

module typed-elaboration where
  mutual
    typed-elaboration-synth : {Γ : tctx} {e : hexp} {τ : htyp} {d : ihexp} {Δ : hctx} →
                            Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                            Δ , Γ ⊢ d :: τ
    typed-elaboration-synth ESConst = TAConst
    typed-elaboration-synth (ESVar x₁) = TAVar x₁
    typed-elaboration-synth (ESLam x₁ ex) = TALam x₁ (typed-elaboration-synth ex)
    typed-elaboration-synth (ESAp {Δ1 = Δ1} _ d x₁ x₂ x₃ x₄)
      with typed-elaboration-ana x₃ | typed-elaboration-ana x₄
    ... | con1 , ih1 | con2 , ih2  = TAAp (TACast (weaken-ta-Δ1 d ih1) con1) (TACast (weaken-ta-Δ2 {Δ1 = Δ1} d ih2) con2)
    typed-elaboration-synth (ESEHole {Γ = Γ} {u = u})  = TAEHole (ctx-top ∅ u (Γ , ⦇-⦈) refl)(STAId (λ x τ z → z))
    typed-elaboration-synth (ESNEHole {Γ = Γ} {τ = τ} {u = u} {Δ = Δ} (d1 , d2) ex)
      with typed-elaboration-synth ex
    ... | ih1 = TANEHole {Δ = Δ ,, (u , Γ , ⦇-⦈)} (ctx-top Δ u (Γ , ⦇-⦈) (d2 u (lem-domsingle _ _))) (weaken-ta-Δ1 (d1 , d2) ih1)(STAId (λ x τ₁ z → z))
    typed-elaboration-synth (ESAsc x)
      with typed-elaboration-ana x
    ... | con , ih = TACast ih con

    typed-elaboration-ana : {Γ : tctx} {e : hexp} {τ τ' : htyp} {d : ihexp} {Δ : hctx} →
                          Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                          (τ' ~ τ) × (Δ , Γ ⊢ d :: τ')
    typed-elaboration-ana (EALam x₁ MAHole ex)
      with typed-elaboration-ana ex
    ... | con , D = TCHole1 , TALam x₁ D
    typed-elaboration-ana (EALam x₁ MAArr ex)
      with typed-elaboration-ana ex
    ... | con , D = TCArr TCRefl con , TALam x₁ D
    typed-elaboration-ana (EASubsume x x₁ x₂ x₃) = ~sym x₃ , typed-elaboration-synth x₂
    typed-elaboration-ana (EAEHole {Γ = Γ} {u = u}) = TCRefl , TAEHole (ctx-top ∅ u (Γ , _) refl) (STAId (λ x τ z → z))
    typed-elaboration-ana (EANEHole {Γ = Γ} {u = u} {τ = τ} {Δ = Δ} (d1 , d2) x)
      with typed-elaboration-synth x
    ... | ih1 = TCRefl , TANEHole {Δ = Δ ,, (u , Γ , τ)} (ctx-top Δ u (Γ , τ) (d2 u (lem-domsingle _ _)) ) (weaken-ta-Δ1 (d1 , d2) ih1) (STAId (λ x₁ τ₁ z → z))

ext: agda

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
module Ag07 where

open import IO

data W (A : Set) (B : A → Set) : Set where
  sup : (a : A) → (b : B a → W A B) → W A B

module WBinTree where
  data Tree : Set where
    Leaf : Tree
    Node : Tree

  data Direction : Set where
    Left  : Direction
    Right : Direction

  data Bottom : Set where

  void : ∀ {A : Set} → Bottom → A
  void ()

  binTree : Tree → Set
  binTree Leaf = Bottom
  binTree Node = Direction

  BinTree : Set
  BinTree = W Tree binTree

  leaf : BinTree
  leaf = sup Leaf void

  node : BinTree → BinTree → BinTree
  node x y = sup Node λ {
    Left  → x ;
    Right → y }

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
module Implicits.Resolution.Ambiguous.SystemFEquiv where

open import Prelude

open import Function.Equivalence using (_⇔_; equivalence)
open import Data.List.Properties
open import Relation.Binary.HeterogeneousEquality as H using ()
open import Data.Vec.Properties as VP using ()
open import Data.Vec hiding ([_])
open import Extensions.Vec
open import Data.List as List using ()
open import Data.Product hiding (map)

open import Implicits.Syntax
open import Implicits.Resolution.Ambiguous.Resolution
open import Implicits.Resolution.Embedding
open import Implicits.Resolution.Embedding.Lemmas

open import SystemF.Everything
     as F using ()

⟦_⟧term→ : ∀ {ν} {Δ : ICtx ν} {r} → Δ ⊢ᵣ r → F.Term ν (List.length (List.map ⟦_⟧tp→ Δ))
⟦_⟧term→ {ν} {Δ} (r-tabs x) = F.Λ (subst (F.Term (suc ν)) (length-weaken-Δ Δ) ⟦ x ⟧term→)
⟦ r-tapp a x ⟧term→ = ⟦ x ⟧term→ F.[ ⟦ a ⟧tp→ ]
⟦_⟧term→ {Δ = Δ} (r-ivar x) =
  F.var (subst Fin (sym $ length-map _ Δ) (proj₁ $ ∈⟶index (VP.List-∈⇒∈ x)))
⟦ r-iabs {a = a} x ⟧term→ = F.λ' ⟦ a ⟧tp→ ⟦ x ⟧term→
⟦ r-iapp f e ⟧term→ = ⟦ f ⟧term→ F.· ⟦ e ⟧term→

from-⊢ : ∀ {ν n t a} {Γ : F.Ctx ν n} → Γ F.⊢ t ∈ a → ⟦ Γ ⟧ctx← ⊢ᵣ ⟦ a ⟧tp←
from-⊢ (F.var x) = r-ivar (lookup-∈ x _)
from-⊢ {Γ = Γ} (F.Λ x) = r-tabs (subst (λ u → u ⊢ᵣ _) (⟦weaken⟧ctx← Γ) (from-⊢ x))
from-⊢ (F.λ' {b = b} a x) = r-iabs (from-⊢ x)
from-⊢ {Γ = Γ} (F._[_] {a = a} x b) = subst
  (λ u → ⟦ Γ ⟧ctx← ⊢ᵣ u)
  (sym (⟦a/sub⟧tp← a b))
  (r-tapp ⟦ b ⟧tp← (from-⊢ x))
from-⊢ (a F.· b) = r-iapp (from-⊢ a) (from-⊢ b)

to-⊢ : ∀ {ν} {Δ : ICtx ν} {r} → (p : Δ ⊢ᵣ r) → ⟦ Δ ⟧ctx→ F.⊢ ⟦ p ⟧term→ ∈ ⟦ r ⟧tp→
to-⊢ {Δ = Δ} (r-tabs {r = r} p) with to-⊢ p
to-⊢ {Δ = Δ} (r-tabs {r = r} p) | x =
  F.Λ (⊢subst-n (length-weaken-Δ Δ) (H.sym (⟦weaken⟧ctx→ Δ)) x)
to-⊢ (r-tapp a p) with to-⊢ p
to-⊢ {Δ = Δ} (r-tapp {r = a} b p) | x =
  subst
    (λ u → ⟦ Δ ⟧ctx→ F.⊢ ⟦ p ⟧term→ F.[ ⟦ b ⟧tp→ ] ∈ u)
    (sym $ ⟦a/sub⟧tp→ a b)
    (x F.[ ⟦ b ⟧tp→ ])
to-⊢ {Δ = Δ} {r = r} (r-ivar x) =
  let i , eq = ∈⟶index (VP.List-∈⇒∈ x) in
      let i' = (subst Fin (sym $ length-map _ Δ) i) in
        subst (λ u → ⟦ Δ ⟧ctx→ F.⊢ (F.var i') ∈ u) (lookup⟦⟧ Δ i eq) (F.var i')
to-⊢ (r-iabs {a = a} p) = F.λ' ⟦ a ⟧tp→ (to-⊢ p)
to-⊢ (r-iapp p p₁) = (to-⊢ p) F.· (to-⊢ p₁)

equivalent : ∀ {ν} (Δ : ICtx ν) r → Δ ⊢ᵣ r ⇔ (∃ λ t → ⟦ Δ ⟧ctx→ F.⊢ t ∈ ⟦ r ⟧tp→)
equivalent Δ r = equivalence
  (λ x → , (to-⊢ x))
  (λ x → subst₂ (λ Δ' r' → Δ' ⊢ᵣ r') (ctx→← _) (tp→← r) (from-⊢ (proj₂ x)))

⊢subst : ∀ {ν n n'} {a a' : F.Type ν} {Γ : F.Ctx ν n} {Γ' : F.Ctx ν n'} →
          n ≡ n' → a ≡ a' → Γ H.≅ Γ' →
          (∃ λ t → Γ F.⊢ t ∈ a) →
          ∃ λ t → Γ' F.⊢ t ∈ a'
⊢subst refl refl H.refl p = p

equivalent' : ∀ {ν n} (Γ : F.Ctx ν n) r → ⟦ Γ ⟧ctx← ⊢ᵣ ⟦ r ⟧tp← ⇔ (∃ λ t → Γ F.⊢ t ∈ r)
equivalent' Γ r = equivalence
  (λ x → ⊢subst
    (length-map-toList (map ⟦_⟧tp← Γ)) (tp←→ r) (ctx←→ Γ) (, to-⊢ x))
  (λ x → (from-⊢ (proj₂ x)))


text:
------------------------------------------------------------------------
-- Pointed and non-pointed ω-cpos
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

module Omega-cpo where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (T)

open import Equivalence equality-with-J as Eq using (_≃_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J

open import Partiality-algebra as PA hiding (_∘_)
import Partiality-monad.Inductive.Monad.Adjunction as PA

-- Possibly non-pointed ω-cpos (with propositional ordering
-- relations).

record ω-cpo p q : Type (lsuc (p ⊔ q)) where

  infix 4 _⊑_

  -- Partial order axioms.

  field
    Carrier         : Type p
    _⊑_             : Carrier → Carrier → Type q
    reflexivity     : ∀ {x} → x ⊑ x
    antisymmetry    : ∀ {x y} → x ⊑ y → y ⊑ x → x ≡ y
    transitivity    : ∀ {x y z} → x ⊑ y → y ⊑ z → x ⊑ z
    ⊑-propositional : ∀ {x y} → Is-proposition (x ⊑ y)

  -- Increasing sequences.

  Increasing-sequence : Type (p ⊔ q)
  Increasing-sequence = ∃ λ (f : ℕ → Carrier) → ∀ n → f n ⊑ f (suc n)

  -- Projection functions for Increasing-sequence.

  infix 30 _[_]

  _[_] : Increasing-sequence → ℕ → Carrier
  _[_] = proj₁

  increasing : (s : Increasing-sequence) →
               ∀ n → (s [ n ]) ⊑ (s [ suc n ])
  increasing = proj₂

  -- Upper bounds.

  Is-upper-bound : Increasing-sequence → Carrier → Type q
  Is-upper-bound s x = ∀ n → (s [ n ]) ⊑ x

  -- Upper bound axioms.

  field
    ⨆                 : Increasing-sequence → Carrier
    upper-bound       : ∀ s → Is-upper-bound s (⨆ s)
    least-upper-bound : ∀ {s ub} → Is-upper-bound s ub → ⨆ s ⊑ ub

  -- The carrier type is a set. (This lemma is analogous to
  -- Theorem 11.3.9 in "Homotopy Type Theory: Univalent Foundations of
  -- Mathematics" (first edition).)

  Carrier-is-set : Is-set Carrier
  Carrier-is-set = proj₁ $ Eq.propositional-identity≃≡
    (λ x y → x ⊑ y × y ⊑ x)
    (λ _ _ → ×-closure 1 ⊑-propositional ⊑-propositional)
    (λ _ → reflexivity , reflexivity)
    (λ x y → uncurry {B = λ _ → y ⊑ x} antisymmetry)

-- Every set can be turned into an ω-cpo.

Set→ω-cpo : ∀ {ℓ} → Set ℓ → ω-cpo ℓ ℓ
Set→ω-cpo (A , A-set) = record
  { Carrier           = A
  ; _⊑_               = _≡_
  ; reflexivity       = refl
  ; antisymmetry      = const
  ; transitivity      = trans
  ; ⊑-propositional   = A-set
  ; ⨆                 = (_$ 0) ∘ proj₁
  ; upper-bound       = uncurry upper-bound
  ; least-upper-bound = _$ 0
  }
  where
  upper-bound : (f : ℕ → A) → (∀ n → f n ≡ f (suc n)) →
                ∀ n → f n ≡ f 0
  upper-bound f inc zero    = refl
  upper-bound f inc (suc n) =
    f (suc n)  ≡⟨ sym (inc n) ⟩
    f n        ≡⟨ upper-bound f inc n ⟩∎
    f 0        ∎

-- Pointed ω-cpos.

record ω-cppo p q : Type (lsuc (p ⊔ q)) where
  field
    cpo : ω-cpo p q

  open ω-cpo cpo public

  field
    least  : Carrier
    least⊑ : ∀ {x} → least ⊑ x

-- A pointed ω-CPO is equivalent to a partiality algebra over the
-- empty type.

ω-cppo≃ω-cppo : ∀ {p q} → ω-cppo p q ≃ PA.ω-cppo p q
ω-cppo≃ω-cppo = Eq.↔⇒≃ record
  { surjection = record
    { logical-equivalence = record
      { to   = λ X → let open ω-cppo X in record
                 { T                       = Carrier
                 ; partiality-algebra-with = record
                   { _⊑_               = _⊑_
                   ; never             = least
                   ; now               = λ ()
                   ; ⨆                 = ⨆
                   ; antisymmetry      = antisymmetry
                   ; T-is-set-unused   = Carrier-is-set
                   ; ⊑-refl            = λ _ → reflexivity
                   ; ⊑-trans           = transitivity
                   ; never⊑            = λ _ → least⊑
                   ; upper-bound       = upper-bound
                   ; least-upper-bound = λ _ _ → least-upper-bound
                   ; ⊑-propositional   = ⊑-propositional
                   }
                 }
      ; from = λ P → let open Partiality-algebra P in record
                 { cpo = record
                   { Carrier           = T
                   ; _⊑_               = _⊑_
                   ; reflexivity       = ⊑-refl _
                   ; antisymmetry      = antisymmetry
                   ; transitivity      = ⊑-trans
                   ; ⊑-propositional   = ⊑-propositional
                   ; ⨆                 = ⨆
                   ; upper-bound       = upper-bound
                   ; least-upper-bound = least-upper-bound _ _
                   }
                 ; least  = never
                 ; least⊑ = never⊑ _
                 }
      }
    ; right-inverse-of = λ P →
        let open Partiality-algebra P in
        cong₂ (λ now (T-is-set : Is-set T) → record
                 { T                       = T
                 ; partiality-algebra-with = record
                   { _⊑_               = _⊑_
                   ; never             = never
                   ; now               = now
                   ; ⨆                 = ⨆
                   ; antisymmetry      = antisymmetry
                   ; T-is-set-unused   = T-is-set
                   ; ⊑-refl            = ⊑-refl
                   ; ⊑-trans           = ⊑-trans
                   ; never⊑            = never⊑
                   ; upper-bound       = upper-bound
                   ; least-upper-bound = least-upper-bound
                   ; ⊑-propositional   = ⊑-propositional
                   }
                 })
              (⟨ext⟩ λ ())
              (H-level-propositional ext 2 _ _)
    }
  ; left-inverse-of = λ _ → refl
  }

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
open import Nat
open import Prelude
open import dynamics-core
open import contexts
open import lemmas-consistency
open import type-assignment-unicity
open import lemmas-progress-checks

-- taken together, the theorems in this file argue that for any expression
-- d, at most one summand of the labeled sum that results from progress may
-- be true at any time: that boxed values, indeterminates, and expressions
-- that step are pairwise disjoint.
--
-- note that as a consequence of currying and comutativity of products,
-- this means that there are three theorems to prove. in addition to those,
-- we also prove several convenince forms that combine theorems about
-- indeterminate and boxed value forms into the same statement about final
-- forms, which mirrors the mutual definition of indeterminate and final
-- and saves some redundant argumentation.
module progress-checks where
  -- boxed values are not indeterminates
  boxedval-not-indet : ∀{d} → d boxedval → d indet → ⊥
  boxedval-not-indet (BVVal VNum) ()
  boxedval-not-indet (BVVal VLam) ()
  boxedval-not-indet (BVArrCast x bv) (ICastArr x₁ ind) = boxedval-not-indet bv ind
  boxedval-not-indet (BVHoleCast x bv) (ICastGroundHole x₁ ind) = boxedval-not-indet bv ind
  boxedval-not-indet (BVHoleCast x bv) (ICastHoleGround x₁ ind x₂) = boxedval-not-indet bv ind
  boxedval-not-indet (BVVal (VInl x)) (IInl ind) = boxedval-not-indet (BVVal x) ind
  boxedval-not-indet (BVVal (VInr x)) (IInr ind) = boxedval-not-indet (BVVal x) ind
  boxedval-not-indet (BVInl bv) (IInl ind) = boxedval-not-indet bv ind
  boxedval-not-indet (BVInr bv) (IInr ind) = boxedval-not-indet bv ind
  boxedval-not-indet (BVSumCast x bv) (ICastSum x₁ ind) = boxedval-not-indet bv ind
  boxedval-not-indet (BVVal (VPair x x₂)) (IPair1 ind x₁) = boxedval-not-indet (BVVal x) ind
  boxedval-not-indet (BVVal (VPair x x₂)) (IPair2 x₁ ind) = boxedval-not-indet (BVVal x₂) ind
  boxedval-not-indet (BVPair bv bv₁) (IPair1 ind x) = boxedval-not-indet bv ind
  boxedval-not-indet (BVPair bv bv₁) (IPair2 x ind) = boxedval-not-indet bv₁ ind
  boxedval-not-indet (BVProdCast x bv) (ICastProd x₁ ind) = boxedval-not-indet bv ind

  -- boxed values don't step
  boxedval-not-step : ∀{d} → d boxedval → (Σ[ d' ∈ ihexp ] (d ↦ d')) → ⊥
  boxedval-not-step (BVVal VNum) (d' , Step FHOuter () x₃)
  boxedval-not-step (BVVal VLam) (d' , Step FHOuter () x₃)
  boxedval-not-step (BVArrCast x bv) (d0' , Step FHOuter (ITCastID) FHOuter) = x refl
  boxedval-not-step (BVArrCast x bv) (_ , Step (FHCast x₁) x₂ (FHCast x₃)) = boxedval-not-step bv (_ , Step x₁ x₂ x₃)
  boxedval-not-step (BVHoleCast () bv) (d' , Step FHOuter (ITCastID) FHOuter)
  boxedval-not-step (BVHoleCast x bv) (d' , Step FHOuter (ITCastSucceed ()) FHOuter)
  boxedval-not-step (BVHoleCast GArrHole bv) (_ , Step FHOuter (ITGround (MGArr x)) FHOuter) = x refl
  boxedval-not-step (BVHoleCast x bv) (_ , Step (FHCast x₁) x₂ (FHCast x₃)) = boxedval-not-step bv (_ , Step x₁ x₂ x₃)
  boxedval-not-step (BVHoleCast x x₁) (_ , Step FHOuter (ITExpand ()) FHOuter)
  boxedval-not-step (BVHoleCast x x₁) (_ , Step FHOuter (ITCastFail x₂ () x₄) FHOuter)
  boxedval-not-step (BVVal (VInl x)) (_ , Step FHOuter () x₃)
  boxedval-not-step (BVVal (VInr x)) (_ , Step FHOuter () x₃)
  boxedval-not-step (BVInl bv) (_ , Step FHOuter () x₂)
  boxedval-not-step (BVInr bv) (_ , Step FHOuter () x₂)
  boxedval-not-step (BVSumCast x bv) (_ , Step FHOuter ITCastID FHOuter) = x refl
  boxedval-not-step (BVSumCast x bv) (_ , Step (FHCast x₁) x₂ (FHCast x₃)) = boxedval-not-step bv (_ , Step x₁ x₂ x₃)
  boxedval-not-step (BVHoleCast GNum bv) (_ , Step FHOuter (ITGround ()) FHOuter)
  boxedval-not-step (BVHoleCast GSumHole bv) (_ , Step FHOuter (ITGround (MGSum x)) FHOuter) = x refl
  boxedval-not-step (BVVal (VInl x)) (_ , Step (FHInl x₁) x₂ (FHInl x₃)) = boxedval-not-step (BVVal x) (_ , Step x₁ x₂ x₃)
  boxedval-not-step (BVVal (VInr x)) (_ , Step (FHInr x₁) x₂ (FHInr x₃)) = boxedval-not-step (BVVal x) (_ , Step x₁ x₂ x₃)
  boxedval-not-step (BVInl bv) (_ , Step (FHInl x) x₁ (FHInl x₂)) = boxedval-not-step bv (_ , Step x x₁ x₂)
  boxedval-not-step (BVInr bv) (_ , Step (FHInr x) x₁ (FHInr x₂)) = boxedval-not-step bv (_ , Step x x₁ x₂)
  boxedval-not-step (BVVal (VPair x x₁)) (_ , Step (FHPair1 x₂) x₃ (FHPair1 x₄)) = boxedval-not-step (BVVal x) (_ , Step x₂ x₃ x₄)
  boxedval-not-step (BVVal (VPair x x₁)) (_ , Step (FHPair2 x₂) x₃ (FHPair2 x₄)) = boxedval-not-step (BVVal x₁) (_ , (Step x₂ x₃ x₄))
  boxedval-not-step (BVPair bv bv₁) (_ , Step (FHPair1 x) x₁ (FHPair1 x₂)) = boxedval-not-step bv (_ , Step x x₁ x₂)
  boxedval-not-step (BVPair bv bv₁) (_ , Step (FHPair2 x) x₁ (FHPair2 x₂)) = boxedval-not-step bv₁ (_ , Step x x₁ x₂)
  boxedval-not-step (BVProdCast x bv) (_ , Step FHOuter ITCastID FHOuter) = x refl
  boxedval-not-step (BVProdCast x bv) (_ , Step (FHCast x₁) x₂ (FHCast x₃)) = boxedval-not-step bv (_ , Step x₁ x₂ x₃)
  boxedval-not-step (BVHoleCast GProdHole bv) (_ , Step FHOuter (ITGround (MGProd x)) FHOut\er) = x refl

  mutual
    -- indeterminates don't step
    indet-not-step : ∀{d} → d indet → (Σ[ d' ∈ ihexp ] (d ↦ d')) → ⊥
    indet-not-step IEHole (d' , Step FHOuter () FHOuter)
    indet-not-step (INEHole x) (d' , Step FHOuter () FHOuter)
    indet-not-step (INEHole x) (_ , Step (FHNEHole x₁) x₂ (FHNEHole x₃)) = final-sub-not-trans x x₁ x₂
    indet-not-step (IAp x₁ () x₂) (_ , Step FHOuter (ITLam) FHOuter)
    indet-not-step (IAp x (ICastArr x₁ ind) x₂) (_ , Step FHOuter (ITApCast) FHOuter) = x _ _ _ _ _  refl
    indet-not-step (IAp x ind _) (_ , Step (FHAp1 x₂) x₃ (FHAp1 x₄)) = indet-not-step ind (_ , Step x₂ x₃ x₄)
    indet-not-step (IAp x ind f) (_ , Step (FHAp2 x₃) x₄ (FHAp2 x₆)) = final-not-step f (_ , Step x₃ x₄ x₆)
    indet-not-step (ICastArr x ind) (d0' , Step FHOuter (ITCastID) FHOuter) = x refl
    indet-not-step (ICastArr x ind) (_ , Step (FHCast x₁) x₂ (FHCast x₃)) = indet-not-step ind (_ , Step x₁ x₂ x₃)
    indet-not-step (ICastGroundHole () ind) (d' , Step FHOuter (ITCastID) FHOuter)
    indet-not-step (ICastGroundHole x ind) (d' , Step FHOuter (ITCastSucceed ()) FHOuter)
    indet-not-step (ICastGroundHole GArrHole ind) (_ , Step FHOuter (ITGround (MGArr x₁)) FHOuter) = x₁ refl
    indet-not-step (ICastGroundHole x ind) (_ , Step (FHCast x₁) x₂ (FHCast x₃)) = indet-not-step ind (_ , Step x₁ x₂ x₃)
    indet-not-step (ICastHoleGround x ind ()) (d' , Step FHOuter (ITCastID ) FHOuter)
    indet-not-step (ICastHoleGround x ind g) (d' , Step FHOuter (ITCastSucceed  x₂) FHOuter) = x _ _ refl
    indet-not-step (ICastHoleGround x ind GArrHole) (_ , Step FHOuter (ITExpand (MGArr x₂)) FHOuter) = x₂ refl
    indet-not-step (ICastHoleGround x ind g) (_ , Step (FHCast x₁) x₂ (FHCast x₃)) = indet-not-step ind (_ , Step x₁ x₂ x₃)
    indet-not-step (ICastGroundHole x x₁) (_ , Step FHOuter (ITExpand ()) FHOuter)
    indet-not-step (ICastHoleGround x x₁ x₂) (_ , Step FHOuter (ITGround ()) FHOuter)
    indet-not-step (ICastGroundHole x x₁) (_ , Step FHOuter (ITCastFail x₂ () x₄) FHOuter)
    indet-not-step (ICastHoleGround x x₁ x₂) (_ , Step FHOuter (ITCastFail x₃ x₄ x₅) FHOuter) = x _ _ refl
    indet-not-step (IFailedCast x x₁ x₂ x₃) (d' , Step FHOuter () FHOuter)
    indet-not-step (IFailedCast x x₁ x₂ x₃) (_ , Step (FHFailedCast x₄) x₅ (FHFailedCast x₆)) = final-not-step x (_ , Step x₄ x₅ x₆)
    indet-not-step (IPlus1 () x₄) (_ , Step FHOuter (ITPlus x₁) FHOuter)
    indet-not-step (IPlus1 x x₄) (_ , Step (FHPlus1 x₁) x₂ (FHPlus1 x₃)) = indet-not-step x (_ , Step x₁ x₂ x₃)
    indet-not-step (IPlus1 x x₄) (.(_ ·+ _) , Step (FHPlus2 x₁) x₂ (FHPlus2 x₃)) = final-not-step x₄ (_ , Step x₁ x₂ x₃)
    indet-not-step (IPlus2 x ()) (_ , Step FHOuter (ITPlus x₁) FHOuter)
    indet-not-step (IPlus2 x x₄) (_ , Step (FHPlus1 x₁) x₂ (FHPlus1 x₃)) = final-not-step x (_ , Step x₁ x₂ x₃)
    indet-not-step (IPlus2 x x₄) (_ , Step (FHPlus2 x₁) x₂ (FHPlus2 x₃)) = indet-not-step x₄ (_ , Step x₁ x₂ x₃)
    indet-not-step (IInl ind) (_ , Step FHOuter () x₂)
    indet-not-step (IInl ind) (_ , Step (FHInl x) x₁ (FHInl x₂)) = indet-not-step ind (_ , Step x x₁ x₂)
    indet-not-step (IInr ind) (_ , Step FHOuter () x₂)
    indet-not-step (IInr ind) (_ , Step (FHInr x) x₁ (FHInr x₂)) = indet-not-step ind (_ , Step x x₁ x₂)
    indet-not-step (ICase x x₁ x₂ ind) (_ , Step FHOuter ITCaseInl x₅) = x _ _ refl
    indet-not-step (ICase x x₁ x₂ ind) (_ , Step FHOuter ITCaseInr x₅) = x₁ _ _ refl
    indet-not-step (ICase x x₁ x₂ ind) (_ , Step FHOuter ITCaseCast x₅) = x₂ _ _ _ _ _ refl
    indet-not-step (ICase x x₁ x₂ ind) (_ , Step (FHCase x₃) x₄ (FHCase x₅)) = indet-not-step ind (_ , Step x₃ x₄ x₅)
    indet-not-step (ICastSum x ind) (_ , Step FHOuter ITCastID FHOuter) = x refl
    indet-not-step (ICastSum x ind) (_ , Step (FHCast x₁) x₂ (FHCast x₃)) = indet-not-step ind (_ , Step x₁ x₂ x₃)
    indet-not-step (ICastGroundHole GNum ind) (_ , Step FHOuter (ITGround ()) FHOuter)
    indet-not-step (ICastGroundHole GSumHole ind) (_ , Step FHOuter (ITGround (MGSum x)) FHOuter) = x refl
    indet-not-step (ICastHoleGround x ind GNum) (_ , Step FHOuter (ITExpand ()) FHOuter)
    indet-not-step (ICastHoleGround x ind GSumHole) (_ , Step FHOuter (ITExpand (MGSum x₁)) FHOuter) = x₁ refl
    indet-not-step (IPair1 ind x) (_ , Step (FHPair1 x₁) x₂ (FHPair1 x₃)) = indet-not-step ind (_ , Step x₁ x₂ x₃)
    indet-not-step (IPair1 ind x) (_ , Step (FHPair2 x₁) x₂ (FHPair2 x₃)) = final-not-step x (_ , Step x₁ x₂ x₃)
    indet-not-step (IPair2 x ind) (_ , Step (FHPair1 x₁) x₂ (FHPair1 x₃)) = final-not-step x (_ , Step x₁ x₂ x₃)
    indet-not-step (IPair2 x ind) (_ , Step (FHPair2 x₁) x₂ (FHPair2 x₃)) = indet-not-step ind (_ , Step x₁ x₂ x₃)
    indet-not-step (IFst x x₁ ind) (_ , Step FHOuter ITFstPair FHOuter) = x _ _ refl
    indet-not-step (IFst x x₁ ind) (_ , Step (FHFst x₂) x₃ (FHFst x₄)) = indet-not-step ind (_ , Step x₂ x₃ x₄)
    indet-not-step (ISnd x x₁ ind) (_ , Step FHOuter ITSndPair FHOuter) = x _ _ refl
    indet-not-step (ISnd x x₁ ind) (_ , Step (FHSnd x₂) x₃ (FHSnd x₄)) = indet-not-step ind (_ , Step x₂ x₃ x₄)
    indet-not-step (ICastGroundHole GProdHole ind) (_ , Step FHOuter (ITGround (MGProd x)) FHOuter) = x refl
    indet-not-step (ICastHoleGround x ind GProdHole) (_ , Step FHOuter (ITExpand (MGProd x₁)) FHOuter) = x₁ refl
    indet-not-step (IPair1 ind x) (_ , Step FHOuter () FHOuter)
    indet-not-step (IPair2 x ind) (_ , Step FHOuter () FHOuter)
    indet-not-step (IFst x x₁ ind) (_ , Step FHOuter ITFstCast FHOuter) = x₁ _ _ _ _ _ refl
    indet-not-step (ISnd x x₁ ind) (_ , Step FHOuter ITSndCast FHOuter) = x₁ _ _ _ _ _ refl
    indet-not-step (ICastProd x ind) (_ , Step FHOuter ITCastID FHOuter) = x refl
    indet-not-step (ICastProd x ind) (_ , Step (FHCast x₁) x₂ (FHCast x₃)) = indet-not-step ind (_ , Step x₁ x₂ x₃)

    -- final expressions don't step
    final-not-step : ∀{d} → d final → Σ[ d' ∈ ihexp ] (d ↦ d') → ⊥
    final-not-step (FBoxedVal x) stp = boxedval-not-step x stp
    final-not-step (FIndet x) stp = indet-not-step x stp

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module Metalogic.Constructive.Provability where

open import Sets.BoolSet
open import Functional
import      Lvl
open import Type

  -- Structural rules
record Structural {ℓ ℓₘ} {Formula : Type{ℓ}} (_⊢_ : BoolSet(Formula) → Formula → Type{ℓₘ}) : Type{ℓₘ Lvl.⊔ ℓ} where
  field
    assumption : ∀{Γ}{φ} → (φ ∈ Γ) → (Γ ⊢ φ)

module Propositional {ℓ ℓₘ} {Formula : Type{ℓ}} (_⊢_ : BoolSet(Formula) → Formula → Type{ℓₘ}) where
  -- Rules of bottom
  record Bottom : Type{ℓₘ Lvl.⊔ ℓ} where
    field
      ⊥    : Formula

    field
      intro : ∀{Γ}{φ} → (Γ ⊢ φ) → ((Γ ∪ singleton(φ)) ⊢ ⊥) → (Γ ⊢ ⊥)
      elim  : ∀{Γ}{φ} → (⊥ ∈ Γ) → (Γ ⊢ φ)

  -- Rules of top
  record Top : Type{ℓₘ Lvl.⊔ ℓ} where
    field
      ⊤    : Formula

    field
      intro : ∀{Γ} → (Γ ⊢ ⊤)

  -- Rules of conjunction
  record Conjunction : Type{ℓₘ Lvl.⊔ ℓ} where
    infixl 1005 _∧_

    field
      _∧_  : Formula → Formula → Formula

    field
      intro : ∀{Γ}{φ₁ φ₂} → (Γ ⊢ φ₁) → (Γ ⊢ φ₂) → (Γ ⊢ (φ₁ ∧ φ₂))
      elimₗ  : ∀{Γ}{φ₁ φ₂} → (Γ ⊢ (φ₁ ∧ φ₂)) → (Γ ⊢ φ₁)
      elimᵣ  : ∀{Γ}{φ₁ φ₂} → (Γ ⊢ (φ₁ ∧ φ₂)) → (Γ ⊢ φ₂)

  -- Rules of implication
  record Implication : Type{ℓₘ Lvl.⊔ ℓ} where
    infixl 1000 _⟶_

    field
      _⟶_ : Formula → Formula → Formula

    field
      intro : ∀{Γ}{φ₁ φ₂} → ((Γ ∪ singleton(φ₁)) ⊢ φ₂) → (Γ ⊢ (φ₁ ⟶ φ₂))
      elim  : ∀{Γ}{φ₁ φ₂} → (Γ ⊢ (φ₁ ⟶ φ₂)) → (Γ ⊢ φ₁) → (Γ ⊢ φ₂)

  -- Rules of reversed implication
  record Consequence : Type{ℓₘ Lvl.⊔ ℓ} where
    infixl 1000 _⟵_

    field
      _⟵_ : Formula → Formula → Formula

    field
      intro : ∀{Γ}{φ₁ φ₂} → ((Γ ∪ singleton(φ₁)) ⊢ φ₂) → (Γ ⊢ (φ₂ ⟵ φ₁))
      elim  : ∀{Γ}{φ₁ φ₂} → (Γ ⊢ (φ₂ ⟵ φ₁)) → (Γ ⊢ φ₁) → (Γ ⊢ φ₂)

  -- Rules of equivalence
  record Equivalence : Type{ℓₘ Lvl.⊔ ℓ} where
    infixl 1000 _⟷_

    field
      _⟷_ : Formula → Formula → Formula

    field
      intro : ∀{Γ}{φ₁ φ₂} → ((Γ ∪ singleton(φ₂)) ⊢ φ₁) → ((Γ ∪ singleton(φ₁)) ⊢ φ₂) → (Γ ⊢ (φ₁ ⟷ φ₂))
      elimₗ  : ∀{Γ}{φ₁ φ₂} → (Γ ⊢ (φ₁ ⟷ φ₂)) → (Γ ⊢ φ₂) → (Γ ⊢ φ₁)
      elimᵣ  : ∀{Γ}{φ₁ φ₂} → (Γ ⊢ (φ₁ ⟷ φ₂)) → (Γ ⊢ φ₁) → (Γ ⊢ φ₂)

  -- Rules of disjunction
  record Disjunction : Type{ℓₘ Lvl.⊔ ℓ} where
    infixl 1004 _∨_

    field
      _∨_  : Formula → Formula → Formula

    field
      introₗ : ∀{Γ}{φ₁ φ₂} → (Γ ⊢ φ₁) → (Γ ⊢ (φ₁ ∨ φ₂))
      introᵣ : ∀{Γ}{φ₁ φ₂} → (Γ ⊢ φ₂) → (Γ ⊢ (φ₁ ∨ φ₂))
      elim  : ∀{Γ}{φ₁ φ₂ φ₃} → (Γ ⊢ (φ₁ ∨ φ₂)) → ((Γ ∪ singleton(φ₁)) ⊢ φ₃) → ((Γ ∪ singleton(φ₂)) ⊢ φ₃) → (Γ ⊢ φ₃)

  -- Rules of negation
  record Negation ⦃ _ : Bottom ⦄ : Type{ℓₘ Lvl.⊔ ℓ} where
    open Bottom ⦃ ... ⦄

    infixl 1010 ¬_

    field
      ¬_   : Formula → Formula

    field
      intro : ∀{Γ}{φ} → ((Γ ∪ singleton(φ)) ⊢ ⊥) → (Γ ⊢ (¬ φ))
      elim  : ∀{Γ}{φ} → (Γ ⊢ (¬ φ)) → (Γ ⊢ φ) → (Γ ⊢ ⊥)

  -- A theory of constructive propositional logic expressed using natural deduction rules
  record Theory : Type{ℓₘ Lvl.⊔ ℓ} where
    open Structural  ⦃ ... ⦄ public
    open Conjunction ⦃ ... ⦄ renaming (intro to [∧]-intro ; elimₗ to [∧]-elimₗ ; elimᵣ to [∧]-elimᵣ) public
    open Disjunction ⦃ ... ⦄ renaming (introₗ to [∨]-introₗ ; introᵣ to [∨]-introᵣ ; elim to [∨]-elim) public
    open Implication ⦃ ... ⦄ renaming (intro to [→]-intro ; elim to [→]-elim) public
    open Consequence ⦃ ... ⦄ renaming (intro to [←]-intro ; elim to [←]-elim) public
    open Equivalence ⦃ ... ⦄ renaming (intro to [↔]-intro ; elimₗ to [↔]-elimₗ ; elimᵣ to [↔]-elimᵣ) public
    open Negation    ⦃ ... ⦄ renaming (intro to [¬]-intro ; elim to [¬]-elim) public
    open Bottom      ⦃ ... ⦄ renaming (intro to [⊥]-intro ; elim to [⊥]-elim) public
    open Top         ⦃ ... ⦄ renaming (intro to [⊤]-intro) public

    field
      ⦃ bottom ⦄      : Bottom
      ⦃ top ⦄         : Top
      ⦃ conjunction ⦄ : Conjunction
      ⦃ disjunction ⦄ : Disjunction
      ⦃ implication ⦄ : Implication
      ⦃ consequence ⦄ : Consequence
      ⦃ equivalence ⦄ : Equivalence
      ⦃ negation ⦄    : Negation

module Predicate {ℓₘₗₛ ℓₘₒₛ ℓₘₗ ℓₘₒ} {Formula : Type{ℓₘₗₛ Lvl.⊔ ℓₘₒₛ}} {Domain : Type{ℓₘₒₛ}} (Proof : Formula → Type{ℓₘₗ Lvl.⊔ ℓₘₒ}) (Construct : Domain → Type{ℓₘₒ}) where
  open Propositional(Proof) renaming (Theory to PropositionalTheory)

  record UniversalQuantification : Type{(ℓₘₗ Lvl.⊔ ℓₘₒ) Lvl.⊔ (ℓₘₗₛ Lvl.⊔ ℓₘₒₛ)} where
    field
      ∀ₗ : (Domain → Formula) → Formula

    field
      intro : ∀{P : Domain → Formula} → (∀{x : Domain} → Proof(P(x))) → Proof(∀ₗ P)
      elim  : ∀{P : Domain → Formula} → Proof(∀ₗ P) → (∀{x : Domain} → Proof(P(x)))

  record ExistentialQuantification : Type{(ℓₘₗ Lvl.⊔ ℓₘₒ) Lvl.⊔ (ℓₘₗₛ Lvl.⊔ ℓₘₒₛ)} where
    field
      ∃ₗ : (Domain → Formula) → Formula

    field
      intro : ∀{P : Domain → Formula}{a} → Proof(P(a)) → Proof(∃ₗ P)
      elim  : ∀{P : Domain → Formula}{Z : Formula} → (∀{x : Domain} → Proof(P(x)) → Proof(Z)) → Proof(∃ₗ P) → Proof(Z)

  -- A theory of constructive predicate/(first-order) logic expressed using natural deduction rules
  record Theory  : Type{(ℓₘₗ Lvl.⊔ ℓₘₒ) Lvl.⊔ (ℓₘₗₛ Lvl.⊔ ℓₘₒₛ)} where
    open Propositional.Theory      ⦃ ... ⦄ public
    open UniversalQuantification   ⦃ ... ⦄ renaming (intro to [∀]-intro ; elim to [∀]-elim) public
    open ExistentialQuantification ⦃ ... ⦄ renaming (intro to [∃]-intro ; elim to [∃]-elim) public

    field
      ⦃ propositional ⦄             : PropositionalTheory
      ⦃ universalQuantification ⦄   : UniversalQuantification
      ⦃ existentialQuantification ⦄ : ExistentialQuantification

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:
module Function.Iteration.Order where

open import Data
open import Data.Boolean.Stmt
open import Functional renaming (id to id-fn)
open import Function.Iteration hiding (_^_)
open import Function.Iteration.Proofs
open import Logic
open import Logic.IntroInstances
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Logic.Predicate
import      Lvl
open import Numeral.Natural
open import Numeral.Natural.Oper hiding (_^_)
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.DivMod.Proofs
open import Numeral.Natural.Oper.FlooredDivision
open import Numeral.Natural.Oper.Modulo
open import Numeral.Natural.Oper.Modulo.Proofs
open import Numeral.Natural.Relation.Divisibility
open import Numeral.Natural.Relation.Divisibility.Proofs
open import Numeral.Natural.Relation.Order.Decidable
open import Numeral.Natural.Relation.Order.Proofs
open import Numeral.Natural.Relation.Order
open import Relator.Equals using () renaming (_≡_ to _≡ₑ_ ; _≢_ to _≢ₑ_ ; [≡]-intro to [≡ₑ]-intro)
open import Structure.Setoid
open import Structure.Function.Domain
open import Structure.Function
open import Structure.Operator.Properties
open import Structure.Operator.Proofs
open import Structure.Operator
open import Structure.Relator.Properties
open import Structure.Relator.Ordering
open import Structure.Relator.Ordering.Lattice
open import Syntax.Transitivity
open import Type
open import Type.Properties.Decidable.Proofs
open import Type.Properties.Empty
open import Type.Size.Finite

private variable ℓ ℓₑ : Lvl.Level
private variable T : Type{ℓ}

module _ ⦃ equiv-T : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) ⦃ op : BinaryOperator(_▫_) ⦄ {id} ⦃ ident : Identity(_▫_)(id) ⦄ ⦃ assoc : Associativity(_▫_) ⦄ where
  -- Operator alias for iterated application of an operator with an element.
  _^_ : T → ℕ → T
  x ^ n = Function.Iteration.repeatₗ(n)(_▫_)(id)(x)

  -- `FiniteOrder(x)(n)` means that the element `x` is of order `n`.
  -- It is finite in the sense that it is a number and not infinite.
  -- An element's order is the smallest positive integer power of x such that the result is the identity element.
  data FiniteOrder (x : T) : ℕ → Stmt{ℓₑ} where
    intro : ∀{n} → LE.Minimum(_≤_)(n ↦ x ^ 𝐒(n) ≡ id)(n) → FiniteOrder(x)(𝐒(n))

  -- `Ord(x)` means that the element `x` has a finite order.
  Ord : T → Stmt
  Ord(x) = ∃(FiniteOrder(x))

  -- `ord(x)` is the order of x (when it is finite).
  ord : (x : T) → ⦃ _ : Ord(x) ⦄ → ℕ
  ord(_) ⦃ [∃]-intro n ⦄ = n

  module _ {x : T} where
    -- An order is never 0 by definition.
    finite-order-0 : ¬ FiniteOrder(x)(𝟎)
    finite-order-0 ()

    -- An element power its order is the identity element.
    [^]-by-ord : ⦃ p : Ord(x) ⦄ → (x ^ ord(x) ⦃ p ⦄ ≡ id)
    [^]-by-ord ⦃ [∃]-intro (𝐒(_)) ⦃ intro p ⦄ ⦄ = LE.Minimum.membership{_≤_ = _≤_}(p)

    -- When an element power something is the identity element, then the power is either zero or greater/equal its order.
    ord-is-minimum : ⦃ p : Ord(x) ⦄ → ∀{n} → (x ^ n ≡ id) → (n ≡ₑ 𝟎) ∨ (ord(x) ⦃ p ⦄ ≤ n)
    ord-is-minimum ⦃ [∃]-intro (_)     ⦃ intro p ⦄ ⦄      {𝟎}   x0id  = [∨]-introₗ [≡ₑ]-intro
    ord-is-minimum ⦃ [∃]-intro .(𝐒 po) ⦃ intro {po} p ⦄ ⦄ {𝐒 n} xsnid = [∨]-introᵣ ([≤]-with-[𝐒] ⦃ LE.Minimum.proof{_≤_ = _≤_}(p) ⦃ xsnid ⦄ ⦄)

    -- When an element power something less than its order and it is the identity element, then the power is 0.
    ord-is-minimum-but-0 : ⦃ p : Ord(x) ⦄ → ∀{n} → (x ^ n ≡ id) → (n < ord(x) ⦃ p ⦄) → (n ≡ₑ 𝟎)
    ord-is-minimum-but-0 ⦃ p ⦄ {𝟎}    _    _    = [≡ₑ]-intro
    ord-is-minimum-but-0 ⦃ p ⦄ {𝐒(n)} xnid nord with ord-is-minimum ⦃ p ⦄ {𝐒(n)} xnid
    ... | [∨]-introᵣ ordsn = [⊥]-elim([<]-to-[≱] nord (ordsn))

    -- An order is never 0.
    ord-non-zero : ⦃ p : Ord(x) ⦄ → (ord(x) ⦃ p ⦄ ≢ₑ 𝟎)
    ord-non-zero ⦃ [∃]-intro 𝟎 ⦃ ⦄ ⦄ [≡ₑ]-intro

    -- Iteration (_^_) distributes to the right.
    -- Can also be seen as iteration preserving from addition to the operation.
    [^]-by-add : ∀{a b} → ((x ^ a) ▫ (x ^ b) ≡ x ^ (a + b))
    [^]-by-add {a}{b} = repeatₗ-by-sum {X = T}{_▫_}{x}{id}{a}{b}

    -- Nested iterations can join to be a product.
    [^]-by-product : ∀{a b} → ((((x ^ a)) ^ b) ≡ x ^ (a ⋅ b))
    [^]-by-product {a}{b} = repeatₗ-by-product {X = T}{_▫_}{x}{id}{a}{b}

    -- When powering a difference yields the identity element, the powered elements are the same.
    [^]-by-distanceₗ : ∀{a b} → (x ^ a ≡ x ^ b) ← (x ^ (a 𝄩 b) ≡ id)
    [^]-by-distanceₗ {a}{b} = repeatₗ-by-distanceₗ {X = T}{_▫_}{x}{id}{a}{b}

    -- Theorems where `n` is a power which yields an identity element.
    module _ {n} (n-id : (x ^ n ≡ id)) where
      -- Adding something to `n` is only leaving the something behind.
      [^]-by-id-add : ∀{a} → (x ^ (n + a)  ≡ x ^ a)
      [^]-by-id-add {a} =
        x ^ (n + a)       🝖-[ symmetry(_≡_) ([^]-by-add {n}{a}) ]
        (x ^ n) ▫ (x ^ a) 🝖-[ congruence₂ₗ(_▫_)(_) n-id ]
        id ▫ (x ^ a)      🝖-[ identityₗ(_▫_)(id) ]
        x ^ a             🝖-end

      -- Multiplying something by `n` is still the identity element.
      [^]-by-id-multiple : ∀{a} → (x ^ (n ⋅ a) ≡ id)
      [^]-by-id-multiple {𝟎}    = repeatₗ-by-0 {X = T}{_▫_}{x}{id}
      [^]-by-id-multiple {𝐒(a)} =
        x ^ (n + (n ⋅ a))       🝖-[ symmetry(_≡_) ([^]-by-add {n}{n ⋅ a}) ]
        (x ^ n) ▫ (x ^ (n ⋅ a)) 🝖-[ congruence₂(_▫_) n-id ([^]-by-id-multiple {a}) ]
        id ▫ id                 🝖-[ identityₗ(_▫_)(id) ]
        id                      🝖-end

    -- A power yields an identity element only when it is a multiple of the order of the element.
    [^]-id-when-div : ⦃ p : Ord(x) ⦄ → ∀{n} → (x ^ n ≡ id) ↔ (ord(x) ⦃ p ⦄ ∣ n)
    [^]-id-when-div ⦃ p ⦄ {n} = [↔]-intro (l{n}) (r{n}) where
      l : ∀{n} → (x ^ n ≡ id) ← (ord(x) ⦃ p ⦄ ∣ n)
      l {.0}                  Div𝟎 = repeatₗ-by-0 {X = T}{_▫_}{x}{id}
      l {.(ord(x) ⦃ p ⦄ + n)} (Div𝐒 {_}{n} div) =
        x ^ (ord x ⦃ p ⦄ + n)       🝖-[ symmetry(_≡_) ([^]-by-add {ord(x) ⦃ p ⦄}{n}) ]
        (x ^ ord x ⦃ p ⦄) ▫ (x ^ n) 🝖-[ congruence₂(_▫_) ([^]-by-ord ⦃ p ⦄) (l{n} div) ]
        id ▫ id                     🝖-[ identityₗ(_▫_)(id) ]
        id                          🝖-end

      r : ∀{n} → (x ^ n ≡ id) → (ord(x) ⦃ p ⦄ ∣ n)
      r {𝟎}    _    = Div𝟎
      r {𝐒(n)} xnid = [↔]-to-[→] mod-divisibility mod-is-0 where
        open import Relator.Equals.Proofs.Equiv using ([≡]-to-equivalence)

        instance
          ord-non-zero-comp : IsTrue(ord(x) ⦃ p ⦄ ≢? 𝟎)
          ord-non-zero-comp = [↔]-to-[→] decider-true (ord-non-zero ⦃ p ⦄)

        instance
          ord-positive : IsTrue(positive?(ord(x) ⦃ p ⦄))
          ord-positive with ord(x) ⦃ p ⦄ | [∃]-proof p
          ... | 𝟎   | pp = finite-order-0 pp
          ... | 𝐒 _ | _  = <>

        instance
          ord-n-ineq : ord(x) ⦃ p ⦄ ≤ 𝐒(n)
          ord-n-ineq with ord-is-minimum ⦃ p ⦄ {𝐒(n)} xnid
          ord-n-ineq | [∨]-introₗ ()
          ord-n-ineq | [∨]-introᵣ proof      = proof

        mod-is-id : x ^ (𝐒(n) mod ord(x) ⦃ p ⦄) ≡ id
        mod-is-id =
          x ^ (𝐒(n) mod ord(x) ⦃ p ⦄)                                                      🝖-[ symmetry(_≡_) (identityₗ(_▫_)(id)) ]
          id ▫ (x ^ (𝐒(n) mod ord(x) ⦃ p ⦄))                                               🝖-[ congruence₂ₗ(_▫_)(_) (symmetry(_≡_) ([^]-by-id-multiple {ord(x) ⦃ p ⦄} ([^]-by-ord ⦃ p ⦄) {𝐒(n) ⌊/⌋ ord(x) ⦃ p ⦄})) ]
          (x ^ ((ord(x) ⦃ p ⦄) ⋅ (𝐒(n) ⌊/⌋ ord(x) ⦃ p ⦄))) ▫ (x ^ (𝐒(n) mod ord(x) ⦃ p ⦄)) 🝖-[ [^]-by-add {(ord(x) ⦃ p ⦄) ⋅ (𝐒(n) ⌊/⌋ ord(x) ⦃ p ⦄)} {𝐒(n) mod ord(x) ⦃ p ⦄} ]
          x ^ (((ord(x) ⦃ p ⦄) ⋅ (𝐒(n) ⌊/⌋ ord(x) ⦃ p ⦄)) + (𝐒(n) mod ord(x) ⦃ p ⦄))       🝖-[ congruence₁(x ^_) ⦃ Relator.Equals.Proofs.Equiv.[≡]-to-function ⦄ ([≡]-to-equivalence([⌊/⌋][mod]-is-division-with-remainder-pred-commuted{𝐒(n)}{ord(x) ⦃ p ⦄})) ]
          x ^ 𝐒(n)                                                                         🝖-[ xnid ]
          id                                                                               🝖-end

        mod-is-0 : 𝐒(n) mod ord(x) ⦃ p ⦄ ≡ 𝟎
        mod-is-0 = ord-is-minimum-but-0 ⦃ p ⦄ mod-is-id mod-maxᵣ

    module _ {inv} ⦃ _ : InverseFunctionᵣ(_▫_)(inv) ⦄ where
      [^]-by-distanceᵣ : ∀{a b} → (x ^ a ≡ x ^ b) → (x ^ (a 𝄩 b) ≡ id)
      [^]-by-distanceᵣ {a}{b} = repeatₗ-by-distanceᵣ{X = T}{_▫_}{x}{id} ⦃ cancᵣ = One.cancellationᵣ-by-associativity-inverse ⦄ {a}{b}

      [^]-equal-[𝄩] : ⦃ p : Ord(x) ⦄ → ∀{a b} → (x ^ a ≡ x ^ b) ↔ (ord(x) ⦃ p ⦄ ∣ (a 𝄩 b))
      [^]-equal-[𝄩] ⦃ p ⦄ {a}{b} = [↔]-transitivity ([↔]-intro ([^]-by-distanceₗ{a}{b}) ([^]-by-distanceᵣ{a}{b})) ([^]-id-when-div ⦃ p ⦄)

      postulate [^]-cancellationₗ : ⦃ p : Ord(x) ⦄ → ∀{a b} → ⦃ a < ord(x) ⦃ p ⦄ ⦄ → ⦃ b < ord(x) ⦃ p ⦄ ⦄ → (x ^ a ≡ x ^ b) → (a ≡ₑ b)

  -- ord(x ^ n) ≡ ord(x) / gcd(n)(ord(x))
  -- (x ▫ y ≡ y ▫ x) → ord(x ▫ y) ∣ lcm(ord(x))(ord(y))
  -- (∀{x} → (ord(x) ≡ 2)) → Commutativity(_▫_)

  -- One element in the group can "generate" any element element in the group by repeated application of the operator.
  Generator : T → Stmt
  Generator(x) = Surjective(x ^_)

  -- A group is cyclic when there is an element that can generate it.
  Cyclic : Stmt
  Cyclic = ∃(Generator)

  {- TODO: Because the thing exists, there is finitely many. Search for the first one
  finite-order-from-dec-existence : ⦃ Decidable(_≡_) ⦄ → ∀{a} → ∃(n ↦ (a ^ 𝐒(n) ≡ id)) → Ord(a)
  finite-order-from-dec-existence {n} asnid = {!!}
  -- intro (Weak.Properties.intro ⦃ asnid ⦄ {!!})

  -- TODO: Assume decidable equality and use finite-order-from-dec-existence above. Existence should follow from finiteness
  finite-have-order : ⦃ Finite(T) ⦄ → ∀{a} → Ord(a)
  ∃.witness (finite-have-order ⦃ [∃]-intro size ⦃ fin-bij ⦄ ⦄) = size
  ∃.proof (finite-have-order ⦃ [∃]-intro 𝟎 ⦃ [∃]-intro fin-bij ⦄ ⦄ {a = a}) with fin-bij a
  ... | ()
  ∃.proof (finite-have-order ⦃ [∃]-intro (𝐒(size)) ⦃ fin-bij ⦄ ⦄) = intro {!!}
  -}

  postulate cyclic-commutative : ⦃ Cyclic ⦄ → Commutativity(_▫_)
  -- generator-order-size : ⦃ Finite(T) ⦄ → ∀{a} → ⦃ p : Ord(a) ⦄ → Generator(a) ↔ ((# T) ≡ₑ ord(a) ⦃ p ⦄)
  -- cyclic-order-size : ⦃ Finite(T) ⦄ → ⦃ Cyclic ⦄ ↔ ∃(a ↦ (# T) ≡ₑ ord(a))

  -- generator-of-power : Generator(a ^ k) ↔ Generator(a ^ gcd(ord(a))(k))
  -- order-of-power : ord(a ^ k) ∣ ord(a) / gcd(ord(a),k)

{-
  module _ {id} ⦃ ident : Identity(_▫_)(id) ⦄ where
    open import Data.Boolean
    open import Data.Boolean.Stmt
    import      Function.Iteration
    open import Logic.Computability
    open import Logic.Computability.Binary renaming (ComputablyDecidable to ComputablyDecidable2)
    open import Logic

    open import Numeral.Natural.Relation.Computability

-}
    {-
    boundedMinOr : ℕ → (ℕ → Bool) → ℕ → ℕ
    boundedMinOr 𝟎          p default = default
    boundedMinOr (𝐒(bound)) p default = if p(bound) then bound else (boundedMinOr bound p default)

    boundedMinOr-proof : ∀{p : ℕ → Bool}{bound default : ℕ} → IsTrue(p(default)) → IsTrue(p(boundedMinOr bound p default))

    min-by-bruteforce : ∀{ℓ}{P : ℕ → Stmt{ℓ}} → ⦃ comp : ComputablyDecidable(P) ⦄ → ⦃ e : ∃(P) ⦄ → ∃(Weak.Properties.MinimumOf(_≤_)(P))
    ∃.witness (min-by-bruteforce {P = P} ⦃ comp ⦄ ⦃ e ⦄) = boundedMinOr([∃]-witness(e)) (ComputablyDecidable.decide(comp)) ([∃]-witness(e))
    Weak.Properties.MinimumOf.proof (∃.proof min-by-bruteforce) {x} ⦃ x₁ ⦄ = {!!}

    ord : (x : T) → ⦃ e : FiniteOrder(x) ⦄ → ⦃ comp : ComputablyDecidable2{X = T}(_≡_) ⦄ → ℕ
    ord(x) ⦃ e ⦄ ⦃ comp ⦄ = Weak.minOf(_≤_)(n ↦ x ^ 𝐒(n) ≡ id) ⦃ min-by-bruteforce ⦃ {!!} ⦄ ⦃ e ⦄ ⦄
    -}


text:
module Issue2487-4 where

open import Agda.Primitive -- this should not be consistency-checked

open import Agda.Builtin.Bool

f : Bool → Bool
f true = true
f _    = false

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --safe --postfix-projections #-}

module Relation.Nullary.Decidable.Logic where

open import Prelude
open import Data.Sum

infixl 7 _&&_
_&&_ : Dec A → Dec B → Dec (A × B)
(x && y) .does = x .does and y .does
(yes x && yes y) .why  = ofʸ (x , y)
(yes x && no  y) .why  = ofⁿ (y ∘ snd)
(no  x && y) .why  = ofⁿ (x ∘ fst)

infixl 6 _||_
_||_ : Dec A → Dec B → Dec (A ⊎ B)
(x || y) .does = x .does or y .does
(yes x || y) .why = ofʸ (inl x)
(no  x || yes y) .why = ofʸ (inr y)
(no  x || no  y) .why = ofⁿ (either x y)

! : Dec A → Dec (¬ A)
! x .does = not (x .does)
! (yes x) .why = ofⁿ (λ z → z x)
! (no  x) .why = ofʸ x

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
{-# OPTIONS --cubical --safe --postfix-projections #-}

module Data.Bool.Properties where

open import HLevels
open import Path
open import Data.Bool.Base
open import Data.Bool.Truth
open import Data.Unit.Properties
open import Data.Unit
open import Data.Empty
open import Data.Empty.Properties using (isProp⊥)
open import Relation.Nullary.Discrete
open import Relation.Nullary.Decidable using (Dec; does; why)

isPropT : ∀ x → isProp (T x)
isPropT false = isProp⊥
isPropT true  = isProp⊤

false≢true : false ≢ true
false≢true p = subst (bool ⊤ ⊥) p tt

true≢false : true ≢ false
true≢false p = subst (bool ⊥ ⊤) p tt

discreteBool : Discrete Bool
discreteBool false y .does = not y
discreteBool true y .does = y
discreteBool false false .why = refl
discreteBool false true .why = false≢true
discreteBool true false .why = true≢false
discreteBool true true .why = refl

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

--open import HoTT
open import homotopy.3x3.PushoutPushout
open import homotopy.3x3.Transpose
open import homotopy.3x3.Common

module homotopy.3x3.From {i} (d : Span^2 {i}) where

open Span^2 d
open M d hiding (Pushout^2)
open M (transpose d) using () renaming (A₀∙ to A∙₀; A₂∙ to A∙₂; A₄∙ to A∙₄;
                                        module F₁∙ to F∙₁; f₁∙ to f∙₁;
                                        module F₃∙ to F∙₃; f₃∙ to f∙₃;
                                        v-h-span to h-v-span)
open M using (Pushout^2)

module I∙₀ = PushoutRec {D = Pushout^2 d}
                        (left ∘ left) (right ∘ left) (glue ∘ left)

i∙₀ : A∙₀ → Pushout^2 d
i∙₀ = I∙₀.f

module I∙₄ = PushoutRec {D = Pushout^2 d}
                        (left ∘ right) (right ∘ right) (glue ∘ right)

i∙₄ : A∙₄ → Pushout^2 d
i∙₄ = I∙₄.f

module E∙₂Red (c : A₂₂) where

  lhs-o : _
  lhs-o =
      ap (i∙₄ ∘ f∙₃) (glue c)
         =⟨ ap-∘ i∙₄ f∙₃ (glue c) ⟩
      ap i∙₄ (ap f∙₃ (glue c))
           =⟨ F∙₃.glue-β c |in-ctx (ap i∙₄) ⟩
      ap i∙₄ (ap left (H₁₃ c) ∙ glue (f₂₃ c) ∙ ap right (! (H₃₃ c)))
           =⟨ ap-∙∙!`∘`∘ i∙₄ left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c) ⟩
      ap (left ∘ right) (H₁₃ c) ∙ ap i∙₄ (glue (f₂₃ c)) ∙ ! (ap (right ∘ right) (H₃₃ c))
           =⟨ I∙₄.glue-β (f₂₃ c) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))) ⟩
      ap (left ∘ right) (H₁₃ c) ∙ glue (right (f₂₃ c)) ∙ ! (ap (right ∘ right) (H₃₃ c)) ∎

  rhs-o : _
  rhs-o =
      ! (ap (left ∘ left) (H₁₁ c)) ∙ glue (left (f₂₁ c)) ∙ ap (right ∘ left) (H₃₁ c)
           =⟨ ! (I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → (! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c))) ⟩
      ! (ap (left ∘ left) (H₁₁ c)) ∙ ap i∙₀ (glue (f₂₁ c)) ∙ ap (right ∘ left) (H₃₁ c)
           =⟨ ! (ap-!∙∙`∘`∘ i∙₀ left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c)) ⟩
      ap i∙₀ (ap left (! (H₁₁ c)) ∙ glue (f₂₁ c) ∙ ap right (H₃₁ c))
           =⟨ ! (F∙₁.glue-β c) |in-ctx (λ u → ap i∙₀ u) ⟩
      ap i∙₀ (ap f∙₁ (glue c))
           =⟨ ∘-ap i∙₀ f∙₁ (glue c) ⟩
      ap (i∙₀ ∘ f∙₁) (glue c) ∎

  T-lhs : Type _
  T-lhs = right (left (f₃₀ (f₂₁ c))) == right (right (f₃₄ (f₂₃ c))) :> Pushout^2 d

  lhs-i : _ == _ :> T-lhs
  lhs-i =
      ap (right ∘ left) (H₃₁ c) ∙ ap right (glue (f₃₂ c)) ∙ ap (right ∘ right) (H₃₃ c)
        =⟨ ! (ap-∙∙`∘`∘ right left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c)) ⟩
      ap right (ap left (H₃₁ c) ∙ glue (f₃₂ c) ∙ ap right (H₃₃ c))
        =⟨ ! (ap (ap right) (F₃∙.glue-β c)) ⟩
      ap right (ap f₃∙ (glue c))
        =⟨ ∘-ap right f₃∙ (glue c) ⟩
      ap (right ∘ f₃∙) (glue c) ∎

  T-rhs : Type _
  T-rhs = left (left (f₁₀ (f₂₁ c))) == left (right (f₁₄ (f₂₃ c))) :> Pushout^2 d

  rhs-i : _ == _ :> T-rhs
  rhs-i =
      ap (left ∘ f₁∙) (glue c)
        =⟨ ap-∘ left f₁∙ (glue c) ⟩
      ap left (ap f₁∙ (glue c))
        =⟨ F₁∙.glue-β c |in-ctx (ap left) ⟩
      ap left (ap left (H₁₁ c) ∙ glue (f₁₂ c) ∙ ap right (H₁₃ c))
        =⟨ ap-∙∙`∘`∘ left left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c) ⟩
      (ap (left ∘ left) (H₁₁ c) ∙ ap left (glue (f₁₂ c)) ∙ ap (left ∘ right) (H₁₃ c)) ∎

  coh! : (p : (_ , _ =□ _ , _)) → _
  coh! = pp-coh! {A = Pushout^2 d}
               {u = glue (left (f₂₁ c))}
               {ap (right ∘ left) (H₃₁ c)}
               {ap right (glue (f₃₂ c))}
               {ap (right ∘ right) (H₃₃ c)}
               {ap (left ∘ left) (H₁₁ c)}
               {ap left (glue (f₁₂ c))}
               {ap (left ∘ right) (H₁₃ c)}
               {glue (right (f₂₃ c))}

  coh : (p : (_ , _ =□ _ , _)) → _
  coh = pp-coh {A = Pushout^2 d}
               {p = ap left (glue (f₁₂ c))}
               {ap (left ∘ right) (H₁₃ c)}
               {glue (right (f₂₃ c))}
               {ap (right ∘ right) (H₃₃ c)}
               {ap (left ∘ left) (H₁₁ c)}
               {glue (left (f₂₁ c))}
               {ap (right ∘ left) (H₃₁ c)}
               {ap right (glue (f₃₂ c))}

  module _ (to : Pushout^2 d → Pushout^2 (transpose d)) where

    ap-ap-coh! : (p : _ , _ =□ _ , _) → _
    ap-ap-coh! = pp-coh!  {u = ap to (glue (left (f₂₁ c)))}
                          {ap (to ∘ right ∘ left) (H₃₁ c)}
                          {ap to (ap right (glue (f₃₂ c)))}
                          {ap (to ∘ right ∘ right) (H₃₃ c)}
                          {ap (to ∘ left ∘ left) (H₁₁ c)}
                          {ap to (ap left (glue (f₁₂ c)))}
                          {ap (to ∘ left ∘ right) (H₁₃ c)}
                          {ap to (glue (right (f₂₃ c)))}

    ap-ap-coh : (p : _ , _ =□ _ , _) → _
    ap-ap-coh = pp-coh {p = ap to (ap left (glue (f₁₂ c)))}
                       {ap (to ∘ left ∘ right) (H₁₃ c)}
                       {ap to (glue (right (f₂₃ c)))}
                       {ap (to ∘ right ∘ right) (H₃₃ c)}
                       {ap (to ∘ left ∘ left) (H₁₁ c)}
                       {ap to (glue (left (f₂₁ c)))}
                       {ap (to ∘ right ∘ left) (H₃₁ c)}
                       {ap to (ap right (glue (f₃₂ c)))}

    ap-ap-coh!-lhs-i : _
    ap-ap-coh!-lhs-i = ! (ap-∙∙`∘`∘ to (right ∘ left) (right ∘ right) (H₃₁ c) (ap right (glue (f₃₂ c))) (H₃₃ c))

    ap-ap-coh!-rhs-i : _
    ap-ap-coh!-rhs-i = ap-∙∙`∘`∘ to (left ∘ left) (left ∘ right) (H₁₁ c) (ap left (glue (f₁₂ c))) (H₁₃ c)

    ap-ap-coh!-lhs-o : _
    ap-ap-coh!-lhs-o = ap-∙∙!'`∘`∘ to (left ∘ right) (right ∘ right) (H₁₃ c) (glue (right (f₂₃ c))) (H₃₃ c)

    ap-ap-coh!-rhs-o : _
    ap-ap-coh!-rhs-o = ! (ap-!'∙∙`∘`∘ to (left ∘ left) (right ∘ left) (H₁₁ c) (glue (left (f₂₁ c))) (H₃₁ c))

    ap-ap-coh!-β : (α : _)
            → ap□ to (coh! α) == ap-ap-coh! (ap□ to α
                                             ∙□-i/ ap-ap-coh!-lhs-i
                                                 / ap-ap-coh!-rhs-i /)
                                 ∙□-i/ ap-ap-coh!-lhs-o
                                     / ap-ap-coh!-rhs-o /
    ap-ap-coh!-β α = ap□-coh! {g₁ = left ∘ right} {right ∘ right} {left ∘ left} {right ∘ left} to
                              {u = glue (left (f₂₁ c))} {H₃₁ c} {ap right (glue (f₃₂ c))} {H₃₃ c}
                              {H₁₁ c} {ap left (glue (f₁₂ c))} {H₁₃ c} {glue (right (f₂₃ c))}
                              α

open E∙₂Red

module E∙₂ = PushoutElim {d = span _ _ _ f₁₂ f₃₂} {P = λ c → i∙₀ (f∙₁ c) == i∙₄ (f∙₃ c)}
  (ap left ∘ glue) (ap right ∘ glue)
  (λ c → ↓-='-in (coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                          ∙□-i/ lhs-i c / rhs-i c /)
                  ∙□-i/ lhs-o c / rhs-o c /))

e∙₂ : (c : A∙₂) → i∙₀ (f∙₁ c) == i∙₄ (f∙₃ c)
e∙₂ = E∙₂.f

module From = PushoutRec {d = h-v-span} {D = Pushout^2 d}
                       i∙₀ i∙₄ e∙₂

from : Pushout^2 (transpose d) → Pushout^2 d
from = From.f

from-glue-glue-β : (c : A₂₂) → ap↓ (ap from) (apd glue (glue c))
                          == (↓-='-in (coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                                              ∙□-i/ lhs-i c / rhs-i c /)
                                       ∙□-i/ lhs-o c / rhs-o c /))
                              ◃/ From.glue-β (left (f₁₂ c)) / ! (From.glue-β (right (f₃₂ c))) /
from-glue-glue-β c = ∘'-apd (ap from) glue (glue c)
                   ∙ coh1 {p = apd (ap from ∘ glue) (glue c)} {From.glue-β (right (f₃₂ c))}
                          {From.glue-β (left (f₁₂ c))} {apd e∙₂ (glue c)}
                          (↓-=-out (apd From.glue-β (glue c)))
                   ∙ (E∙₂.glue-β c |in-ctx (λ u → u ◃/ From.glue-β (left (f₁₂ c)) / ! (From.glue-β (right (f₃₂ c)))/))

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module general-util where

open import instances public

get-file-contents : (filename : string) → IO (maybe string)
get-file-contents e =
  doesFileExist e >>= λ b →
     if b then
      (readFiniteFile e >>= λ s → return (just s))
     else
      return nothing

maybe-else : ∀{ℓ}{A B : Set ℓ} → B → (A → B) → maybe A → B
maybe-else y f (just x) = f x
maybe-else y f nothing = y

maybe-else' : ∀{ℓ}{A B : Set ℓ} → maybe A → B → (A → B) → B
maybe-else' m y f = maybe-else y f m

maybe-join : ∀ {a} {A : Set a} → maybe (maybe A) → maybe A
maybe-join = maybe-else nothing id

maybe-equal? : ∀ {a} {A : Set a} → (A → A → 𝔹) → (m₁ m₂ : maybe A) → 𝔹
maybe-equal? f (just x) (just x₁) = f x x₁
maybe-equal? f (just x) nothing = ff
maybe-equal? f nothing (just x) = ff
maybe-equal? f nothing nothing = tt

_maybe-or_ : ∀ {ℓ} {A : Set ℓ} → maybe A → maybe A → maybe A
(nothing maybe-or ma) = ma
(just a  maybe-or ma) = just a

maybe-not : ∀ {ℓ} {A : Set ℓ} → maybe A → maybe ⊤
maybe-not (just a) = nothing
maybe-not nothing = just triv

maybe-if : 𝔹 → maybe ⊤
maybe-if tt = just triv
maybe-if ff = nothing

when : ∀ {A : Set} → 𝔹 → A → maybe A
when b a = maybe-if b >> just a

unless : ∀ {A : Set} → 𝔹 → A → maybe A
unless b a = maybe-if (~ b) >> just a

trie-lookupd : ∀ {A : Set} → trie A → string → A → A
trie-lookupd t s d with trie-lookup t s
trie-lookupd t s d | nothing = d
trie-lookupd t s d | just x = x

trie-lookup-else : ∀{A : Set} → A → trie A → string → A
trie-lookup-else d t s = trie-lookupd t s d

trie-single : ∀{A : Set} → string → A → trie A
trie-single s x = trie-insert empty-trie s x

trie-any : ∀{A : Set} → (A → 𝔹) → trie A  → 𝔹
trie-cal-any : ∀{A : Set} → (A → 𝔹) → cal (trie A)  → 𝔹
trie-any f (Node odata ts) = maybe-else (trie-cal-any f ts) f odata
trie-cal-any f [] = ff
trie-cal-any f ((c , t) :: cs) = trie-any f t || trie-cal-any f cs

trie-all : ∀{A : Set} → (A → 𝔹) → trie A → 𝔹
trie-all f = ~_ ∘ trie-any (~_ ∘ f)

trie-lookup𝕃 : ∀ {A : Set} → trie (𝕃 A) → string → 𝕃 A
trie-lookup𝕃 t s = trie-lookupd t s []

trie-lookup𝕃2 : ∀ {A : Set} → trie (string × 𝕃 A) → string → string × 𝕃 A
trie-lookup𝕃2 t s = trie-lookupd t s ("[nomod]" , [])

trie-lookup-string : trie string → string → string
trie-lookup-string t s = trie-lookupd t s "[not-found]"

trie-insert-append : ∀ {A : Set} → trie (𝕃 A) → string → A → trie (𝕃 A)
trie-insert-append t s a = trie-insert t s (a :: (trie-lookup𝕃 t s))

trie-insert-append2 : ∀ {A : Set} → trie (string × 𝕃 A) → string → string → A → trie (string × 𝕃 A)
trie-insert-append2 t s mn a = trie-insert t s (mn , (a :: snd (trie-lookup𝕃2 t s)))

trie-fill : ∀{A : Set} → trie A → 𝕃 (string × A) → trie A
trie-fill t ((s , a) :: vs) = trie-fill (trie-insert t s a) vs
trie-fill t [] = t

trie-empty? : ∀ {A} → trie A → 𝔹
trie-empty? t = ~ trie-nonempty t

trie-filter : ∀ {A} → (A → 𝔹) → trie A → trie A
cal-filter  : ∀ {A} → (A → 𝔹) → cal (trie A) → cal (trie A)

trie-filter f (Node odata ts'@(c :: ts))
  = Node odata (cal-filter f ts')
trie-filter f t@(Node (just x) [])
  = if f x then t else empty-trie
trie-filter f (Node nothing [])
  = empty-trie

cal-filter f [] = []
cal-filter f ((a , t) :: c)
  with trie-filter f t | cal-filter f c
... | t' | c'
  = if trie-empty? t then c' else (a , t') :: c'

trie-fold : ∀ {F : Set → Set} {A B : Set} → trie A →
            F B → (string → A → F B → F B) → F B
trie-fold t n c = foldr (λ {(k , v) → c k v}) n (trie-mappings t)

trie-catMaybe : ∀ {A} → trie (maybe A) → trie A
cal-catMaybe  : ∀ {A} → cal (trie (maybe A)) → cal (trie A)

trie-catMaybe (Node odata ts'@(t :: ts)) = Node (maybe-join odata) (cal-catMaybe ts')
trie-catMaybe (Node odata []) = maybe-else empty-trie (λ a → Node (just a) []) (maybe-join odata)

cal-catMaybe [] = []
cal-catMaybe ((c , tr) :: trs)
  with trie-catMaybe tr | cal-catMaybe trs
... | tr' | trs' = if trie-empty? tr' then trs' else (c , tr') :: trs'

trie-equal? : ∀ {A : Set} → (A → A → 𝔹) → (t₁ t₂ : trie A) → 𝔹
trie-equal? {A} f t₁ t₂ =
    length t₁𝕃 =ℕ length t₂𝕃
  && list-all check-elems t₁𝕃
  where
    t₁𝕃 = trie-mappings t₁
    t₂𝕃 = trie-mappings t₂

    check-elems : string × A → 𝔹
    check-elems (name , dat₁) with trie-lookup t₂ name
    ... | nothing = ff
    ... | just dat₂ = f dat₁ dat₂

string-split-h : 𝕃 char → char → 𝕃 char → 𝕃 string → 𝕃 string
string-split-h [] delim str-build out = reverse ((𝕃char-to-string (reverse str-build)) :: out)
string-split-h (c :: cs) delim str-build out with (c =char delim)
... | tt = string-split-h cs delim [] ((𝕃char-to-string (reverse str-build)) :: out)
... | ff = string-split-h cs delim (c :: str-build) out

string-split : string → char → 𝕃 string
string-split str delim = string-split-h (string-to-𝕃char str) delim [] []

undo-escape-string-h : 𝕃 char → 𝕃 char → 𝕃 char
undo-escape-string-h ('\\' :: 'n' :: rest) so-far = undo-escape-string-h rest ('\n' :: so-far)
undo-escape-string-h ('\\' :: '\"' :: rest) so-far = undo-escape-string-h rest ('\"' :: so-far)
undo-escape-string-h (c :: rest) so-far = undo-escape-string-h rest (c :: so-far)
undo-escape-string-h [] so-far = reverse so-far

undo-escape-string : string → string
undo-escape-string str = 𝕃char-to-string (undo-escape-string-h (string-to-𝕃char str) [])

is-pfx : (pfx str : string) → maybe string
is-pfx pfx str = h (string-to-𝕃char pfx) (string-to-𝕃char str) where
  h : 𝕃 char → 𝕃 char → maybe string
  h [] cs = just (𝕃char-to-string cs)
  h (cₚ :: csₚ) [] = nothing
  h (cₚ :: csₚ) (cₛ :: csₛ) with cₚ =char cₛ
  ...| ff = nothing
  ...| tt = h csₚ csₛ

-- functions.agda
curry : ∀{ℓ₁ ℓ₂ ℓ₃}{A : Set ℓ₁}{B : Set ℓ₂}{C : Set ℓ₃}
        → (A × B → C) → A → B → C
curry f a b = f (a , b)

uncurry : ∀{ℓ₁ ℓ₂ ℓ₃}{A : Set ℓ₁}{B : Set ℓ₂}{C : Set ℓ₃}
          → (f : A → B → C) → (p : A × B) → C
uncurry f (a , b) = f a b

uncurry₂ : ∀{a b c d}{A : Set a}{B : Set b}{C : Set c}{D : Set d}
          → (f : A → B → C → D) → (p : A × B × C) → D
uncurry₂ f (a , b , c) = f a b c

elim-pair : ∀{ℓ₀ ℓ₁ ℓ₂}{A : Set ℓ₀}{B : Set ℓ₁}{C : Set ℓ₂}
            → A × B → (A → B → C) → C
elim-pair (a , b) f = f a b

elim-Σi : ∀ {ℓ₀ ℓ₁ ℓ₂} {A : Set ℓ₀} {B : A → Set ℓ₁} {X : Set ℓ₂}
          → Σi A B → ({a : A} → B a → X) → X
elim-Σi (, b) f = f b

elim_for : ∀ {ℓ₀ ℓ₁ ℓ₂} {A : Set ℓ₀} {B : Set ℓ₁} {X : Set ℓ₂} → A × B → (A → B → X) → X
elim (a , b) for f = f a b

infixr 0 case_ret_of_ case_of_

case_ret_of_ :
  ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁}
  (x : A) (B : A → Set ℓ₂) → ((x : A) → B x) → B x
case x ret B of f = f x

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

case₂_,_of_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → A → B → (A → B → C) → C
case₂ x , y of f = f x y

flip : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
       → (A → B → C) → (B → A → C)
flip f = λ b a → f a b

const : ∀ {a b} {A : Set a} {B : Set b} →
        A → B → A
const a b = a

infixr 0 _$_
_$_ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → A → B
f $ x = f x

-- _∘_ just needs a fixity and association declaration in the IAL
infixr 9 _∘'_
_∘'_ : ∀ {a b c} {A : Set a}{B : Set b}{C : Set c}
         → (B → C) → (A → B) → A → C
g ∘' f = λ a → g (f a)

-- list.agda

take : ∀{ℓ}{A : Set ℓ} → ℕ → 𝕃 A → 𝕃 A
take 0 l = []
take (suc n) (x :: l) = x :: (take n l)
take (suc n) [] = []

drop : ∀{ℓ}{A : Set ℓ} → ℕ → 𝕃 A → 𝕃 A
drop zero xs = xs
drop (suc _) [] = []
drop (suc n) (x :: xs) = drop n xs

drop-last : ∀{ℓ}{A : Set ℓ} → ℕ → 𝕃 A → 𝕃 A
drop-last n xs = take (length xs ∸ n) xs

zip-with : ∀{ℓ₁ ℓ₂ ℓ₃}{A : Set ℓ₁}{B : Set ℓ₂}{C : Set ℓ₃}
           → (A → B → C) → 𝕃 A → 𝕃 B → 𝕃 C
zip-with f xs ys = map (uncurry f) (zip xs ys)

for_yield_ : ∀ {a b} {A : Set a} {B : Set b} → 𝕃 A → (A → B) → 𝕃 B
for xs yield f = map f xs

for_accum_use_ : ∀ {a b} {A : Set a} {B : Set b} → 𝕃 A → B → (A → B → B) → B
for xs accum n use f = foldr f n xs

foldl : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → (A → B → B) → B → 𝕃 A → B
foldl f b [] = b
foldl f b (a :: as) = foldl f (f a b) as

foldr' : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → B → (A → B → B) → 𝕃 A → B
foldr' = flip foldr

-- error.agda
err-guard : 𝔹 → string → error-t ⊤
err-guard tt msg = yes-error msg
err-guard ff _   = no-error triv

-- sum.agda
either-else' : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → A ∨ B → (A → C) → (B → C) → C
either-else' (inj₁ x) f g = f x
either-else' (inj₂ y) f g = g y

either-else : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → (A → C) → (B → C) → A ∨ B → C
either-else f g (inj₁ x) = f x
either-else f g (inj₂ y) = g y

err⊎-guard : ∀ {e} {E : Set e} → 𝔹 → E → E ∨ ⊤
err⊎-guard tt err = inj₁ err
err⊎-guard ff _   = inj₂ triv

--infixl 1 _≫⊎_
--_≫⊎_ : ∀ {E B : Set} → E ∨ ⊤ → E ∨ B → E ∨ B
--m₁ ≫⊎ m₂ = m₁ ≫=⊎ λ _ → m₂

-- Some file writing functions
data IOMode : Set where
  ReadMode : IOMode
  WriteMode : IOMode
  AppendMode : IOMode
  ReadWriteMode : IOMode

filepath = string

postulate
  Handle : Set
  -- IOMode : Set
  openFile : filepath → IOMode -> IO Handle
  closeFile : Handle -> IO ⊤
  hPutStr : Handle → string → IO ⊤
  hSetToLineBuffering : Handle → IO ⊤
  hFlush : Handle → IO ⊤
  stdout : Handle
  doesDirectoryExist : filepath → IO 𝔹

{-# FOREIGN GHC import qualified System.IO #-}
{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# FOREIGN GHC import qualified System.Directory #-}
{-# COMPILE GHC Handle = type System.IO.Handle #-}
{-# COMPILE GHC IOMode = data System.IO.IOMode (System.IO.ReadMode | System.IO.WriteMode | System.IO.AppendMode | System.IO.ReadWriteMode) #-}
{-# COMPILE GHC hSetToLineBuffering = \ hdl -> System.IO.hSetBuffering hdl System.IO.LineBuffering #-}
{-# COMPILE GHC hFlush = System.IO.hFlush #-}
{-# COMPILE GHC stdout = System.IO.stdout #-}
{-# COMPILE GHC openFile = \ fp mode -> do outh <- System.IO.openFile (Data.Text.unpack fp) mode; System.IO.hSetNewlineMode outh System.IO.noNewlineTranslation; System.IO.hSetEncoding outh System.IO.utf8; return outh #-}
{-# COMPILE GHC closeFile = System.IO.hClose #-}
{-# COMPILE GHC hPutStr = Data.Text.IO.hPutStr #-}
{-# COMPILE GHC doesDirectoryExist = System.Directory.doesDirectoryExist . Data.Text.unpack #-}

clearFile : filepath → IO ⊤
clearFile fp = openFile fp WriteMode >>= λ hdl → hPutStr hdl "" >> closeFile hdl

flush : IO ⊤
flush = hFlush stdout

setToLineBuffering : IO ⊤
setToLineBuffering = hSetToLineBuffering stdout

withFile : {A : Set} → filepath → IOMode → (Handle → IO A) → IO A
withFile fp mode f = openFile fp mode >>= λ hdl → f hdl >≯ closeFile hdl

-- Coordinated Universal Time
infix 15 _utc-after_ _utc-before_

postulate
  UTC : Set
  getCurrentTime : IO UTC
  _utc-after_ : UTC → UTC → 𝔹
  _utc-before_ : UTC → UTC → 𝔹
  utcToString : UTC → string
  getModificationTime : filepath → IO UTC
  getCurrentDirectory : IO filepath
  pathSeparator : char

{-# FOREIGN GHC import qualified Data.Time.Clock #-}
{-# FOREIGN GHC import qualified Data.Time.Calendar #-}
{-# FOREIGN GHC import qualified System.FilePath #-}
{-# COMPILE GHC UTC = type Data.Time.Clock.UTCTime #-}
{-# COMPILE GHC getCurrentTime = Data.Time.Clock.getCurrentTime #-}
{-# COMPILE GHC _utc-after_ = (>) #-}
{-# COMPILE GHC _utc-before_ = (<) #-}
{-# COMPILE GHC utcToString = Data.Text.pack . show #-}
{-# COMPILE GHC getModificationTime = System.Directory.getModificationTime . Data.Text.unpack #-}
{-# COMPILE GHC getCurrentDirectory = System.Directory.getCurrentDirectory >>= return . Data.Text.pack #-}
{-# COMPILE GHC pathSeparator = System.FilePath.pathSeparator #-}

pathSeparatorString = 𝕃char-to-string [ pathSeparator ]

splitPath : filepath → 𝕃 string
splitPath = h [] [] ∘ string-to-𝕃char where
  cons-if-nonempty : 𝕃 char → 𝕃 string → 𝕃 string
  cons-if-nonempty [] acc = acc
  cons-if-nonempty cur acc = 𝕃char-to-string (reverse cur) :: acc
  h : 𝕃 string → 𝕃 char → 𝕃 char → 𝕃 string
  h acc cur [] = reverse (cons-if-nonempty cur acc)
  h acc cur (c :: cs) with c =char pathSeparator
  ...| tt = h (cons-if-nonempty cur acc) [] cs
  ...| ff = h acc (c :: cur) cs

joinPath : 𝕃 string → filepath
joinPath [] = ""
joinPath (x :: []) = x
joinPath (x :: xs) = x ^ pathSeparatorString ^ joinPath xs

pathIsAbsolute : filepath → 𝔹
pathIsAbsolute = maybe-else ff (λ c → (c =char '~') || (c =char pathSeparator)) ∘ (head2 ∘ string-to-𝕃char)

filepath-replace-tilde : filepath → IO (maybe filepath)
filepath-replace-tilde fp with string-to-𝕃char fp
...| '~' :: '/' :: fp-cs = getHomeDirectory >>=r λ home →
                           just (combineFileNames home (𝕃char-to-string fp-cs))
...| fp-cs = return nothing

-- string binary tree, for more efficient I/O printing than concatenation
data rope : Set where
  _⊹⊹_ : rope → rope → rope
  [[_]] : string → rope

infixl 9 _⊹⊹_
infix 9 [[_]]

[[]] : rope
[[]] = [[ "" ]]

rope-to-string : rope → string
rope-to-string = flip h "" where
  h : rope → string → string
  h (s₁ ⊹⊹ s₂) = h s₁ ∘ h s₂
  h [[ s ]] acc = s ^ acc

rope-length : rope → ℕ
rope-length [[ s ]] = string-length s
rope-length (r₁ ⊹⊹ r₂) = rope-length r₁ + rope-length r₂

𝕃-to-rope : ∀{A : Set} → (A → rope) → string → 𝕃 A → rope
𝕃-to-rope to-rope sep [] = [[]]
𝕃-to-rope to-rope sep (x :: []) = to-rope x
𝕃-to-rope to-rope sep (x :: xs) = to-rope x ⊹⊹ [[ sep ]] ⊹⊹ 𝕃-to-rope to-rope sep xs

putStrLn : string → IO ⊤
putStrLn str = putStr str >> putStr "\n" -- >> flush

putRope : rope → IO ⊤
-- putRope = putStr ∘ rope-to-string
putRope s = h s (return triv) where
  h : rope → IO ⊤ → IO ⊤
  h (s₁ ⊹⊹ s₂) io = h s₁ (h s₂ io)
  h [[ s ]] io = putStr s >> io

putRopeLn : rope → IO ⊤
putRopeLn s = putRope s >> putStr "\n" -- >> flush

hPutRope : Handle → rope → IO ⊤
hPutRope outh s = h s (return triv) outh where
  h : rope → IO ⊤ → Handle → IO ⊤
  h (s₁ ⊹⊹ s₂) io outh = h s₁ (h s₂ io outh) outh
  h [[ s ]] io outh = hPutStr outh s >> io

writeRopeToFile : filepath → rope → IO ⊤
writeRopeToFile fp s = clearFile fp >> openFile fp AppendMode >>= λ hdl → hPutRope hdl s >> closeFile hdl

stringset-singleton : string → stringset
stringset-singleton x = stringset-insert empty-stringset x

set-nth : ∀ {ℓ} {X : Set ℓ} → ℕ → X → 𝕃 X → 𝕃 X
set-nth n x [] = []
set-nth zero x (x' :: xs) = x :: xs
set-nth (suc n) x (x' :: xs) = x' :: set-nth n x xs

map-fst : ∀ {ℓ₀ ℓ₁ ℓ₂} {X₀ : Set ℓ₀} {X₁ : Set ℓ₁} {X₂ : Set ℓ₂} → (X₀ → X₂) → (X₀ × X₁) → (X₂ × X₁)
map-fst f (x₀ , x₁) = (f x₀ , x₁)

map-snd : ∀ {ℓ₀ ℓ₁ ℓ₂} {X₀ : Set ℓ₀} {X₁ : Set ℓ₁} {X₂ : Set ℓ₂} → (X₁ → X₂) → (X₀ × X₁) → (X₀ × X₂)
map-snd f (x₀ , x₁) = (x₀ , f x₁)

--cons = _::_
--nil = []

--data 𝕃ᵢ (A : ℕ → Set) : ℕ → Set where
--  cons : ∀ {n} → A 0 → 𝕃ᵢ A n → 𝕃ᵢ A (suc n)
--  nil : 𝕃ᵢ A 0

--pattern _,_ = _::_

--{-# TERMINATING #-}
--𝕃ᵢ-nests : Set → ℕ → Set
--𝕃ᵢ-nests A 0 = A
--𝕃ᵢ-nests A (suc n) = 𝕃ᵢ (𝕃ᵢ-nests A) 1

--cons' : ∀ {A n} → A → 𝕃ᵢ (𝕃ᵢ-nests A) n → 𝕃ᵢ (𝕃ᵢ-nests A) (suc n)
--cons' h t = cons h t

{-
-- Syntactic sugar for Haskell-esque list construction
infixr 4 _,,_
infixr 5 [:_ _:]

[:_ = id

_:] = [_]

_,,_ : ∀ {ℓ} {A : Set ℓ} → A → 𝕃 A → 𝕃 A
_,,_ = _::_
-}

infixr 4 _⌟_
_⌟_ : ∀ {ℓ}{A : Set ℓ}{b : 𝔹} → A → if b then A else 𝕃 A → 𝕃 A
_⌟_ {b = tt} a a' = a :: a' :: []
_⌟_ {b = ff} a as = a :: as

[:_:] = id

𝕃-sugar-example = [: 0 ⌟ 1 ⌟ 2 ⌟ 3 ⌟ 4 :]

{-
postulate
  ord : char → ℕ
  chr : ℕ → char
{-# FOREIGN GHC import qualified Data.Char #-}
{-# COMPILE GHC ord = toInteger . Data.Char.ord #-}
{-# COMPILE GHC chr = Data.Char.chr . fromIntegral #-}

toLower : char → char
toLower c =
  let n = ord c
      up? = n ≥ 65 {- A -} && n ≤ 90 {- Z -} in
  chr (if up? then n ∸ 32 else n)

toUpper : char → char
toUpper c =
  let n = ord c
      low? = n ≥ 97 {- A -} && n ≤ 122 {- Z -} in
  chr (if low? then n + 32 else n)

capitalize : string → string
capitalize x with string-to-𝕃char x
...| [] = ""
...| c :: cs = 𝕃char-to-string (toUpper c :: cs)

uncapitalize : string → string
uncapitalize x with string-to-𝕃char x
...| [] = ""
...| c :: cs = 𝕃char-to-string (toLower c :: cs)
-}

max_stars_repo_name: zmthy/cedille

max_issues_repo_name: zmthy/cedille

max_forks_repo_name: zmthy/cedille


text:
------------------------------------------------------------------------
-- M-types for indexed containers, defined coinductively (in Cubical
-- Agda)
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe --guardedness #-}

import Equality.Path as P

module Container.Indexed.Variant.M.Codata
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Container.Indexed equality-with-J using (_⇾_; _∘⇾_)
open import Container.Indexed.Variant equality-with-J
  hiding (Final′≃Final′)
import Container.Indexed.Variant P.equality-with-J as PC
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J
open import H-level equality-with-J

private
  variable
    a iℓ s  : Level
    A I     : Type a
    i p q x : A
    C       : Container I s p
    n       : ℕ

-- An M-type for a given container.
--
-- This definition is similar to one in "Indexed containers" by
-- Altenkirch, Ghani, Hancock, McBride and Morris.

record M {I : Type iℓ} (C : Container I s p) (i : I) :
         Type (iℓ ⊔ s ⊔ p) where
  coinductive
  constructor in-M
  field
    out-M : ⟦ C ⟧ (M C) i

open M public

-- An η-law.

η : in-M (out-M x) ≡ x
η = _↔_.from ≡↔≡ η′
  where
  η′ : in-M (out-M x) P.≡ x
  η′ {x = x} _ .out-M = x .out-M

-- M C is, in a certain sense, a fixpoint of ⟦ C ⟧.

M-fixpoint : ⟦ C ⟧ (M C) i ≃ M C i
M-fixpoint = Eq.↔→≃ in-M out-M (λ _ → η) refl

-- A coalgebra defined using M and out-M.

M-coalgebra : (C : Container I s p) → Coalgebra C
M-coalgebra C = M C , λ _ → out-M

private

  -- M-coalgebra C is a final coalgebra.
  --
  -- This code is based on code written by Andrea Vezzosi for the
  -- cubical library.

  M-final′′ : PC.Final′ (M-coalgebra C)
  M-final′′ {C = C@(S ◁ P)} Y@(Q , f) = unfold , unique
    where
    g : Q ⇾ M C
    g i q .out-M .proj₁     = f i q .proj₁
    g i q .out-M .proj₂ j p = g j (f i q .proj₂ j p)

    g-ok : (λ _ → out-M) ∘⇾ g P.≡ map C g ∘⇾ f
    g-ok i j q .proj₁            = f j q .proj₁
    g-ok i j q .proj₂ k p .out-M = g-ok i k (f j q .proj₂ k p)

    unfold : Y PC.⇨ M-coalgebra C
    unfold = g , g-ok

    module _ (u : Y PC.⇨ M-coalgebra C) where

      lemma₁ :
        x P.≡ u .proj₁ i q →
        x .out-M .proj₁ P.≡
        (map C (u .proj₁) ∘⇾ f) i q .proj₁
      lemma₁ {i = i} {x = x} {q = q} eq =
        x .out-M .proj₁                     P.≡⟨ P.cong (λ x → x .out-M .proj₁) eq ⟩
        u .proj₁ i q .out-M .proj₁          P.≡⟨ P.cong (λ f → f i q .proj₁) (u .proj₂) ⟩∎
        (map C (u .proj₁) ∘⇾ f) i q .proj₁  ∎

      lemma₂ :
        (eq : x P.≡ u .proj₁ i q) →
        P.[ (λ l → P (lemma₁ eq l) ⇾ M C) ]
          x .out-M .proj₂ ≡
          (map C (u .proj₁) ∘⇾ f) i q .proj₂
      lemma₂ {i = i} {x = x} {q = q} eq =
        x .out-M .proj₂                     P.≡⟨ P.hcong (λ x → x .out-M .proj₂) eq ⟩[ (λ p → P p ⇾ M C) ]
        u .proj₁ i q .out-M .proj₂          P.≡⟨ P.hcong (λ f → f i q .proj₂) (u .proj₂) ⟩∎h
        (map C (u .proj₁) ∘⇾ f) i q .proj₂  ∎

      unique′ : ∀ i q x → x P.≡ u .proj₁ i q → x P.≡ g i q
      unique′ _ _ _ eq j .out-M .proj₁     = lemma₁ eq j
      unique′ i q x eq j .out-M .proj₂ k p =
        unique′ k (f i q .proj₂ k p₁) (x .out-M .proj₂ k p₀) lemma₂′ j
        where
        lem₁ = lemma₁ eq

        p₀ : P (lem₁ P.0̲) k
        p₁ : P (lem₁ P.1̲) k
        p₀ = P.transport (λ l → P (lem₁ (P.min j (P.- l))) k) (P.- j) p
        p₁ = P.transport (λ l → P (lem₁ (P.max j      l )) k)      j  p

        p₀≡p₁ : P.[ (λ l → P (lem₁ l) k) ] p₀ ≡ p₁
        p₀≡p₁ = P.elim¹
          (λ eq →
             ∀ p →
             P.[ (λ l → eq l) ]
               P.transport (λ l → eq (P.min j (P.- l))) (P.- j) p ≡
               P.transport (λ l → eq (P.max j      l ))      j  p)
          (λ p →
             P.transport (λ _ → P (x .out-M .proj₁) k) (P.- j) p  P.≡⟨ P.cong (_$ p) $ P.transport-refl (P.- j) ⟩
             p                                                    P.≡⟨ P.cong (_$ p) $ P.sym $ P.transport-refl j ⟩∎
             P.transport (λ _ → P (x .out-M .proj₁) k) j p        ∎)
          (P.cong (λ s → P s k) lem₁)
          p

        lemma₂′ :
          x .out-M .proj₂ k p₀ P.≡
          (map C (u .proj₁) ∘⇾ f) i q .proj₂ k p₁
        lemma₂′ l = lemma₂ eq l k (p₀≡p₁ l)

      unique : unfold .proj₁ P.≡ u .proj₁
      unique =
        P.⟨ext⟩ λ _ → P.⟨ext⟩ λ _ → P.sym $
        unique′ _ _ _ P.refl

  -- Finality expressed using equality is equivalent to finality
  -- expressed using paths.

  Final′≃Final′ :
    (X : Coalgebra C) →
    Final′ X ≃ PC.Final′ X
  Final′≃Final′ X =
    (∀ Y → ∃ λ (m : Y    ⇨ X) → (m′ : Y    ⇨ X) → proj₁ m ≡ proj₁ m′)    ↔⟨ (∀-cong ext λ _ →
                                                                             Σ-cong (lemma _) λ _ →
                                                                             Π-cong ext (lemma _) λ _ →
                                                                             ≡↔≡) ⟩□
    (∀ Y → ∃ λ (m : Y PC.⇨ X) → (m′ : Y PC.⇨ X) → proj₁ m P.≡ proj₁ m′)  □
    where
    lemma : ∀ Y → (Y ⇨ X) ↔ (Y PC.⇨ X)
    lemma Y = ∃-cong λ _ → ≡↔≡

-- M-coalgebra C is a final coalgebra.
--
-- The lemma M-final′′ is based on code written by Andrea Vezzosi for
-- the cubical library.

M-final′ :
  (C : Container I s p) →
  Final′ (M-coalgebra C)
M-final′ C = _≃_.from (Final′≃Final′ (M-coalgebra C)) M-final′′

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality