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

open import HoTT
open import groups.HomSequence

module cohomology.Theory where

-- [i] for the universe level of the group
record CohomologyTheory i : Type (lsucc i) where
  {- functorial parts -}
  field
    C : ℤ → Ptd i → Group i

    C-is-abelian : (n : ℤ) (X : Ptd i) → is-abelian (C n X)

  C-abgroup : ℤ → Ptd i → AbGroup i
  C-abgroup n X = C n X , C-is-abelian n X

  CEl : ℤ → Ptd i → Type i
  CEl n X = Group.El (C n X)

  Cident : (n : ℤ) (X : Ptd i) → CEl n X
  Cident n X = Group.ident (C n X)

  ⊙CEl : ℤ → Ptd i → Ptd i
  ⊙CEl n X = ⊙[ CEl n X , Cident n X ]

  {- functorial parts -}
  field
    C-fmap : (n : ℤ) {X Y : Ptd i} → X ⊙→ Y → (C n Y →ᴳ C n X)

  CEl-fmap : (n : ℤ) {X Y : Ptd i} → X ⊙→ Y → (CEl n Y → CEl n X)
  CEl-fmap n f = GroupHom.f (C-fmap n f)

  field
    C-fmap-idf : (n : ℤ) {X : Ptd i}
      → ∀ x → CEl-fmap n {X} {X} (⊙idf X) x == x

    C-fmap-∘ : (n : ℤ) {X Y Z : Ptd i} (g : Y ⊙→ Z) (f : X ⊙→ Y)
      → ∀ x → CEl-fmap n (g ⊙∘ f) x == CEl-fmap n f (CEl-fmap n g x)

  field
    C-Susp : (n : ℤ) (X : Ptd i) → C (succ n) (⊙Susp X) ≃ᴳ C n X

  CEl-Susp : (n : ℤ) (X : Ptd i) → CEl (succ n) (⊙Susp X) ≃ CEl n X
  CEl-Susp n X = GroupIso.f-equiv (C-Susp n X)

  field
    -- This naming is stretching the convention
    C-Susp-fmap : (n : ℤ) {X Y : Ptd i} (f : X ⊙→ Y)
      → CommSquareᴳ (C-fmap (succ n) (⊙Susp-fmap f)) (C-fmap n f)
          (GroupIso.f-hom (C-Susp n Y)) (GroupIso.f-hom (C-Susp n X))

  C-Susp-fmap-cse : (n : ℤ) {X Y : Ptd i} (f : X ⊙→ Y)
    → CommSquareEquivᴳ (C-fmap (succ n) (⊙Susp-fmap f)) (C-fmap n f)
        (GroupIso.f-hom (C-Susp n Y)) (GroupIso.f-hom (C-Susp n X))
  C-Susp-fmap-cse n {X} {Y} f = C-Susp-fmap n f , GroupIso.f-is-equiv (C-Susp n Y) , GroupIso.f-is-equiv (C-Susp n X)

  C-Susp-fmap' : (n : ℤ) {X Y : Ptd i} (f : X ⊙→ Y)
    → CommSquareᴳ (C-fmap n f) (C-fmap (succ n) (⊙Susp-fmap f))
        (GroupIso.g-hom (C-Susp n Y)) (GroupIso.g-hom (C-Susp n X))
  C-Susp-fmap' n f = fst (CommSquareEquivᴳ-inverse-v (C-Susp-fmap-cse n f))

  CEl-Susp-fmap : (n : ℤ) {X Y : Ptd i} (f : X ⊙→ Y)
    → CommSquare (CEl-fmap (succ n) (⊙Susp-fmap f)) (CEl-fmap n f)
        (GroupIso.f (C-Susp n Y)) (GroupIso.f (C-Susp n X))
  CEl-Susp-fmap n f = comm-sqr λ y' → C-Susp-fmap n f □$ᴳ y'

  field
    C-exact : (n : ℤ) {X Y : Ptd i} (f : X ⊙→ Y)
      → is-exact (C-fmap n (⊙cfcod' f)) (C-fmap n f)

  C-additive : (n : ℤ) {I : Type i} (Z : I → Ptd i)
    → C n (⊙BigWedge Z) →ᴳ Πᴳ I (λ i → C n (Z i))
  C-additive n Z = Πᴳ-fanout (C-fmap n ∘ ⊙bwin {X = Z})

  CEl-additive : (n : ℤ) {I : Type i} (Z : I → Ptd i)
    → CEl n (⊙BigWedge Z) → Π I (λ i → CEl n (Z i))
  CEl-additive n Z = GroupHom.f (C-additive n Z)

  field
    C-additive-is-equiv : (n : ℤ) {I : Type i} (Z : I → Ptd i)
      → has-choice 0 I i
      → is-equiv (CEl-additive n Z)

  C-additive-iso : (n : ℤ) {I : Type i} (Z : I → Ptd i)
    → has-choice 0 I i
    → C n (⊙BigWedge Z) ≃ᴳ Πᴳ I (λ i → C n (Z i))
  C-additive-iso n Z ac = C-additive n Z , C-additive-is-equiv n Z ac

  C2 : ℤ → Group i
  C2 n = C n (⊙Lift ⊙Bool)

  C2-is-abelian : (n : ℤ) → is-abelian (C2 n)
  C2-is-abelian n = C-is-abelian n (⊙Lift ⊙Bool)

  C2-abgroup : ℤ → AbGroup i
  C2-abgroup n = C-abgroup n (⊙Lift ⊙Bool)

  -- XXX This is put here due to the limitation of the current Agda.
  -- See issue #434.
  abstract
    ∘-C-fmap : (n : ℤ) {X Y Z : Ptd i} (f : X ⊙→ Y) (g : Y ⊙→ Z)
      → ∀ x → CEl-fmap n f (CEl-fmap n g x) == CEl-fmap n (g ⊙∘ f) x
    ∘-C-fmap n f g x = ! (C-fmap-∘ n g f x)

  CEl-fmap-idf = C-fmap-idf
  CEl-fmap-∘ = C-fmap-∘
  ∘-CEl-fmap = ∘-C-fmap

  CEl-emap : (n : ℤ) {X Y : Ptd i} → X ⊙≃ Y → Group.El (C n Y) ≃ Group.El (C n X)
  CEl-emap n ⊙eq = equiv (CEl-fmap n (⊙–> ⊙eq)) (CEl-fmap n (⊙<– ⊙eq)) to-from from-to where
    abstract
      to-from = λ x → ! (CEl-fmap-∘ n (⊙<– ⊙eq) (⊙–> ⊙eq) x)
                    ∙ ap (λ f → CEl-fmap n f x) (⊙λ= (⊙<–-inv-l ⊙eq))
                    ∙ CEl-fmap-idf n x
      from-to = λ x → ! (CEl-fmap-∘ n (⊙–> ⊙eq) (⊙<– ⊙eq) x)
                    ∙ ap (λ f → CEl-fmap n f x) (⊙λ= (⊙<–-inv-r ⊙eq))
                    ∙ CEl-fmap-idf n x

  abstract
    CEl-isemap : (n : ℤ) {X Y : Ptd i} (f : X ⊙→ Y) → is-equiv (fst f) → is-equiv (CEl-fmap n f)
    CEl-isemap n f f-ise = snd (CEl-emap n (f , f-ise))

  C-emap : (n : ℤ) {X Y : Ptd i} → X ⊙≃ Y → C n Y ≃ᴳ C n X
  C-emap n ⊙eq = ≃-to-≃ᴳ (CEl-emap n ⊙eq) lemma
    where abstract lemma = GroupHom.pres-comp (C-fmap n (⊙–> ⊙eq))

  C-isemap = CEl-isemap

  {- Cohomology groups are independent of basepoint, and the action of
   - the cohomology is independent of the basepoint-preservation path -}

  C-base-indep : (n : ℤ) {A : Type i} (a₀ a₁ : A)
    → C n ⊙[ A , a₀ ] ≃ᴳ C n ⊙[ A , a₁ ]
  C-base-indep n a₀ a₁ =
    C-Susp n ⊙[ _ , a₁ ] ∘eᴳ (C-Susp n ⊙[ _ , a₀ ])⁻¹ᴳ

  private
    abstract
      CEl-fmap-base-indep' : (n : ℤ) {X Y : Ptd i}
        (f : de⊙ X → de⊙ Y) (p₁ p₂ : f (pt X) == pt Y)
        → ∀ y → CEl-fmap n (f , p₁) y == CEl-fmap n (f , p₂) y
      CEl-fmap-base-indep' n {X} {Y} f p₁ p₂ y =
        CEl-fmap n (f , p₁) y
          =⟨ ! $ <–-inv-r (CEl-Susp n Y) y |in-ctx CEl-fmap n (f , p₁) ⟩
        CEl-fmap n (f , p₁) (–> (CEl-Susp n Y) (<– (CEl-Susp n Y) y))
          =⟨ ! $ commutes (CEl-Susp-fmap n (f , p₁)) (<– (CEl-Susp n Y) y) ⟩
        –> (CEl-Susp n X) (CEl-fmap (succ n) (Susp-fmap f , idp) (<– (CEl-Susp n Y) y))
          =⟨ commutes (CEl-Susp-fmap n (f , p₂)) (<– (CEl-Susp n Y) y) ⟩
        CEl-fmap n (f , p₂) (–> (CEl-Susp n Y) (<– (CEl-Susp n Y) y))
          =⟨ <–-inv-r (CEl-Susp n Y) y |in-ctx CEl-fmap n (f , p₂) ⟩
        CEl-fmap n (f , p₂) y
          =∎

  abstract
    -- FIXME is there a better name?
    CEl-fmap-base-indep : (n : ℤ) {X Y : Ptd i} {f g : X ⊙→ Y}
      → (∀ x → fst f x == fst g x)
      → (∀ y → CEl-fmap n f y == CEl-fmap n g y)
    CEl-fmap-base-indep n h y = CEl-fmap-base-indep' n _ _ _ _
                              ∙ ap (λ f → CEl-fmap n f y) (⊙λ=' h (↓-idf=cst-in' idp))
  C-fmap-base-indep = CEl-fmap-base-indep

  {- cohomology of the unit -}
  abstract
    C-Unit : ∀ n → is-trivialᴳ (C n (⊙Lift {j = i} ⊙Unit))
    C-Unit n x =
      x
        =⟨ ! (CEl-fmap-idf n x) ⟩
      CEl-fmap n (⊙idf _) x
        =⟨ CEl-fmap-base-indep n (λ _ → idp) x ⟩
      CEl-fmap n (⊙cst ⊙∘ ⊙cfcod' (⊙idf _)) x
        =⟨ CEl-fmap-∘ n ⊙cst (⊙cfcod' (⊙idf _)) x ⟩
      CEl-fmap n (⊙cfcod' (⊙idf _)) (CEl-fmap n ⊙cst x)
        =⟨ ! (CEl-fmap-idf n (CEl-fmap n (⊙cfcod' (⊙idf _)) (CEl-fmap n ⊙cst x))) ⟩
      CEl-fmap n (⊙idf _) (CEl-fmap n (⊙cfcod' (⊙idf _)) (CEl-fmap n ⊙cst x))
        =⟨ im-sub-ker (C-exact n (⊙idf _)) _ [ CEl-fmap n ⊙cst x , idp ] ⟩
      Cident n (⊙Lift {j = i} ⊙Unit)
        =∎

  {- more functoriality -}
  abstract
    C-fmap-cst : (n : ℤ) {X Y : Ptd i} → ∀ y → CEl-fmap n (⊙cst {X = X} {Y = Y}) y == Cident n X
    C-fmap-cst n {X} {Y} y =
      CEl-fmap n (⊙cst {X = ⊙LU} ⊙∘ ⊙cst {X = X}) y
        =⟨ CEl-fmap-∘ n ⊙cst ⊙cst y ⟩
      CEl-fmap n (⊙cst {X = X}) (CEl-fmap n (⊙cst {X = ⊙LU}) y)
        =⟨ C-Unit n (CEl-fmap n (⊙cst {X = ⊙LU}) y)
           |in-ctx CEl-fmap n (⊙cst {X = X} {Y = ⊙LU}) ⟩
      CEl-fmap n (⊙cst {X = X}) (Cident n ⊙LU)
        =⟨ GroupHom.pres-ident (C-fmap n (⊙cst {X = X} {Y = ⊙LU})) ⟩
      Cident n X ∎
      where
      ⊙LU = ⊙Lift {j = i} ⊙Unit

    C-fmap-const : (n : ℤ) {X Y : Ptd i} {f : X ⊙→ Y}
      → (∀ x → fst f x == pt Y)
      → ∀ y → CEl-fmap n f y == Cident n X
    C-fmap-const n f-is-const y =
      CEl-fmap-base-indep n f-is-const y ∙ C-fmap-cst n y

    -- FIXME Is there a better name?
    C-fmap-inverse : (n : ℤ) {X Y : Ptd i} (f : X ⊙→ Y) (g : Y ⊙→ X)
      → (∀ x → fst g (fst f x) == x)
      → (∀ x → CEl-fmap n f (CEl-fmap n g x) == x)
    C-fmap-inverse n f g p x = ! (CEl-fmap-∘ n g f x) ∙ CEl-fmap-base-indep n p x ∙ C-fmap-idf n x

  CEl-fmap-cst = C-fmap-cst
  CEl-fmap-const = C-fmap-const
  CEl-fmap-inverse = C-fmap-inverse

record OrdinaryTheory i : Type (lsucc i) where
  constructor ordinary-theory
  field
    -- XXX This should be cohomology-thy
    cohomology-theory : CohomologyTheory i
  open CohomologyTheory cohomology-theory public
  field
    C-dimension : {n : ℤ} → n ≠ 0 → is-trivialᴳ (C2 n)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module HyperReal where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Empty
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Level renaming ( suc to succ ; zero to Zero ; _⊔_ to _L⊔_ )
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Binary.Definitions
open import Relation.Binary.Structures
open import nat
open import logic
open import bijection

HyperNat : Set
HyperNat = ℕ → ℕ

open _∧_
open Bijection

n1 : ℕ → ℕ
n1 n = proj1 (fun→ nxn n)

n2 : ℕ → ℕ
n2 n = proj2 (fun→ nxn n)

_n*_ : (i j : HyperNat ) → HyperNat
i n* j = λ k → i k * j k

_n+_ : (i j : HyperNat ) → HyperNat
i n+ j = λ k → i k + j k

hzero : HyperNat
hzero _ = 0

h : (n : ℕ) → HyperNat
h n _ = n

record _n=_  (i j : HyperNat ) :  Set where
   field
      =-map : Bijection ℕ ℕ
      =-m : ℕ
      is-n= : (k : ℕ ) → k > =-m → i k ≡ j (fun→ =-map  k)

open _n=_

record _n≤_  (i j : HyperNat ) :  Set where
   field
      ≤-map : Bijection ℕ ℕ
      ≤-m : ℕ
      is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (fun→ ≤-map  k)

open _n≤_

record _n<_  (i j : HyperNat ) :  Set where
   field
      <-map : Bijection ℕ ℕ
      <-m : ℕ
      is-n< : (k : ℕ ) → k > <-m → i k < j (fun→ <-map  k)

open _n<_

_n<=s≤_ :  (i j : HyperNat ) → (i n< j) ⇔ (( i n+ h 1 ) n≤ j )
_n<=s≤_ = {!!}

¬hn<0 : {x : HyperNat } → ¬ ( x n< h 0 )
¬hn<0 {x} x<0 = ⊥-elim ( nat-≤> (is-n< x<0 (suc (<-m x<0)) a<sa) 0<s )

postulate
   <-cmpn  : Trichotomous {Level.zero} _n=_  _n<_

n=IsEquivalence : IsEquivalence _n=_
n=IsEquivalence = record { refl = record {=-map = bid ℕ ; =-m = 0 ; is-n= = λ _ _ → refl}
  ; sym = λ xy →  record {=-map = bi-sym ℕ ℕ (=-map xy) ; =-m =  =-m xy ; is-n= = λ k lt → {!!} } -- (is-n= xy k lt) }
  ; trans =  λ xy yz →  record {=-map = bi-trans ℕ ℕ ℕ (=-map xy) (=-map yz) ; =-m =  {!!} ; is-n= = λ k lt → {!!} } }

HNTotalOrder : IsTotalPreorder _n=_ _n≤_
HNTotalOrder = record {
     isPreorder = record {
              isEquivalence = n=IsEquivalence
            ; reflexive     = λ eq → record { ≤-map = =-map eq ; ≤-m = =-m eq ; is-n≤ = {!!} }
            ; trans         = trans1 }
    ; total = total
  } where
      open import Data.Sum.Base using (_⊎_)
      open _⊎_
      total : (x y : HyperNat ) → (x n≤ y) ⊎ (y n≤ x)
      total x y with <-cmpn x y
      ... | tri< a ¬b ¬c = inj₁ {!!}
      ... | tri≈ ¬a b ¬c = {!!}
      ... | tri> ¬a ¬b c = {!!}
      trans1 : {i j k : HyperNat} →  i n≤ j → j n≤ k → i n≤ k
      trans1 = {!!}

record n-finite (i : HyperNat ) : Set where
  field
     val : ℕ
     is-val : i n= h val

n-infinite :  (i : HyperNat ) → Set
n-infinite i = (j : ℕ ) → h j n≤ i

n-linear : HyperNat
n-linear i = i

n-linear-is-infnite : n-infinite n-linear
n-linear-is-infnite i = record { ≤-map = bid ℕ ; ≤-m = i ; is-n≤ = λ k lt → <to≤ lt }

¬-infinite-n-finite :  (i : HyperNat ) →  n-finite i → ¬ n-infinite i
¬-infinite-n-finite = {!!}

data HyperZ : Set where
   hz : HyperNat → HyperNat → HyperZ

hZ : ℕ → ℕ → HyperZ
hZ x y = hz (λ _ → x) (λ _ → y )

_z+_ : (i j : HyperZ ) → HyperZ
hz i i₁ z+ hz j j₁ = hz ( i n+ j ) (i₁ n+ j₁ )

_z*_ : (i j : HyperZ ) → HyperZ
hz i i₁ z* hz j j₁ = hz (λ k → i k * j k + i₁ k * j₁ k ) (λ k →  i k * j₁ k - i₁ k * j k )

--  x0 - y0 ≡ x1 - y1
--  x0 + y1 ≡ x1 + y0
--
_z=_ :  (i j : HyperZ ) → Set
_z=_ (hz x0 y0) (hz x1 y1)  = (x0 n+ y1) n= (x1 n+ y0)

_z≤_ :  (i j : HyperZ ) → Set
_z≤_ (hz x0 y0) (hz x1 y1)  = (x0 n+ y1) n≤ (x1 n+ y0)

_z<_ :  (i j : HyperZ ) → Set
_z<_ (hz x0 y0) (hz x1 y1)  = (x0 n+ y1) n< (x1 n+ y0)

<-cmpz  : Trichotomous {Level.zero}  _z=_ _z<_
<-cmpz (hz x0 y0) (hz x1 y1)  = <-cmpn (x0 n+ y1) (x1 n+ y0)

-z :  (i : HyperZ ) →  HyperZ
-z (hz x y) = hz y x

z-z=0 : (i : HyperZ ) → (i z+ (-z i)) z= hZ 0 0
z-z=0 = {!!}

z+infinite :  (i : HyperZ ) → Set
z+infinite i = (j : ℕ ) → hZ j 0 z≤ i

z-infinite :  (i : HyperZ ) → Set
z-infinite i = (j : ℕ ) → i z≤ hZ 0 j

import Axiom.Extensionality.Propositional
postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m

---    x*y    ...... 0 0 0 0 ...
---    x      ...... 0 0 1 0 1 ....
---    y      ...... 0 1 0 1 0 ....

HNnzero* : {x y : HyperNat } → ¬ ( x n= h 0 ) → ¬ ( y n= h 0  ) → ¬ ( (x n* y) n= h 0 )
HNnzero* {x} {y} nzx nzy xy0 = hn1 where
   hn2 : ( h 0 n< x ) → ( h 0 n< y  ) →  ¬ ( (x n* y) n= h 0 )
   hn2 0<x 0<y  xy0 = ⊥-elim ( nat-≡< (sym (is-n= xy0 (suc mxy) {!!} )) {!!}  ) where
       mxy : ℕ
       mxy = <-m 0<x ⊔ <-m 0<y ⊔ =-m xy0
   hn1 : ⊥
   hn1 with <-cmpn x (h 0)
   ... | tri≈ ¬a b ¬c = nzx b
   ... | tri< a ¬b ¬c = ⊥-elim ( ¬hn<0 a)
   hn1 | tri> ¬a ¬b c with <-cmpn y (h 0)
   ... | tri< a ¬b₁ ¬c = ⊥-elim ( ¬hn<0 a)
   ... | tri≈ ¬a₁ b ¬c = nzy b
   ... | tri> ¬a₁ ¬b₁ c₁ = hn2 c c₁ xy0

HZzero : HyperZ → Set
HZzero z = hZ 0 0 z= z

HZzero? : ( i : HyperZ ) → Dec (HZzero i)
HZzero? = {!!}

data HyperR : Set where
   hr :  HyperZ → (k : HyperNat ) → ((i : ℕ) → 0 < k i) → HyperR

HZnzero* : {x y : HyperZ } → ¬ ( HZzero x ) → ¬ ( HZzero y ) → ¬ ( HZzero (x z* y) )
HZnzero* {x} {y} nzx nzy nzx*y = {!!}

HRzero : HyperR → Set
HRzero (hr i j nz ) = HZzero i

R0 : HyperR
R0 = hr (hZ 0 0) (h 1) {!!}

record Rational : Set where
  field
     rp rm k : ℕ
     0<k : 0 < k

hR :  ℕ → ℕ → (k : HyperNat ) → ((i : ℕ) → 0 < k i) → HyperR
hR x y k ne = hr (hZ x y) k ne

rH : (r : Rational ) → HyperR
rH r =  hr (hZ (Rational.rp r) (Rational.rm r)) (h (Rational.k r)) {!!}

--
--  z0 / y0 = z1 / y1 ← z0 * y1 = z1 * y0
--
_h=_ :  (i j : HyperR ) → Set
hr z0 k0 ne0 h= hr z1 k1 ne1  = (z0 z* (hz k1 (h 0))) z= (z1 z* (hz k0 (h 0)))

_h≤_ :  (i j : HyperR ) → Set
hr z0 k0 ne0 h≤ hr z1 k1 ne1  = (z0 z* (hz k1 (h 0))) z≤ (z1 z* (hz k0 (h 0)))

_h<_ :  (i j : HyperR ) → Set
hr z0 k0 ne0 h< hr z1 k1 ne1  = (z0 z* (hz k1 (h 0))) z< (z1 z* (hz k0 (h 0)))

<-cmph  : Trichotomous {Level.zero}  _h=_ _h<_
<-cmph (hr z0 k0 ne0 ) ( hr z1 k1 ne1 ) = <-cmpz  (z0 z* (hz k1 (h 0)))  (z1 z* (hz k0 (h 0)))

_h*_ : (i j : HyperR) → HyperR
hr x k nz h* hr y k₁ nz₁ = hr ( x z* y ) ( k n* k₁ ) {!!}

_h+_ : (i j : HyperR) → HyperR
hr x k nz h+ hr y k₁ nz₁ = hr ( (x z* (hz k hzero)) z+  (y z* (hz k₁ hzero)) ) (k n* k₁) {!!}

-h : (i : HyperR) → HyperR
-h (hr x k nz) = hr (-z x) k nz

inifinitesimal-R : (inf : HyperR) → Set
inifinitesimal-R inf = ( r : Rational ) → R0 h< rH r → ( -h (rH r) h< inf ) ∧ ( inf h< rH r)

1/x : HyperR
1/x = hr (hZ 1 0) n-linear {!!}

1/x-is-inifinitesimal : inifinitesimal-R 1/x
1/x-is-inifinitesimal r 0<r = ⟪ {!!} , {!!} ⟫

HyperReal :  Set
HyperReal = ℕ  → HyperR

HR→HRl : HyperR → HyperReal
HR→HRl (hr (hz x y) k ne) k1 = hr (hz (λ k2 → (x k1)) (λ k2 → (x k1))) k ne

HRl→HR : HyperReal → HyperR
HRl→HR r = hr (hz (λ k → {!!}) (λ k → {!!}) ) factor {!!} where
   factor : HyperNat
   factor n = {!!}
   fne : (n : ℕ) → ¬ (factor n= h 0)
   fne = {!!}

_≈_ : (x y : HyperR ) → Set
x ≈ y = inifinitesimal-R (x h+ ( -h y ))

is-inifinitesimal : {x : HyperR } → inifinitesimal-R x → x ≈ R0
is-inifinitesimal {x} inf = {!!}

record Standard : Set where
   field
      standard          : HyperR → HyperR
      is-standard       : {x : HyperR } → x ≈ standard x
      standard-unique   : {x y : HyperR } →  x ≈ y → standard x ≡ standard y
      st-inifinitesimal : {x : HyperR } → inifinitesimal-R x → st x ≡ R0

postulate
   ST : Standard

open Standard

st :  HyperR → HyperR
st x = standard ST x

ext: agda

max_stars_repo_name: shinji-kono/HyperReal-in-agda

max_issues_repo_name: shinji-kono/HyperReal-in-agda

max_forks_repo_name: shinji-kono/HyperReal-in-agda


text:
module Data.Tuple.Equiv.Id where

import      Lvl
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Data.Tuple.Equiv
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Operator
open import Type

private variable ℓ ℓₒ₁ ℓₒ₂ : Lvl.Level
private variable A B : Type{ℓ}
private variable f g : A → B
private variable p : A ⨯ B

instance
  Tuple-Id-extensionality : Extensionality{A = A}{B = B}([≡]-equiv)
  Tuple-Id-extensionality = intro

Tuple-left-map : (Tuple.left(Tuple.map f g p) ≡ f(Tuple.left(p)))
Tuple-left-map = [≡]-intro

Tuple-right-map : (Tuple.right(Tuple.map f g p) ≡ g(Tuple.right(p)))
Tuple-right-map = [≡]-intro

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:
-- Syntax of a second-order language
module SOAS.Metatheory.Syntax {T : Set} where

open import SOAS.Families.Core {T}
open import SOAS.Families.Build

open import SOAS.Common
open import SOAS.Context
open import Categories.Object.Initial
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive
open import SOAS.Coalgebraic.Strength
open import SOAS.Abstract.ExpStrength
open import SOAS.Metatheory.MetaAlgebra

-- Data characterising a second-order syntax:
-- * a signature endofunctor ⅀
-- * coalgebraic and exponential strength
-- * initial (⅀,𝔛)-meta-algebra for each 𝔛
-- + an inductive metavariable constructor for convenience
record Syntax : Set₁ where
  field
    ⅀F    : Functor 𝔽amiliesₛ 𝔽amiliesₛ
    ⅀:CS  : CompatStrengths ⅀F
    𝕋:Init : (𝔛 : Familyₛ) → Initial (𝕄etaAlgebras ⅀F 𝔛)
    mvarᵢ  : {𝔛 : Familyₛ}{τ : T}{Π Γ : Ctx} (open Initial (𝕋:Init 𝔛))
          → 𝔛 τ Π → Sub (𝐶 ⊥) Π Γ → 𝐶 ⊥ τ Γ

  module _ {𝔛 : Familyₛ} where
    open Initial (𝕋:Init 𝔛)

  private
    variable
      α α₁ α₂ α₃ α₄ α₅ α₆ α₇ α₈ α₉ : T
      Γ Π Π₁ Π₂ Π₃ Π₄ Π₅ Π₆ Π₇ Π₈ Π₉  : Ctx
      𝔐 : MCtx
    Tm : MCtx → Familyₛ
    Tm 𝔐 = 𝐶 (Initial.⊥ (𝕋:Init ∥ 𝔐 ∥))

  -- Shorthands for metavariables associated with a metavariable environment
  infix 100 𝔞⟨_ 𝔟⟨_ 𝔠⟨_ 𝔡⟨_ 𝔢⟨_
  infix 100 ◌ᵃ⟨_ ◌ᵇ⟨_ ◌ᶜ⟨_ ◌ᵈ⟨_ ◌ᵉ⟨_

  𝔞⟨_ : Sub (Tm (⁅ Π ⊩ₙ α ⁆ 𝔐)) Π Γ → Tm (⁅ Π ⊩ₙ α ⁆ 𝔐) α Γ
  𝔞⟨ ε = mvarᵢ ↓ ε

  𝔟⟨_ : Sub (Tm (⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐)) Π Γ
      → Tm (⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐) α Γ
  𝔟⟨ ε = mvarᵢ (↑ ↓) ε

  𝔠⟨_ : Sub (Tm (⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐))  Π Γ
      → Tm (⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐) α Γ
  𝔠⟨ ε = mvarᵢ (↑ ↑ ↓) ε

  𝔡⟨_ : Sub (Tm (⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐)) Π Γ
      → Tm (⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐) α Γ
  𝔡⟨ ε = mvarᵢ (↑ ↑ ↑ ↓) ε
  𝔢⟨_ : Sub (Tm (⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐)) Π Γ
      → Tm (⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐) α Γ
  𝔢⟨ ε = mvarᵢ (↑ ↑ ↑ ↑ ↓) ε

  𝔣⟨_ : Sub (Tm (⁅ Π₅ ⊩ₙ α₅ ⁆ ⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐)) Π Γ
      → Tm (⁅ Π₅ ⊩ₙ α₅ ⁆ ⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐) α Γ
  𝔣⟨ ε = mvarᵢ (↑ ↑ ↑ ↑ ↑ ↓) ε

  𝔤⟨_ : Sub (Tm (⁅ Π₆ ⊩ₙ α₆ ⁆ ⁅ Π₅ ⊩ₙ α₅ ⁆ ⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐)) Π Γ
      → Tm (⁅ Π₆ ⊩ₙ α₆ ⁆ ⁅ Π₅ ⊩ₙ α₅ ⁆ ⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐) α Γ
  𝔤⟨ ε = mvarᵢ (↑ ↑ ↑ ↑ ↑ ↑ ↓) ε

  𝔥⟨_ : Sub (Tm (⁅ Π₇ ⊩ₙ α₇ ⁆ ⁅ Π₆ ⊩ₙ α₆ ⁆ ⁅ Π₅ ⊩ₙ α₅ ⁆ ⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐)) Π Γ
      → Tm (⁅ Π₇ ⊩ₙ α₇ ⁆ ⁅ Π₆ ⊩ₙ α₆ ⁆ ⁅ Π₅ ⊩ₙ α₅ ⁆ ⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐) α Γ
  𝔥⟨ ε = mvarᵢ (↑ ↑ ↑ ↑ ↑ ↑ ↑ ↓) ε

  𝔦⟨_ : Sub (Tm (⁅ Π₈ ⊩ₙ α₈ ⁆ ⁅ Π₇ ⊩ₙ α₇ ⁆ ⁅ Π₆ ⊩ₙ α₆ ⁆ ⁅ Π₅ ⊩ₙ α₅ ⁆ ⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐)) Π Γ
      → Tm (⁅ Π₈ ⊩ₙ α₈ ⁆ ⁅ Π₇ ⊩ₙ α₇ ⁆ ⁅ Π₆ ⊩ₙ α₆ ⁆ ⁅ Π₅ ⊩ₙ α₅ ⁆ ⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐) α Γ
  𝔦⟨ ε = mvarᵢ (↑ ↑ ↑ ↑ ↑ ↑ ↑ ↑ ↓) ε

  𝔧⟨_ : Sub (Tm (⁅ Π₉ ⊩ₙ α₉ ⁆ ⁅ Π₈ ⊩ₙ α₈ ⁆ ⁅ Π₇ ⊩ₙ α₇ ⁆ ⁅ Π₆ ⊩ₙ α₆ ⁆ ⁅ Π₅ ⊩ₙ α₅ ⁆ ⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐)) Π Γ
      → Tm (⁅ Π₉ ⊩ₙ α₉ ⁆ ⁅ Π₈ ⊩ₙ α₈ ⁆ ⁅ Π₇ ⊩ₙ α₇ ⁆ ⁅ Π₆ ⊩ₙ α₆ ⁆ ⁅ Π₅ ⊩ₙ α₅ ⁆ ⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ Π ⊩ₙ α ⁆ 𝔐) α Γ
  𝔧⟨ ε = mvarᵢ (↑ ↑ ↑ ↑ ↑ ↑ ↑ ↑ ↑ ↓) ε

  -- Shorthands for metavariables with an empty metavariable environment
  𝔞 : Tm (⁅ α ⁆ 𝔐) α Γ
  𝔞 = 𝔞⟨ •
  𝔟 : Tm (⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ α ⁆ 𝔐) α Γ
  𝔟 = 𝔟⟨ •
  𝔠 : Tm (⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ α ⁆ 𝔐) α Γ
  𝔠 = 𝔠⟨ •
  𝔡 : Tm (⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ α ⁆ 𝔐) α Γ
  𝔡 = 𝔡⟨ •
  𝔢 : Tm (⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ α ⁆ 𝔐) α Γ
  𝔢 = 𝔢⟨ •

  𝔣 : Tm (⁅ Π₅ ⊩ₙ α₅ ⁆ ⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅ α ⁆ 𝔐) α Γ
  𝔣 = 𝔣⟨ •

  𝔤 : Tm (⁅ Π₆ ⊩ₙ α₆ ⁆ ⁅ Π₅ ⊩ₙ α₅ ⁆ ⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅  α ⁆ 𝔐) α Γ
  𝔤 = 𝔤⟨ •

  𝔥 : Tm (⁅ Π₇ ⊩ₙ α₇ ⁆ ⁅ Π₆ ⊩ₙ α₆ ⁆ ⁅ Π₅ ⊩ₙ α₅ ⁆ ⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅  α ⁆ 𝔐) α Γ
  𝔥 = 𝔥⟨ •

  𝔦 :  Tm (⁅ Π₈ ⊩ₙ α₈ ⁆ ⁅ Π₇ ⊩ₙ α₇ ⁆ ⁅ Π₆ ⊩ₙ α₆ ⁆ ⁅ Π₅ ⊩ₙ α₅ ⁆ ⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅  α ⁆ 𝔐) α Γ
  𝔦 = 𝔦⟨ •

  𝔧 :  Tm (⁅ Π₉ ⊩ₙ α₉ ⁆ ⁅ Π₈ ⊩ₙ α₈ ⁆ ⁅ Π₇ ⊩ₙ α₇ ⁆ ⁅ Π₆ ⊩ₙ α₆ ⁆ ⁅ Π₅ ⊩ₙ α₅ ⁆ ⁅ Π₄ ⊩ₙ α₄ ⁆ ⁅ Π₃ ⊩ₙ α₃ ⁆ ⁅ Π₂ ⊩ₙ α₂ ⁆ ⁅ Π₁ ⊩ₙ α₁ ⁆ ⁅  α ⁆ 𝔐) α Γ
  𝔧 = 𝔧⟨ •

  -- Synonyms for holes
  ◌ᵃ = 𝔞 ; ◌ᵇ = 𝔟 ; ◌ᶜ = 𝔠 ; ◌ᵈ = 𝔡 ; ◌ᵉ = 𝔢
  ◌ᵃ⟨_ = 𝔞⟨_ ; ◌ᵇ⟨_ = 𝔟⟨_ ; ◌ᶜ⟨_ = 𝔠⟨_ ; ◌ᵈ⟨_ = 𝔡⟨_ ; ◌ᵉ⟨_ = 𝔢⟨_

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
{-# OPTIONS --inversion-max-depth=10 #-}

open import Agda.Builtin.Nat

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

F : Nat → Set
F zero    = Nat
F (suc n) = Nat × F n

f : (n : Nat) → F n
f zero    = zero
f (suc n) = n , f n

mutual

  n : Nat
  n = _

  test : F n
  test = f (suc n)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

-- Nils' idea about databases in the Agda mailing list.
-- http://thread.gmane.org/gmane.comp.lang.agda/2911/focus=2917

module DataBase where

infixr 7 _,_ _,′_
infixr 5 _∧_

data _∧_ (A B : Set) : Set where
  _,_ : A → B → A ∧ B

_,′_ : ∀ {A B} → A → B → A ∧ B
_,′_ = _,_

postulate
  P Q R S : Set
  h₁      : P → Q
  h₂      : Q → R
  h₃      : R → S

postulate thm₁ : P → S
{-# ATP prove thm₁ h₁ h₂ h₃ #-}

db = h₁ ,′ h₂ ,′ h₃

postulate thm₂ : P → S
{-# ATP prove thm₂ db #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
--------------------------------------------------------------------------------
-- White or blacklisting of characters
--------------------------------------------------------------------------------

module Parse.MultiChar where

import Data.List.NonEmpty as NE
open import Data.String hiding (show)

open import Prelude

-- TODO: Groups of characters, such as digits or lower case letters
MultiCharGroup : Set
MultiCharGroup = ⊥

matchCharGroup : MultiCharGroup → Char → Bool
matchCharGroup ()

data CharMatcher : Set where
  Single : Char → CharMatcher
  Group  : MultiCharGroup → CharMatcher

instance
  CharMatcher-Show : Show CharMatcher
  CharMatcher-Show = record { show = helper }
    where
      helper : CharMatcher → String
      helper (Single c) = fromChar c

parseCharMatcher : String → Maybe CharMatcher
parseCharMatcher s with uncons s
... | just (c , "") = just (Single c)
... | _             = nothing

matchCharMatcher : CharMatcher → Char → Bool
matchCharMatcher (Single x) c = x ≣ c
matchCharMatcher (Group  g) c = matchCharGroup g c

record MultiChar : Set where
  field
    matches : List CharMatcher
    negated : Bool

instance
  MultiChar-Show : Show MultiChar
  MultiChar-Show = record { show = helper }
    where
      helper : MultiChar → String
      helper m = (if negated then "!" else "") + show matches
        where open MultiChar m

parseMultiChar : Bool → List String → MultiChar
parseMultiChar b l = record { matches = mapMaybe parseCharMatcher l ; negated = b }

parseMultiCharNE : Bool → NE.List⁺ String → MultiChar
parseMultiCharNE b l = parseMultiChar b (NE.toList l)

matchMulti : MultiChar → Char → Bool
matchMulti m c = negated xor (or $ map (flip matchCharMatcher c) matches)
  where open MultiChar m

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
module #4 where

open import Data.Nat
open import Data.Product

{-
Exercise 1.4. Assuming as given only the iterator for natural numbers

iter : ∏ C → (C → C) → N → C
      C:U

with the defining equations

        iter(C, c0, cs, 0) :≡ c0
  iter(C, c0, cs, succ(n)) :≡ cs(iter(C, c0, cs, n)),

derive a function having the type of the recursor recN. Show that the defining equations of the
recursor hold propositionally for this function, using the induction principle for N.
-}

iter : ∀{k}{C : Set k} → C → (C → C) → ℕ → C
iter c0 cs zero = c0
iter c0 cs (suc n) = cs (iter c0 cs n)

ind-ℕ : ∀{k}{C : ℕ → Set k} → C zero → ((n : ℕ) → C n → C (suc n)) → (n : ℕ) → C n
ind-ℕ c0 cs zero = c0
ind-ℕ c0 cs (suc n) = cs n (ind-ℕ c0 cs n)

rec : ∀{k}{C : Set k} → C → (ℕ → C → C) → ℕ → C
rec {i}{C} c0 f n = proj₂ (iter z (λ p → (suc (proj₁ p) , f (proj₁ p) (proj₂ p))) n)
  where
    z : ℕ × C
    z = (0 , c0)

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An example showing how the Debug.Trace module can be used
------------------------------------------------------------------------

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

module README.Debug.Trace where

------------------------------------------------------------------------
-- Sometimes compiled code can contain bugs.

-- Whether caused by the compiler or present in the source code already, they
-- can be hard to track. A primitive debugging technique is to strategically
-- insert calls to tracing functions which will display their String argument
-- upon evaluation.

open import Data.String.Base using (_++_)
open import Debug.Trace

-- We can for instance add tracing messages to make sure an invariant is
-- respected or check in which order evaluation takes place in the backend
-- (which can inform our decision to use, or not, strictness primitives).

-- In the following example, we define a division operation on natural numbers
-- using the original dividend as the termination measure. We:

-- 1. check in the base case that when the fuel runs out then the updated dividend
--    is already zero.

-- 2. wrap the calls to _∸_ and go in respective calls to trace to see when all
--    of these thunks are forced: are we building a big thunk in go's second
--    argument or evaluating it as we go?

open import Data.Maybe.Base
open import Data.Nat.Base
open import Data.Nat.Show using (show)

div : ℕ → ℕ → Maybe ℕ
div m zero = nothing
div m n    = just (go m m) where

  -- invariants: m ≤ fuel
  -- result : m / n
  go : (fuel : ℕ) (m : ℕ) → ℕ
  go zero       m = trace ("Invariant: " ++ show m ++ " should be zero.") zero
  go (suc fuel) m =
    let m' = trace ("Thunk for step " ++ show fuel ++ " forced") (m ∸ n) in
    trace ("Recursive call for step " ++ show fuel) (suc (go fuel m'))

-- To observe the behaviour of this code, we need to compile it and run it.
-- To run it, we need a main function. We define a very basic one: run div,
-- and display its result if the run was successful.

-- We add two calls to trace to see when div is evaluated and when the returned
-- number is forced (by a call to show).

open import IO

main =
  let r = trace "Call to div" (div 4 2)
      j = λ n → trace "Forcing the result wrapped in just." (putStrLn (show n)) in
  run (maybe′ j (return _) r)

-- We get the following trace where we can see that checking that the
-- maybe-solution is just-headed does not force the natural number. Once forced,
-- we observe that we indeed build a big thunk on go's second argument (all the
-- recursive calls happen first and then we force the thunks one by one).

-- Call to div
-- Forcing the result wrapped in just.
-- Recursive call for step 3
-- Recursive call for step 2
-- Recursive call for step 1
-- Recursive call for step 0
-- Thunk for step 0 forced
-- Thunk for step 1 forced
-- Thunk for step 2 forced
-- Thunk for step 3 forced
-- Invariant: 0 should be zero.
-- 4

-- We also notice that the result is incorrect: 4/2 is 2 and not 4. We quickly
-- notice that (div m (suc n)) will perform m recursive calls no matter what.
-- And at each call it will put add 1. We can fix this bug by adding a new first
-- equation to go:

-- go fuel zero = zero

-- Running the example again we observe that because we now need to check
-- whether go's second argument is zero, the function is more strict: we see
-- that recursive calls and thunk forcings are interleaved.

-- Call to div
-- Forcing the result wrapped in just.
-- Recursive call for step 3
-- Thunk for step 3 forced
-- Recursive call for step 2
-- Thunk for step 2 forced
-- 2


text:
open import Nat
open import Prelude
open import dynamics-core

open import lemmas-gcomplete

module lemmas-complete where
  -- no term is both complete and indeterminate
  lem-ind-comp : ∀{d} → d dcomplete → d indet → ⊥
  lem-ind-comp DCNum ()
  lem-ind-comp (DCPlus comp comp₁) (IPlus1 ind fin) = lem-ind-comp comp ind
  lem-ind-comp (DCPlus comp comp₁) (IPlus2 fin ind) = lem-ind-comp comp₁ ind
  lem-ind-comp DCVar ()
  lem-ind-comp (DCLam comp x₁) ()
  lem-ind-comp (DCAp comp comp₁) (IAp x ind x₁) = lem-ind-comp comp ind
  lem-ind-comp (DCCast comp x x₁) (ICastArr x₂ ind) = lem-ind-comp comp ind
  lem-ind-comp (DCCast comp x x₁) (ICastGroundHole x₂ ind) = lem-ind-comp comp ind
  lem-ind-comp (DCCast comp x x₁) (ICastHoleGround x₂ ind x₃) = lem-ind-comp comp ind
  lem-ind-comp (DCInl x comp) (IInl ind) = lem-ind-comp comp ind
  lem-ind-comp (DCInr x comp) (IInr ind) = lem-ind-comp comp ind
  lem-ind-comp (DCCase comp comp₁ comp₂) (ICase x x₁ x₂ ind) = lem-ind-comp comp ind
  lem-ind-comp (DCCast comp x x₁) (ICastSum x₂ ind) = lem-ind-comp comp ind
  lem-ind-comp (DCPair comp comp₁) (IPair1 ind x) = lem-ind-comp comp ind
  lem-ind-comp (DCPair comp comp₁) (IPair2 x ind) = lem-ind-comp comp₁ ind
  lem-ind-comp (DCFst comp) (IFst x x₁ ind) = lem-ind-comp comp ind
  lem-ind-comp (DCSnd comp) (ISnd x x₁ ind) = lem-ind-comp comp ind
  lem-ind-comp (DCCast comp x x₁) (ICastProd x₂ ind) = lem-ind-comp comp ind

  -- complete types that are consistent are equal
  complete-consistency : ∀{τ1 τ2} → τ1 ~ τ2 → τ1 tcomplete → τ2 tcomplete → τ1 == τ2
  complete-consistency TCRefl TCNum comp2 = refl
  complete-consistency TCRefl (TCArr comp1 comp2) comp3 = refl
  complete-consistency TCRefl (TCSum tc1 tc3) comp2 = refl
  complete-consistency TCHole1 comp1 ()
  complete-consistency (TCArr consis consis₁) (TCArr comp1 comp2) (TCArr comp3 comp4)
   with complete-consistency consis comp1 comp3 | complete-consistency consis₁ comp2 comp4
  ... | refl | refl = refl
  complete-consistency (TCSum consis consis₁) (TCSum comp1 comp2) (TCSum comp3 comp4)
    with complete-consistency consis comp1 comp3 | complete-consistency consis₁ comp2 comp4
  ... | refl | refl = refl
  complete-consistency TCRefl (TCProd comp comp₁) comp2 = refl
  complete-consistency TCHole2 () comp2
  complete-consistency (TCProd consis consis₁) (TCProd comp1 comp2) (TCProd comp3 comp4)
    with complete-consistency consis comp1 comp3 | complete-consistency consis₁ comp2 comp4
  ... | refl | refl = refl

  -- a well typed complete term is assigned a complete type
  complete-ta : ∀{Γ Δ d τ} → (Γ gcomplete) →
                             (Δ , Γ ⊢ d :: τ) →
                             d dcomplete →
                             τ tcomplete
  complete-ta gc TANum comp = TCNum
  complete-ta gc (TAPlus wt wt₁) comp = TCNum
  complete-ta gc (TAVar x₁) DCVar = gc _ _ x₁
  complete-ta gc (TALam a wt) (DCLam comp x₁) = TCArr x₁ (complete-ta (gcomp-extend gc x₁ a ) wt comp)
  complete-ta gc (TAAp wt wt₁) (DCAp comp comp₁)
    with complete-ta gc wt comp
  ... | TCArr qq qq₁ = qq₁
  complete-ta gc (TAEHole x x₁) ()
  complete-ta gc (TANEHole x wt x₁) ()
  complete-ta gc (TACast wt x) (DCCast comp x₁ x₂) = x₂
  complete-ta gc (TAFailedCast wt x x₁ x₂) ()
  complete-ta gc (TAInl wt) (DCInl x comp) = TCSum (complete-ta gc wt comp) x
  complete-ta gc (TAInr wt) (DCInr x comp) = TCSum x (complete-ta gc wt comp)
  complete-ta gc (TACase wt apt₁ wt₁ apt₂ wt₂) (DCCase comp comp₁ comp₂)
    with complete-ta gc wt comp
  ... | TCSum τc1 τc2 =  complete-ta (gcomp-extend gc τc1 apt₁) wt₁ comp₁
  complete-ta gc (TAPair wt wt₁) (DCPair comp comp₁) = TCProd (complete-ta gc wt comp) (complete-ta gc wt₁ comp₁)
  complete-ta gc (TAFst wt) (DCFst comp)
    with complete-ta gc wt comp
  ... | TCProd τc1 τc2 = τc1
  complete-ta gc (TASnd wt) (DCSnd comp)
    with complete-ta gc wt comp
  ... | TCProd τc1 τc2 = τc2

  -- a well typed term synthesizes a complete type
  comp-synth : ∀{Γ e τ} →
               Γ gcomplete →
               e ecomplete →
               Γ ⊢ e => τ →
               τ tcomplete
  comp-synth gc ec SNum = TCNum
  comp-synth gc ec (SPlus x x₁) = TCNum
  comp-synth gc (ECAsc x ec) (SAsc x₁) = x
  comp-synth gc ec (SVar x) = gc _ _ x
  comp-synth gc (ECAp ec ec₁) (SAp wt MAHole x₁) with comp-synth gc ec wt
  ... | ()
  comp-synth gc (ECAp ec ec₁) (SAp wt MAArr x₁) with comp-synth gc ec wt
  comp-synth gc (ECAp ec ec₁) (SAp wt MAArr x₁) | TCArr qq qq₁ = qq₁
  comp-synth gc () SEHole
  comp-synth gc () (SNEHole wt)
  comp-synth gc (ECLam2 ec x₁) (SLam x₂ wt) = TCArr x₁ (comp-synth (gcomp-extend gc x₁ x₂) ec wt)
  comp-synth gc (ECPair ec ec₁) (SPair wt wt₁)
    with comp-synth gc ec wt | comp-synth gc ec₁ wt₁
  ... | τc1 | τc2 = TCProd τc1 τc2
  comp-synth gc (ECFst ec) (SFst wt MPHole) with comp-synth gc ec wt
  ... | ()
  comp-synth gc (ECFst ec) (SFst wt MPProd) with comp-synth gc ec wt
  ... | TCProd τc1 τc2 = τc1
  comp-synth gc (ECSnd ec) (SSnd wt MPHole) with comp-synth gc ec wt
  ... | ()
  comp-synth gc (ECSnd ec) (SSnd wt MPProd) with comp-synth gc ec wt
  ... | TCProd τc1 τc2 = τc2

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
{-# OPTIONS --cubical #-}
module Issue4365 where

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.String

postulate
  s : String

_ : primTransp (\ i → String) i0 s ≡ s
_ = \ _ → s


text:
{-

An simpler definition of truncation ∥ A ∥ n from n ≥ -1

Note that this uses the HoTT book's indexing, so it will be off
 from `∥_∥_` in HITs.Truncation.Base by -2

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Truncation.FromNegOne.Base where

open import Cubical.Data.NatMinusOne renaming (suc₋₁ to suc)
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.HITs.Sn

data  ∥_∥_ {ℓ} (A : Type ℓ) (n : ℕ₋₁) : Type ℓ where
  ∣_∣ : A  → ∥ A ∥ n
  hub : (f : S (suc n) → ∥ A ∥ n) → ∥ A ∥ n
  spoke : (f : S (suc n) → ∥ A ∥ n) (x : S (suc n)) → hub f ≡ f x


text:
module CantOpenConstructorsFromRecordModule where

module Datatypes where
  record Foo : Set where
    constructor foo

ok : Datatypes.Foo
ok = Datatypes.foo

open Datatypes.Foo

bad : Datatypes.Foo
bad = foo

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- ASR (29 September 2014). Adapted from the example in issue 1269.

-- Case: quote η-reduced and quoteTerm η-reduced.

open import Common.Equality
open import Common.Level
open import Common.Prelude renaming (Nat to ℕ)
open import Common.Product
open import Common.Reflection

data Even  : ℕ → Set where
  isEven0  : Even 0
  isEven+2 : ∀ {n} → Even n → Even (suc (suc n))

pattern expected =
  def (quote Σ)
      ( arg (argInfo hidden relevant) (def (quote Common.Level.lzero) []) ∷
        arg (argInfo hidden relevant) (def (quote Common.Level.lzero) []) ∷
        arg (argInfo visible relevant) (def (quote ℕ) []) ∷
        arg (argInfo visible relevant) (def (quote Even) []) ∷
        [] )

isExpected : Term → Bool
isExpected expected = true
isExpected _        = false

`_ : Bool → Term
` true  = con (quote true) []
` false = con (quote false) []

macro
  checkExpectedType : QName → Tactic
  checkExpectedType i hole =
    bindTC (getType i)   λ t →
    bindTC (normalise t) λ t → give (` isExpected t) hole

input0 : ∃ Even
input0 = 0 , isEven0

input1 : ∃ (λ n → Even n)
input1 = 0 , isEven0

quote0 : Bool
quote0 = checkExpectedType input0

quote1 : Bool
quote1 = checkExpectedType input1

ok0 : quote0 ≡ true
ok0 = refl

ok1 : quote1 ≡ true
ok1 = refl

------------------------------------------------------------------------------
-- For debugging purpose

quotedTerm0 : Term
quotedTerm0 = quoteTerm (∃ Even)

quotedTerm1 : Term
quotedTerm1 = quoteTerm (∃ (λ n → Even n))

b : quotedTerm0 ≡ expected
b = refl

c : quotedTerm1 ≡ expected
c = refl


text:
-- Author: David Darais
--
-- This is a dependent de Bruijn encoding of STLC with proofs for
-- progress and preservation. This file has zero dependencies and is
-- 100% self-contained.
--
-- Because there is only a notion of well-typed terms (non-well-typed
-- terms do not exist), preservation is merely by observation that
-- substitution (i.e., cut) can be defined.
--
-- A small-step evaluation semantics is defined after the definition of cut.
--
-- Progress is proved w.r.t. the evaluation semantics.
--
-- Some ideas for extensions or homeworks are given at the end.
--
-- A few helper definitions are required.
-- * Basic Agda constructions (like booleans, products, dependent sums,
--   and lists) are defined first in a Prelude module which is
--   immediately opened.
-- * Binders (x : τ ∈ Γ) are proofs that the element τ is contained in
--   the list of types Γ. Helper functions for weakening and
--   introducing variables into contexts which are reusable are
--   defined in the Prelude. Helpers for weakening terms are defined
--   below. Some of the non-general helpers (like cut[∈]) could be
--   defined in a generic way to be reusable, but I decided against
--   this to keep things simple.

module Darais where

open import Agda.Primitive using (_⊔_)

module Prelude where

  infixr 3 ∃𝑠𝑡
  infixl 5 _∨_
  infix 10 _∈_
  infixl 15 _⧺_
  infixl 15 _⊟_
  infixl 15 _∾_
  infixr 20 _∷_

  data 𝔹 : Set where
    T : 𝔹
    F : 𝔹

  data _∨_ {ℓ₁ ℓ₂} (A : Set ℓ₁) (B : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
    Inl : A → A ∨ B
    Inr : B → A ∨ B

  syntax ∃𝑠𝑡 A (λ x → B) = ∃ x ⦂ A 𝑠𝑡 B
  data ∃𝑠𝑡 {ℓ₁ ℓ₂} (A : Set ℓ₁) (B : A → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
    ⟨∃_,_⟩ : ∀ (x : A) → B x → ∃ x ⦂ A 𝑠𝑡 B x

  data ⟬_⟭ {ℓ} (A : Set ℓ) : Set ℓ where
    [] : ⟬ A ⟭
    _∷_ : A → ⟬ A ⟭ → ⟬ A ⟭

  _⧺_ : ∀ {ℓ} {A : Set ℓ} → ⟬ A ⟭ → ⟬ A ⟭ → ⟬ A ⟭
  [] ⧺ ys = ys
  x ∷ xs ⧺ ys = x ∷ (xs ⧺ ys)

  _∾_ : ∀ {ℓ} {A : Set ℓ} → ⟬ A ⟭ → ⟬ A ⟭ → ⟬ A ⟭
  [] ∾ ys = ys
  (x ∷ xs) ∾ ys = xs ∾ x ∷ ys

  data _∈_ {ℓ} {A : Set ℓ} (x : A) : ∀ (xs : ⟬ A ⟭) → Set ℓ where
    Z : ∀ {xs} → x ∈ x ∷ xs
    S : ∀ {x′ xs} → x ∈ xs → x ∈ x′ ∷ xs

  _⊟_ : ∀ {ℓ} {A : Set ℓ} (xs : ⟬ A ⟭) {x} → x ∈ xs → ⟬ A ⟭
  x ∷ xs ⊟ Z = xs
  x ∷ xs ⊟ S ε = x ∷ (xs ⊟ ε)

  wk[∈] : ∀ {ℓ} {A : Set ℓ} {xs : ⟬ A ⟭} {x : A} xs′ → x ∈ xs → x ∈ xs′ ∾ xs
  wk[∈] [] x = x
  wk[∈] (x′ ∷ xs) x = wk[∈] xs (S x)

  i[∈][_] : ∀ {ℓ} {A : Set ℓ} {xs : ⟬ A ⟭} {x x′ : A} (ε′ : x′ ∈ xs) → x ∈ xs ⊟ ε′ → x ∈ xs
  i[∈][ Z ] x = S x
  i[∈][ S ε′ ] Z = Z
  i[∈][ S ε′ ] (S x) = S (i[∈][ ε′ ] x)

open Prelude

-- ============================ --
-- Simply Typed Lambda Calculus --
-- ============================ --

-- A dependent de Bruijn encoding
-- Or, the dynamic semantics of natural deduction as seen through Curry-Howard

-- types --

data type : Set where
  ⟨𝔹⟩ : type
  _⟨→⟩_ : type → type → type

-- terms --

infix 10 _⊢_
data _⊢_ : ∀ (Γ : ⟬ type ⟭) (τ : type) → Set where
  ⟨𝔹⟩ : ∀ {Γ}
    (b : 𝔹)
    → Γ ⊢ ⟨𝔹⟩
  ⟨if⟩_❴_❵❴_❵ : ∀ {Γ τ}
    (e₁ : Γ ⊢ ⟨𝔹⟩)
    (e₂ : Γ ⊢ τ)
    (e₃ : Γ ⊢ τ)
    → Γ ⊢ τ
  Var : ∀ {Γ τ}
    (x : τ ∈ Γ)
    → Γ ⊢ τ
  ⟨λ⟩ : ∀ {Γ τ₁ τ₂}
    (e : τ₁ ∷ Γ ⊢ τ₂)
    → Γ ⊢ τ₁ ⟨→⟩ τ₂
  _⟨⋅⟩_ : ∀ {Γ τ₁ τ₂}
    (e₁ : Γ ⊢ τ₁ ⟨→⟩ τ₂)
    (e₂ : Γ ⊢ τ₁)
    → Γ ⊢ τ₂

-- introducing a new variable to the context --

i[⊢][_] : ∀ {Γ τ τ′} (x′ : τ′ ∈ Γ) → Γ ⊟ x′ ⊢ τ → Γ ⊢ τ
i[⊢][ x′ ] (⟨𝔹⟩ b) = ⟨𝔹⟩ b
i[⊢][ x′ ] ⟨if⟩ e₁ ❴ e₂ ❵❴ e₃ ❵ = ⟨if⟩ i[⊢][ x′ ] e₁ ❴ i[⊢][ x′ ] e₂ ❵❴ i[⊢][ x′ ] e₃ ❵
i[⊢][ x′ ] (Var x) = Var (i[∈][ x′ ] x)
i[⊢][ x′ ] (⟨λ⟩ e) = ⟨λ⟩ (i[⊢][ S x′ ] e)
i[⊢][ x′ ] (e₁ ⟨⋅⟩ e₂) = i[⊢][ x′ ] e₁ ⟨⋅⟩ i[⊢][ x′ ] e₂

i[⊢] : ∀ {Γ τ τ′} → Γ ⊢ τ → τ′ ∷ Γ ⊢ τ
i[⊢] = i[⊢][ Z ]

-- substitution for variables --

cut[∈]<_>[_] : ∀ {Γ τ₁ τ₂} (x : τ₁ ∈ Γ) Γ′ → Γ′ ∾ (Γ ⊟ x) ⊢ τ₁ → τ₂ ∈ Γ → Γ′ ∾ (Γ ⊟ x) ⊢ τ₂
cut[∈]< Z >[ Γ′ ] e Z = e
cut[∈]< Z >[ Γ′ ] e (S y) = Var (wk[∈] Γ′ y)
cut[∈]< S x′ >[ Γ′ ] e Z = Var (wk[∈] Γ′ Z)
cut[∈]< S x′ >[ Γ′ ] e (S x) = cut[∈]< x′ >[ _ ∷ Γ′ ] e x

cut[∈]<_> : ∀ {Γ τ₁ τ₂} (x : τ₁ ∈ Γ) → Γ ⊟ x ⊢ τ₁ → τ₂ ∈ Γ → Γ ⊟ x ⊢ τ₂
cut[∈]< x′ > = cut[∈]< x′ >[ [] ]

-- substitution for terms --

cut[⊢][_] : ∀ {Γ τ₁ τ₂} (x : τ₁ ∈ Γ) → Γ ⊟ x ⊢ τ₁ → Γ ⊢ τ₂ → Γ ⊟ x ⊢ τ₂
cut[⊢][ x′ ] e′ (⟨𝔹⟩ b) = ⟨𝔹⟩ b
cut[⊢][ x′ ] e′ ⟨if⟩ e₁ ❴ e₂ ❵❴ e₃ ❵ = ⟨if⟩ cut[⊢][ x′ ] e′ e₁ ❴ cut[⊢][ x′ ] e′ e₂ ❵❴ cut[⊢][ x′ ] e′ e₃ ❵
cut[⊢][ x′ ] e′ (Var x) = cut[∈]< x′ > e′ x
cut[⊢][ x′ ] e′ (⟨λ⟩ e) = ⟨λ⟩ (cut[⊢][ S x′ ] (i[⊢] e′) e)
cut[⊢][ x′ ] e′ (e₁ ⟨⋅⟩ e₂) = cut[⊢][ x′ ] e′ e₁ ⟨⋅⟩ cut[⊢][ x′ ] e′ e₂

cut[⊢] : ∀ {Γ τ₁ τ₂} → Γ ⊢ τ₁ → τ₁ ∷ Γ ⊢ τ₂ → Γ ⊢ τ₂
cut[⊢] = cut[⊢][ Z ]

-- values --

data value {Γ} : ∀ {τ} → Γ ⊢ τ → Set where
  ⟨𝔹⟩ : ∀ b → value (⟨𝔹⟩ b)
  ⟨λ⟩ : ∀ {τ τ′} (e : τ′ ∷ Γ ⊢ τ) → value (⟨λ⟩ e)

-- CBV evaluation for terms --
-- (borrowing some notation and style from Wadler: https://wenkokke.github.io/sf/Stlc)

infix 10 _↝_
data _↝_ {Γ τ} : Γ ⊢ τ → Γ ⊢ τ → Set where
  ξ⋅₁ : ∀ {τ′} {e₁ e₁′ : Γ ⊢ τ′ ⟨→⟩ τ} {e₂ : Γ ⊢ τ′}
    → e₁ ↝ e₁′
    → e₁ ⟨⋅⟩ e₂ ↝ e₁′ ⟨⋅⟩ e₂
  ξ⋅₂ : ∀ {τ′} {e₁ : Γ ⊢ τ′ ⟨→⟩ τ} {e₂ e₂′ : Γ ⊢ τ′}
    → value e₁
    → e₂ ↝ e₂′
    → e₁ ⟨⋅⟩ e₂ ↝ e₁ ⟨⋅⟩ e₂′
  βλ : ∀ {τ′} {e₁ : τ′ ∷ Γ ⊢ τ} {e₂ : Γ ⊢ τ′}
    → value e₂
    → ⟨λ⟩ e₁ ⟨⋅⟩ e₂ ↝ cut[⊢] e₂ e₁
  ξif : ∀ {e₁ e₁′ : Γ ⊢ ⟨𝔹⟩} {e₂ e₃ : Γ ⊢ τ}
    → e₁ ↝ e₁′
    → ⟨if⟩ e₁ ❴ e₂ ❵❴ e₃ ❵ ↝ ⟨if⟩ e₁′ ❴ e₂ ❵❴ e₃ ❵
  ξif-T : ∀ {e₂ e₃ : Γ ⊢ τ}
    → ⟨if⟩ ⟨𝔹⟩ T ❴ e₂ ❵❴ e₃ ❵ ↝ e₂
  ξif-F : ∀ {e₂ e₃ : Γ ⊢ τ}
    → ⟨if⟩ ⟨𝔹⟩ F ❴ e₂ ❵❴ e₃ ❵ ↝ e₃

-- progress --

progress : ∀ {τ} (e : [] ⊢ τ) → value e ∨ (∃ e′ ⦂ [] ⊢ τ 𝑠𝑡 e ↝ e′)
progress (⟨𝔹⟩ b) = Inl (⟨𝔹⟩ b)
progress ⟨if⟩ e ❴ e₁ ❵❴ e₂ ❵ with progress e
… | Inl (⟨𝔹⟩ T) = Inr ⟨∃ e₁ , ξif-T ⟩
… | Inl (⟨𝔹⟩ F) = Inr ⟨∃ e₂ , ξif-F ⟩
… | Inr ⟨∃ e′ , ε ⟩ = Inr ⟨∃ ⟨if⟩ e′ ❴ e₁ ❵❴ e₂ ❵ , ξif ε ⟩
progress (Var ())
progress (⟨λ⟩ e) = Inl (⟨λ⟩ e)
progress (e₁ ⟨⋅⟩ e₂) with progress e₁
… | Inr ⟨∃ e₁′ , ε ⟩ = Inr ⟨∃ e₁′ ⟨⋅⟩ e₂ , ξ⋅₁ ε ⟩
… | Inl (⟨λ⟩ e) with progress e₂
… | Inl x = Inr ⟨∃ cut[⊢] e₂ e , βλ x ⟩
… | Inr ⟨∃ e₂′ , ε ⟩ = Inr ⟨∃ e₁ ⟨⋅⟩ e₂′ , ξ⋅₂ (⟨λ⟩ e) ε ⟩

-- Some ideas for possible extensions or homework assignments
-- 1. A. Write a conversion from the dependent de Bruijn encoding (e : Γ ⊢ τ)
--       to the untyped lambda calculus (e : term).
--    B. Prove that the image of this conversion is well typed.
--    C. Write a conversion from well-typed untyped lambda calculus
--       terms ([e : term] and [ε : (Γ ⊢ e ⦂ τ)] into the dependent de
--       Bruijn encoding (e : Γ ⊢ τ)
-- 2. A. Write a predicate analogous to 'value' for strongly reduced
--       terms (reduction under lambda)
--    B. Prove "strong" progress: A term is either fully beta-reduced
--       (including under lambda) or it can take a step
-- 3. Relate this semantics to a big-step semantics.
-- 4. Prove strong normalization.
-- 5. Relate this semantics to a definitional interpreter into Agda's Set.


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of Rational numbers
------------------------------------------------------------------------

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

module Data.Rational.Properties where

open import Function using (_∘_ ; _$_)
open import Data.Integer as ℤ using (ℤ; ∣_∣; +_; -[1+_])
open import Data.Integer.Coprimality using (coprime-divisor)
import Data.Integer.Properties as ℤ
open import Data.Rational.Base
open import Data.Nat as ℕ using (ℕ; zero; suc)
import Data.Nat.Properties as ℕ
open import Data.Nat.Coprimality as C using (Coprime; coprime?)
open import Data.Nat.Divisibility hiding (/-cong)
open import Data.Product using (_,_)
open import Data.Sum
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (Dec; yes; no; recompute)
open import Relation.Nullary.Decidable as Dec′ using (True; fromWitness)

open import Algebra.FunctionProperties {A = ℚ} _≡_
open import Algebra.FunctionProperties.Consequences.Propositional

------------------------------------------------------------------------
-- Helper lemmas

private
  recomputeCP : ∀ {n d} → .(Coprime n (suc d)) → Coprime n (suc d)
  recomputeCP {n} {d-1} c = recompute (coprime? n (suc d-1)) c

------------------------------------------------------------------------
-- Equality

≡⇒≃ : _≡_ ⇒ _≃_
≡⇒≃ refl = refl

≃⇒≡ : _≃_ ⇒ _≡_
≃⇒≡ {i = mkℚ n₁ d₁ c₁} {j = mkℚ n₂ d₂ c₂} eq = helper
  where
  open ≡-Reasoning

  1+d₁∣1+d₂ : suc d₁ ∣ suc d₂
  1+d₁∣1+d₂ = coprime-divisor (+ suc d₁) n₁ (+ suc d₂)
    (C.sym (recomputeCP c₁)) $
    divides ∣ n₂ ∣ $ begin
      ∣ n₁ ℤ.* + suc d₂ ∣  ≡⟨ cong ∣_∣ eq ⟩
      ∣ n₂ ℤ.* + suc d₁ ∣  ≡⟨ ℤ.abs-*-commute n₂ (+ suc d₁) ⟩
      ∣ n₂ ∣ ℕ.* suc d₁    ∎

  1+d₂∣1+d₁ : suc d₂ ∣ suc d₁
  1+d₂∣1+d₁ = coprime-divisor (+ suc d₂) n₂ (+ suc d₁)
    (C.sym (recomputeCP c₂)) $
    divides ∣ n₁ ∣ (begin
      ∣ n₂ ℤ.* + suc d₁ ∣  ≡⟨ cong ∣_∣ (sym eq) ⟩
      ∣ n₁ ℤ.* + suc d₂ ∣  ≡⟨ ℤ.abs-*-commute n₁ (+ suc d₂) ⟩
      ∣ n₁ ∣ ℕ.* suc d₂    ∎)

  helper : mkℚ n₁ d₁ c₁ ≡ mkℚ n₂ d₂ c₂
  helper with ∣-antisym 1+d₁∣1+d₂ 1+d₂∣1+d₁
  ... | refl with ℤ.*-cancelʳ-≡ n₁ n₂ (+ suc d₁) (λ ()) eq
  ...   | refl = refl

infix 4 _≟_

_≟_ : Decidable {A = ℚ} _≡_
p ≟ q with (↥ p ℤ.* ↧ q) ℤ.≟ (↥ q ℤ.* ↧ p)
... | yes pq≃qp = yes (≃⇒≡ pq≃qp)
... | no ¬pq≃qp = no (¬pq≃qp ∘ ≡⇒≃)

------------------------------------------------------------------------
-- _≤_

infix 4 _≤?_

drop-*≤* : ∀ {p q} → p ≤ q → (↥ p ℤ.* ↧ q) ℤ.≤ (↥ q ℤ.* ↧ p)
drop-*≤* (*≤* pq≤qp) = pq≤qp

≤-reflexive : _≡_ ⇒ _≤_
≤-reflexive refl = *≤* ℤ.≤-refl

≤-refl : Reflexive _≤_
≤-refl = ≤-reflexive refl

≤-trans : Transitive _≤_
≤-trans {i = p@(mkℚ n₁ d₁ c₁)} {j = q@(mkℚ n₂ d₂ c₂)} {k = r@(mkℚ n₃ d₃ c₃)} (*≤* eq₁) (*≤* eq₂)
  = *≤* $ ℤ.*-cancelʳ-≤-pos (n₁ ℤ.* ℤ.+ suc d₃) (n₃ ℤ.* ℤ.+ suc d₁) d₂ $ begin
  let sd₁ = ↧ p; sd₂ = ↧ q; sd₃ = ↧ r in
  (n₁  ℤ.* sd₃) ℤ.* sd₂  ≡⟨ ℤ.*-assoc n₁ sd₃ sd₂ ⟩
  n₁   ℤ.* (sd₃ ℤ.* sd₂) ≡⟨ cong (n₁ ℤ.*_) (ℤ.*-comm sd₃ sd₂) ⟩
  n₁   ℤ.* (sd₂ ℤ.* sd₃) ≡⟨ sym (ℤ.*-assoc n₁ sd₂ sd₃) ⟩
  (n₁  ℤ.* sd₂) ℤ.* sd₃  ≤⟨ ℤ.*-monoʳ-≤-pos d₃ eq₁ ⟩
  (n₂  ℤ.* sd₁) ℤ.* sd₃  ≡⟨ cong (ℤ._* sd₃) (ℤ.*-comm n₂ sd₁) ⟩
  (sd₁ ℤ.* n₂)  ℤ.* sd₃  ≡⟨ ℤ.*-assoc sd₁ n₂ sd₃ ⟩
  sd₁  ℤ.* (n₂  ℤ.* sd₃) ≤⟨ ℤ.*-monoˡ-≤-pos d₁ eq₂ ⟩
  sd₁  ℤ.* (n₃  ℤ.* sd₂) ≡⟨ sym (ℤ.*-assoc sd₁ n₃ sd₂) ⟩
  (sd₁ ℤ.* n₃)  ℤ.* sd₂  ≡⟨ cong (ℤ._* sd₂) (ℤ.*-comm sd₁ n₃) ⟩
  (n₃  ℤ.* sd₁) ℤ.* sd₂  ∎
  where open ℤ.≤-Reasoning

≤-antisym : Antisymmetric _≡_ _≤_
≤-antisym (*≤* le₁) (*≤* le₂) = ≃⇒≡ (ℤ.≤-antisym le₁ le₂)

≤-total : Total _≤_
≤-total p q = [ inj₁ ∘ *≤* , inj₂ ∘ *≤* ]′ (ℤ.≤-total
  (↥ p ℤ.* ↧ q)
  (↥ q ℤ.* ↧ p))

_≤?_ : Decidable _≤_
p ≤? q = Dec′.map′ *≤* drop-*≤* ((↥ p ℤ.* ↧ q) ℤ.≤? (↥ q ℤ.* ↧ p))

≤-isPreorder : IsPreorder _≡_ _≤_
≤-isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = ≤-reflexive
  ; trans         = ≤-trans
  }

≤-isPartialOrder : IsPartialOrder _≡_ _≤_
≤-isPartialOrder = record
  { isPreorder = ≤-isPreorder
  ; antisym    = ≤-antisym
  }

≤-isTotalOrder : IsTotalOrder _≡_ _≤_
≤-isTotalOrder = record
  { isPartialOrder = ≤-isPartialOrder
  ; total          = ≤-total
  }

≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
≤-isDecTotalOrder = record
  { isTotalOrder = ≤-isTotalOrder
  ; _≟_          = _≟_
  ; _≤?_         = _≤?_
  }

≤-decTotalOrder : DecTotalOrder _ _ _
≤-decTotalOrder = record
  { Carrier         = ℚ
  ; _≈_             = _≡_
  ; _≤_             = _≤_
  ; isDecTotalOrder = ≤-isDecTotalOrder
  }

≤-irrelevant : Irrelevant _≤_
≤-irrelevant (*≤* x₁) (*≤* x₂) = cong *≤* (ℤ.≤-irrelevant x₁ x₂)

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.0

≤-irrelevance = ≤-irrelevant
{-# WARNING_ON_USAGE ≤-irrelevance
"Warning: ≤-irrelevance was deprecated in v1.0.
Please use ≤-irrelevant instead."
#-}


text:
module Common.UntypedContext where

open import Common.Context public

-- Naturals, as a projection of contexts.

ᴺ⌊_⌋ : ∀ {U} → Cx U → ℕ
ᴺ⌊ ∅ ⌋     = zero
ᴺ⌊ Γ , A ⌋ = suc ᴺ⌊ Γ ⌋

-- Inversion principle for naturals.

invsuc : ∀ {n n′} → ℕ.suc n ≡ suc n′ → n ≡ n′
invsuc refl = refl

-- Finite naturals, or nameless untyped de Bruijn indices, as a projection of context membership.

ⁱ⌊_⌋ : ∀ {U} {A : U} {Γ} → A ∈ Γ → Fin ᴺ⌊ Γ ⌋
ⁱ⌊ top ⌋   = zero
ⁱ⌊ pop i ⌋ = suc ⁱ⌊ i ⌋

-- Preorder on naturals, as a projection of context inclusion.

infix 3 _≤_
data _≤_ : ℕ → ℕ → Set where
  done : zero ≤ zero
  skip : ∀ {n n′} → n ≤ n′ → n ≤ suc n′
  keep : ∀ {n n′} → n ≤ n′ → suc n ≤ suc n′

≤⌊_⌋ : ∀ {U} {Γ Γ′ : Cx U} → Γ ⊆ Γ′ → ᴺ⌊ Γ ⌋ ≤ ᴺ⌊ Γ′ ⌋
≤⌊ done ⌋   = done
≤⌊ skip η ⌋ = skip ≤⌊ η ⌋
≤⌊ keep η ⌋ = keep ≤⌊ η ⌋

refl≤ : ∀ {n} → n ≤ n
refl≤ {zero}  = done
refl≤ {suc n} = keep refl≤

trans≤ : ∀ {n n′ n″} → n ≤ n′ → n′ ≤ n″ → n ≤ n″
trans≤ η        done      = η
trans≤ η        (skip η′) = skip (trans≤ η η′)
trans≤ (skip η) (keep η′) = skip (trans≤ η η′)
trans≤ (keep η) (keep η′) = keep (trans≤ η η′)

unskip≤ : ∀ {n n′} → suc n ≤ n′ → n ≤ n′
unskip≤ (skip η) = skip (unskip≤ η)
unskip≤ (keep η) = skip η

unkeep≤ : ∀ {n n′} → suc n ≤ suc n′ → n ≤ n′
unkeep≤ (skip η) = unskip≤ η
unkeep≤ (keep η) = η

weak≤ : ∀ {n} → n ≤ suc n
weak≤ = skip refl≤

bot≤ : ∀ {n} → zero ≤ n
bot≤ {zero}  = done
bot≤ {suc n} = skip bot≤

-- Monotonicity of finite naturals with respect to preorder on naturals.

monoFin : ∀ {n n′} → n ≤ n′ → Fin n → Fin n′
monoFin done     ()
monoFin (skip η) i       = suc (monoFin η i)
monoFin (keep η) zero    = zero
monoFin (keep η) (suc i) = suc (monoFin η i)

reflmonoFin : ∀ {n} → (i : Fin n) → i ≡ monoFin refl≤ i
reflmonoFin zero    = refl
reflmonoFin (suc i) = cong suc (reflmonoFin i)

transmonoFin : ∀ {n n′ n″} → (η : n ≤ n′) (η′ : n′ ≤ n″) (i : Fin n)
               → monoFin η′ (monoFin η i) ≡ monoFin (trans≤ η η′) i
transmonoFin done     η′        ()
transmonoFin η        (skip η′) i       = cong suc (transmonoFin η η′ i)
transmonoFin (skip η) (keep η′) i       = cong suc (transmonoFin η η′ i)
transmonoFin (keep η) (keep η′) zero    = refl
transmonoFin (keep η) (keep η′) (suc i) = cong suc (transmonoFin η η′ i)

-- Addition of naturals, as a projection of context concatenation.

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

id+₁ : ∀ {n} → n + zero ≡ n
id+₁ = refl

id+₂ : ∀ {n} → zero + n ≡ n
id+₂ {zero}  = refl
id+₂ {suc n} = cong suc id+₂

weak≤+₁ : ∀ {n} n′ → n ≤ n + n′
weak≤+₁ zero     = refl≤
weak≤+₁ (suc n′) = skip (weak≤+₁ n′)

weak≤+₂ : ∀ {n n′} → n′ ≤ n + n′
weak≤+₂ {n} {zero}   = bot≤
weak≤+₂ {n} {suc n′} = keep weak≤+₂

-- Subtraction of naturals, as a projection of context thinning.

_-_ : (n : ℕ) → Fin n → ℕ
zero  - ()
suc n - zero  = n
suc n - suc i = suc (n - i)

thin≤ : ∀ {n} → (i : Fin n) → n - i ≤ n
thin≤ zero    = weak≤
thin≤ (suc i) = keep (thin≤ i)

-- Decidable equality of finite naturals.

data _=Fin_ {n} (i : Fin n) : Fin n → Set where
  same : i =Fin i
  diff : (j : Fin (n - i)) → i =Fin monoFin (thin≤ i) j

_≟Fin_ : ∀ {n} → (i j : Fin n) → i =Fin j
zero  ≟Fin zero   = same
zero  ≟Fin suc j  rewrite reflmonoFin j = diff j
suc i ≟Fin zero   = diff zero
suc i ≟Fin suc j  with i ≟Fin j
suc i ≟Fin suc .i | same   = same
suc i ≟Fin suc ._ | diff j = diff (suc j)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.HLevels' where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Nat
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.Loopspace
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.Data.Unit
open import Cubical.Foundations.Structure

private
  variable
    ℓ : Level

isOfHLevel' : HLevel → Type ℓ → Type ℓ
isOfHLevel' 0 A = isOfHLevel 0 A
isOfHLevel' (suc n) A = (x y : A) → isOfHLevel' n (x ≡ y)

isOfHLevel'→ : {n : HLevel} {A : Type ℓ} (l : isOfHLevel' n A) → isOfHLevel n A
isOfHLevel'→ {n = 0} l = l
isOfHLevel'→ {n = 1} l a b = l a b .fst
isOfHLevel'→ {n = suc (suc _)} l a b = isOfHLevel'→ (l a b)

isOfHLevel→' : {n : HLevel} {A : Type ℓ} (l : isOfHLevel n A) → isOfHLevel' n A
isOfHLevel→' {n = 0} l = l
isOfHLevel→' {n = 1} l = isProp→isContrPath l
isOfHLevel→' {n = suc (suc _)} l = λ x y → isOfHLevel→' (l x y)

isPropIsOfHLevel' : (n : HLevel) {A : Type ℓ} → isProp (isOfHLevel' n A)
isPropIsOfHLevel' 0 = isPropIsOfHLevel 0
isPropIsOfHLevel' 1 p q = funExt (λ a → funExt (λ b → isPropIsContr (p a b) (q a b)))
isPropIsOfHLevel' (suc (suc n)) f g i a b = isPropIsOfHLevel' (suc n) (f a b) (g a b) i -- isPropIsOfHLevel (suc (suc n))

isOfHLevel≡' : (n : HLevel) {A : Type ℓ} → isOfHLevel n A ≡ isOfHLevel' n A
isOfHLevel≡' n = isoToPath (iso isOfHLevel→'
                                isOfHLevel'→
                                (λ p' → isPropIsOfHLevel' n _ p')
                                λ p → isPropIsOfHLevel n _ p)

HL→ = isOfHLevel→'
HL← = isOfHLevel'→

module _ {X : Type ℓ} where
  -- Lemma 7.2.8 in the HoTT book
  -- For n >= -1, if X being inhabited implies X is an n-type, then X is an n-type
  inh→ntype→ntype : {n : ℕ} (t : X → isOfHLevel (suc n) X) → isOfHLevel (suc n) X
  inh→ntype→ntype {n = 0} t = λ x y → t x x y
  inh→ntype→ntype {n = suc _} t = λ x y → t x x y

module _ {X : Type ℓ} where
  -- Theorem 7.2.7 in the HoTT book
  -- For n >= -1, X is an (n+1)-type if all its loop spaces are n-types
  truncSelfId→truncId : {n : ℕ} → ((x : X) → isOfHLevel (suc n) (x ≡ x)) → isOfHLevel (suc (suc n)) X
  truncSelfId→truncId {n = 0} t =
    λ x x' → inh→ntype→ntype {n = 0}
                              λ p → J (λ y q → isOfHLevel 1 (x ≡ y))
                                      (t x)
                                      p
  truncSelfId→truncId {n = suc m} t =
    λ x x' → inh→ntype→ntype {n = suc m}
                              λ p → J (λ y q → isOfHLevel (suc (suc m)) (x ≡ y))
                                      (t x)
                                      p

  EquivPresHLevel : {Y : Type ℓ} → {n : ℕ} → (X≃Y : X ≃ Y) → (hX : isOfHLevel n X) → isOfHLevel n Y
  EquivPresHLevel {Y} {n} X≃Y hX = subst (λ x → isOfHLevel n x) (ua X≃Y) hX

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
{-# OPTIONS --allow-unsolved-metas #-}
module _ where

open import Agda.Primitive

postulate Applicative : ∀ {a b} (F : Set a → Set b) → Set (lsuc a ⊔ b)

record Traversable {a} (T : Set a) : Set (lsuc a) where
  constructor mkTrav
  field traverse : ∀ {F} {{AppF : Applicative F}} → T → F T
    -- unsolved metas in type of F

postulate
  V     : ∀ {a} → Set a
  travV : ∀ {a} {F : Set a → Set a} {{AppF : Applicative F}} → V → F V

module M (a : Level) where
  TravV : Traversable {a} V
  TravV = mkTrav travV

postulate
  a : Level
  F : Set → Set
  instance AppF : Applicative F

mapM : V → F V
mapM = Traversable.traverse (M.TravV _)
  -- Here we try to cast (TypeChecking.Constraints.castConstraintToCurrentContext)
  -- a level constraint from M talking about the local (a : Level) to the top-level
  -- (empty) context. This ought not result in an __IMPOSSIBLE__.


text:
record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

open _×_

app : {A B : Set} → (A → B) × A → B
app (f , x) = f x

data D : Set where d : D

postulate
  P   : {A : Set} → A → Set
  p   : (f : D → D) → P f → P (f d)
  foo : (F : Set → Set) → F D
  bar : (F : Set → Set) → P (foo F)

q : P (app (foo (λ A → (A → A) × A)))
q =
  let H : Set → Set
      H = _ in
  p (foo H) (bar H)

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

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use Data.Vec.Recursive instead.
------------------------------------------------------------------------

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

module Data.Product.N-ary where

{-# WARNING_ON_IMPORT
"Data.Product.N-ary was deprecated in v1.1.
Use Data.Vec.Recursive instead."
#-}

open import Data.Vec.Recursive public


text:
-- Andreas, 2011-04-11 adapted from Data.Nat.Properties

{-# OPTIONS --universe-polymorphism #-}

module FrozenMVar2 where

open import Imports.Level

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

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

Rel : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
Rel A ℓ = A → A → Set ℓ

Op₂ : ∀ {ℓ} → Set ℓ → Set ℓ
Op₂ A = A → A → A

module FunctionProperties
         {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where

  Associative : Op₂ A → Set _
  Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))

open FunctionProperties _≡_  -- THIS produces frozen metas

data ℕ : Set where
  zℕ : ℕ
  sℕ : (n : ℕ) → ℕ

infixl 6 _+_

_+_ : ℕ → ℕ → ℕ
zℕ   + n = n
sℕ m + n = sℕ (m + n)

+-assoc : Associative _+_
-- +-assoc : ∀ x y z -> ((x + y) + z) ≡ (x + (y + z)) -- this works
+-assoc zℕ     _ _ = refl
+-assoc (sℕ m) n o = cong sℕ (+-assoc m n o)
-- Due to a frozen meta we get:
-- Type mismatch when checking that the pattern zℕ has type _95

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Numeral.Natural.Inductions where

import Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Functional
open import Numeral.Natural
import      Numeral.Natural.Induction
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Oper.Proofs.Order
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Relator.Ordering
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Syntax.Type
open import Type

module _ {ℓ} where
  open Numeral.Natural.Induction{ℓ}

  [ℕ]-unnecessary-induction : ∀{b : ℕ}{φ : ℕ → Stmt{ℓ}} → (∀(i : ℕ) → (i ≤ b) → φ(i)) → (∀(i : ℕ) → φ(i) → φ(𝐒(i))) → (∀{n} → φ(n))
  [ℕ]-unnecessary-induction {𝟎}   {φ} (base) (next) = [ℕ]-induction {φ} (base(𝟎) ([≤]-minimum)) (next)
  [ℕ]-unnecessary-induction {𝐒(b)}{φ} (base) (next) = [ℕ]-unnecessary-induction {b}{φ} (base-prev) (next) where
    base-prev : ∀(i : ℕ) → (i ≤ b) → φ(i)
    base-prev(𝟎)    (proof) = base(𝟎) ([≤]-minimum)
    base-prev(𝐒(i)) (proof) = next(i) (base-prev(i) ([≤]-predecessor {i}{b} proof))

  [ℕ]-multiple-base-cases-induction : ∀{b : ℕ}{φ : ℕ → Stmt{ℓ}} → (∀(i : ℕ) → (i ≤ b) → φ(i)) → (∀(i : ℕ) → (b ≤ i) → φ(i) → φ(𝐒(i))) → (∀{n} → φ(n))
  [ℕ]-multiple-base-cases-induction {𝟎}   {φ} base next = [ℕ]-induction {φ} (base(𝟎) ([≤]-minimum)) (i ↦ next(i) ([≤]-minimum))
  [ℕ]-multiple-base-cases-induction {𝐒(b)}{φ} base next = [ℕ]-multiple-base-cases-induction {b}{φ} (base-prev) (next-prev) where
    base-prev : ∀(i : ℕ) → (i ≤ b) → φ(i)
    base-prev(i) (proof) = base(i) ([≤]-successor proof)

    next-prev : ∀(i : ℕ) → (b ≤ i) → φ(i) → φ(𝐒(i))
    next-prev(i) (proof) (φi) with [≤]-to-[<][≡] proof
    ...                          | [∨]-introₗ a<b       = next(i) (a<b) φi
    ...                          | [∨]-introᵣ [≡]-intro = base(𝐒(b)) (reflexivity(_≤_))

  [ℕ]-strong-induction : ∀{φ : ℕ → Stmt{ℓ}} → φ(𝟎) → (∀{i : ℕ} → (∀{j : ℕ} → (j ≤ i) → φ(j)) → φ(𝐒(i))) → (∀{n} → φ(n))
  [ℕ]-strong-induction {φ} (base) (next) {n} = ([ℕ]-inductionᵢ {Q} (Q0) (QS) {n}) {n} (reflexivity(_≤_)) where
    Q : ℕ → Stmt
    Q(k) = (∀{n} → (n ≤ k) → φ(n))

    Q0 : Q(𝟎)
    Q0{𝟎}    (_) = base
    Q0{𝐒(j)} (proof) = [⊥]-elim([≤][0]ᵣ-negation {j} (proof))

    QS : ∀{k : ℕ} → Q(k) → Q(𝐒(k))
    QS{k} (qk) {𝟎}    (0≤Sk)  = base
    QS{k} (qk) {𝐒(n)} (Sn≤Sk) = (next{n} (qn)) :of: φ(𝐒(n)) where
      n≤k : n ≤ k
      n≤k = [≤]-without-[𝐒] {n}{k} (Sn≤Sk)

      qn : Q(n)
      qn{a} (a≤n) = qk{a} ((a≤n) 🝖 (n≤k))

  [ℕ]-multiple-base-cases-strong-induction : ∀{b : ℕ}{φ : ℕ → Stmt{ℓ}} → (∀{i : ℕ} → (i ≤ b) → φ(i)) → (∀{i : ℕ} → (b ≤ i) → (∀{j : ℕ} → (b ≤ j) → (j ≤ i) → φ(j)) → φ(𝐒(i))) → (∀{n} → φ(n))
  [ℕ]-multiple-base-cases-strong-induction {𝟎}    {φ} base next {n} = [ℕ]-strong-induction{φ} ((base [≤]-minimum)) (\{i} → φj ↦ next{i} [≤]-minimum (\{j} _ → φj{j}))
  [ℕ]-multiple-base-cases-strong-induction {𝐒(b)} {φ} base next {n} =  [ℕ]-multiple-base-cases-strong-induction {b} {φ} base-prev next-prev {n} where
    base-prev : {i : ℕ} → i ≤ b → φ i
    base-prev{i} ib = base{i} ([≤]-successor ib)

    next-prev : {i : ℕ} → b ≤ i → ({j : ℕ} → b ≤ j → j ≤ i → φ j) → φ (𝐒 i)
    next-prev{i} bi φj with [≤]-to-[<][≡] bi
    ...                   | [∨]-introₗ b<i      = next{i} (b<i) (\{j} → bj ↦ φj{j} ([≤]-predecessor bj))
    ...                   | [∨]-introᵣ [≡]-intro = base{𝐒(i)} (reflexivity(_≤_))

  [ℕ]-strong-induction-with-monus : ∀{φ : ℕ → Stmt{ℓ}} → φ(𝟎) → (∀{i : ℕ} → (∀{j : ℕ} → φ(i −₀ j)) → φ(𝐒(i))) → (∀{n} → φ(n))
  [ℕ]-strong-induction-with-monus {φ} (base) (next) {n} = [ℕ]-strong-induction {φ} (base) (next2) {n} where
    convert-assumption : ∀{i} → (∀{j} → (j ≤ i) → φ(j)) → (∀{j} → φ(i −₀ j))
    convert-assumption {i} assumption {j} = assumption{i −₀ j} ([−₀]-lesser {i}{j})

    next2 : ∀{i} → (∀{j} → (j ≤ i) → φ(j)) → φ(𝐒(i))
    next2{i} assumption = next{i} (\{j} → convert-assumption{i} assumption {j})

  -- TODO: This is just a generalisation of [ℕ]-strong-induction-with-monus. If a function (T → 𝕟(i)) is surjective for every i∊ℕ, then f could be used in the induction step
  -- [ℕ]-induction-with-surjection : ∀{φ : ℕ → Stmt}{ℓT}{T : Type{ℓT}}{f : ℕ → T → ℕ}{f⁻¹ : (i : ℕ) → (n : ℕ) → ⦃ _ : n ≤ i ⦄ → T}
  --                               → (∀{i n} → (proof : (n ≤ i)) → (f(i)(f⁻¹(i)(n) ⦃ proof ⦄) ≡ n))
  --                               → φ(𝟎)
  --                               → (∀{i : ℕ}
  --                                 → (∀{t : T} → (φ ∘ f(i))(t))
  --                                 → φ(𝐒(i))
  --                               )
  --                               → (∀{n} → φ(n))
  -- [ℕ]-induction-with-surjection {φ}{ℓT}{T}{f}{f⁻¹} surj base next {n} = [ℕ]-strong-induction {φ} (base) (next2) {n} where
  --   postulate convert-assumption : ∀{i} → (∀{j} → (j ≤ i) → φ(j)) → (∀{t} → φ(f(i)(t)))
  --   -- convert-assumption {i} assumption {j} = assumption{i −₀ j} ([−₀]-lesser {i}{j})
  --
  --   next2 : ∀{i} → (∀{j} → (j ≤ i) → φ(j)) → φ(𝐒(i))
  --   next2{i} assumption = next{i} (\{j} → convert-assumption{i} assumption {j})

module _ where
  open Strict.Properties

  instance
    [ℕ]-accessibleₗ : ∀{n} → Accessibleₗ(_<_)(n)
    [ℕ]-accessibleₗ{n} = intro ⦃ proof{n} ⦄ where
      proof : ∀{n m} → ⦃ _ : (m < n) ⦄ → Accessibleₗ(_<_)(m)
      proof {𝟎}   {m}    ⦃ ⦄
      proof{𝐒(n)} {𝟎}    ⦃ succ mn ⦄ = intro ⦃ \ ⦃ ⦄ ⦄
      proof{𝐒(n)} {𝐒(m)} ⦃ succ mn ⦄ = intro ⦃ \{k} ⦃ xsm ⦄ → Accessibleₗ.proof ([ℕ]-accessibleₗ {n}) ⦃ transitivity(_≤_) xsm mn ⦄ ⦄

  [ℕ]-wellfounded : WellFounded(_<_)
  [ℕ]-wellfounded = [ℕ]-accessibleₗ


text:
open import Prelude

module Implicits.Resolution.Deterministic.Resolution where

open import Data.Fin.Substitution
open import Data.List
open import Data.List.All

open import Implicits.Syntax
open import Implicits.Syntax.Type.Unification
open import Implicits.Substitutions
open import Extensions.ListFirst

infixl 4 _⊢ᵣ_ _⊢_↓_ _⟨_⟩=_
infixl 6 _◁_

data _◁_ {ν} : Type ν → SimpleType ν → Set where
  m-simp : ∀ {a} → simpl a ◁ a
  m-tabs   : ∀ {a r} b → r tp[/tp b ] ◁ a → ∀' r ◁ a
  m-iabs   : ∀ {a b r} → r ◁ a → b ⇒ r ◁ a

_⟨_⟩=_ : ∀ {ν} (Δ : ICtx ν) → SimpleType ν → Type ν → Set
Δ ⟨ τ ⟩= r = first r ∈ Δ ⇔ (flip _◁_ τ)

mutual
  data _⊢_↓_ {ν} (K : ICtx ν) : Type ν → SimpleType ν → Set where
    i-simp : ∀ a → K ⊢ simpl a ↓ a
    i-iabs : ∀ {ρ₁ ρ₂ a} → K ⊢ᵣ ρ₁ → K ⊢ ρ₂ ↓ a → K ⊢ ρ₁ ⇒ ρ₂ ↓ a
    i-tabs : ∀ {ρ a} b → K ⊢ ρ tp[/tp b ] ↓ a → K ⊢ ∀' ρ ↓ a

  data _⊢ᵣ_ {ν} (K : ICtx ν) : Type ν → Set where
    r-simp : ∀ {τ ρ} → K ⟨ τ ⟩= ρ → K ⊢ ρ ↓ τ → K ⊢ᵣ simpl τ
    r-iabs : ∀ ρ₁ {ρ₂} → ρ₁ ∷ K ⊢ᵣ ρ₂ → K ⊢ᵣ ρ₁ ⇒ ρ₂
    r-tabs : ∀ {ρ} → ictx-weaken K ⊢ᵣ ρ → K ⊢ᵣ ∀' ρ

_⊢ᵣ[_] : ∀ {ν} → (K : ICtx ν) → List (Type ν) → Set
_⊢ᵣ[_] K ρs = All (λ r → K ⊢ᵣ r) ρs

r↓a⟶r◁a : ∀ {ν} {K : ICtx ν} {r a} → K ⊢ r ↓ a → r ◁ a
r↓a⟶r◁a (i-simp a) = m-simp
r↓a⟶r◁a (i-iabs _ x) = m-iabs (r↓a⟶r◁a x)
r↓a⟶r◁a (i-tabs b x) = m-tabs b (r↓a⟶r◁a x)


text:
module WrongNumberOfConstructorArguments where

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

f : Nat -> Nat
f (zero n) = n
f suc      = zero


text:
{-# OPTIONS --subtyping #-}

open import Agda.Builtin.Equality

record _↠_ (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    to∘from : ∀ x → to (from x) ≡ x

record Erased (@0 A : Set) : Set where
  constructor [_]
  field
    @0 erased : A

open Erased

-- fails : {A : Set} → A ↠ Erased A
-- fails = record
--   { to      = [_]
--   ; from    = erased
--   ; to∘from = λ _ → refl
--   }

works : {A : Set} → A ↠ Erased A
works = record
  { to      = [_]
  ; from    = _
  ; to∘from = λ _ → refl
  }


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

open import Level

open import Categories.Category
open import Categories.Functor

Categories : ∀ o ℓ e → Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
Categories o ℓ e = record
  { Obj = Category o ℓ e
  ; _⇒_ = Functor
  ; _≡_ = _≡_
  ; _∘_ = _∘_
  ; id = id
  ; assoc = λ {_} {_} {_} {_} {F} {G} {H} → assoc {F = F} {G} {H}
  ; identityˡ = λ {_} {_} {F} → identityˡ {F = F}
  ; identityʳ = λ {_} {_} {F} → identityʳ {F = F}
  ; equiv = λ {X} {Y} → equiv {C = X} {D = Y}
  ; ∘-resp-≡ = λ {_} {_} {_} {f} {h} {g} {i} → ∘-resp-≡ {F = f} {h} {g} {i}
  }

{-
module Agda where
  open import Category.Agda
  open import Category.Discrete

  D : ∀ o → Functor (Agda o) (Categories o o zero)
  D o = record
    { F₀ = Discrete
    ; F₁ = λ f → record
      { F₀ = λ x → f x
      ; F₁ = ≣-cong f
      ; identity = tt
      ; homomorphism = tt
      ; F-resp-≡ = λ _ → tt
      }
    ; identity = λ _ → refl tt
    ; homomorphism = λ _ → refl tt
    ; F-resp-≡ = F-resp-≡′
    }
    where
    F-resp-≡′ : {A B : Set o} {F G : A → B} → (∀ x → F x ≣ G x) → ∀ {X Y : A} (f : X ≣ Y) → [ Discrete B ] ≣-cong F f ∼ ≣-cong G f
    F-resp-≡′ {A} {B} {F} {G} f {x} ≣-refl = helper {F = F} {G} (f x)
      where
      helper : {F G : A → B} → {p q : B} → p ≣ q → [ Discrete B ] ≣-refl {x = p} ∼ ≣-refl {x = q}
      helper ≣-refl = refl tt

  Ob : ∀ o → Functor (Categories o o zero) (Agda o)
  Ob o = record
    { F₀ = Category.Obj
    ; F₁ = Functor.F₀
    ; identity = λ _ → ≣-refl
    ; homomorphism = λ _ → ≣-refl
    ; F-resp-≡ = λ {_} {_} {F} {G} → F-resp-≡′ {F = F} {G}
    }
    where
    F-resp-≡′ : {A B : Category o o zero} {F G : Functor A B}
              → ({X Y : Category.Obj A} (f : Category.Hom A X Y) → [ B ] Functor.F₁ F f ∼ Functor.F₁ G f)
              → ((x : Category.Obj A) → Functor.F₀ F x ≣ Functor.F₀ G x)
    F-resp-≡′ {A} {B} {F} {G} F∼G x = helper (F∼G (Category.id A {x}))
      where
      helper : ∀ {X Y} {p : Category.Hom B X X} {q : Category.Hom B Y Y} → [ B ] p ∼ q → X ≣ Y
      helper (refl q) = ≣-refl

  open import Category.Adjunction

  D⊣Ob : ∀ o → Adjunction (D o) (Ob o)
  D⊣Ob o = record
    { unit = record
      { η = λ _ x → x
      ; commute = λ _ _ → ≣-refl
      }
    ; counit = record
      { η = λ X → record
        { F₀ = λ x → x
        ; F₁ = counit-id′ {X}
        ; identity = IsEquivalence.refl (Category.equiv X)
        ; homomorphism = {!!}
        ; F-resp-≡ = {!!}
        }
      ; commute = {!!}
      }
    ; zig = {!!}
    ; zag = λ _ → ≣-refl
    }
    where
    counit-id′ : {X : Category o o zero} → {A B : Category.Obj X} → A ≣ B → Category.Hom X A B
    counit-id′ {X} ≣-refl = Category.id X
-}

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
------------------------------------------------------------------------
-- A sequential colimit for which everything except for the "base
-- case" is erased
------------------------------------------------------------------------

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

-- The definition of sequential colimits and the statement of the
-- non-dependent universal property are based on those in van Doorn's
-- "Constructing the Propositional Truncation using Non-recursive
-- HITs".

-- The module is parametrised by a notion of equality. The higher
-- constructor of the HIT defining sequential colimits uses path
-- equality, but the supplied notion of equality is used for many
-- other things.

import Equality.Path as P

module Colimit.Sequential.Very-erased
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

open import Prelude hiding ([_,_])

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Erased.Cubical eq

private
  variable
    a b p₀ p₊ q : Level
    A B P₀      : Type a
    P₊          : A → Type p₊
    n           : ℕ
    e step₀ x   : A

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

-- A sequential colimit for which everything except for the "base
-- case" is erased.

data Colimitᴱ
       (P₀ : Type p₀)
       (@0 P₊ : ℕ → Type p₊)
       (@0 step₀ : P₀ → P₊ zero)
       (@0 step₊ : ∀ {n} → P₊ n → P₊ (suc n)) :
       Type (p₀ ⊔ p₊) where
  ∣_∣₀        : P₀ → Colimitᴱ P₀ P₊ step₀ step₊
  @0 ∣_∣₊     : P₊ n → Colimitᴱ P₀ P₊ step₀ step₊
  @0 ∣∣₊≡∣∣₀ᴾ : (x : P₀) → ∣ step₀ x ∣₊ P.≡ ∣ x ∣₀
  @0 ∣∣₊≡∣∣₊ᴾ : (x : P₊ n) → ∣ step₊ x ∣₊ P.≡ ∣ x ∣₊

-- A variant of ∣∣₊≡∣∣₀ᴾ.

@0 ∣∣₊≡∣∣₀ :
  {step₊ : ∀ {n} → P₊ n → P₊ (suc n)} (x : P₀) →
  _≡_ {A = Colimitᴱ P₀ P₊ step₀ step₊} ∣ step₀ x ∣₊ ∣ x ∣₀
∣∣₊≡∣∣₀ x = _↔_.from ≡↔≡ (∣∣₊≡∣∣₀ᴾ x)

-- A variant of ∣∣₊≡∣∣₊ᴾ.

@0 ∣∣₊≡∣∣₊ :
  {step₊ : ∀ {n} → P₊ n → P₊ (suc n)} (x : P₊ n) →
  _≡_ {A = Colimitᴱ P₀ P₊ step₀ step₊} ∣ step₊ x ∣₊ ∣ x ∣₊
∣∣₊≡∣∣₊ x = _↔_.from ≡↔≡ (∣∣₊≡∣∣₊ᴾ x)

------------------------------------------------------------------------
-- Eliminators

-- A dependent eliminator, expressed using paths.

record Elimᴾ
         {P₀ : Type p₀}
         {@0 P₊ : ℕ → Type p₊}
         {@0 step₀ : P₀ → P₊ zero}
         {@0 step₊ : ∀ {n} → P₊ n → P₊ (suc n)}
         (Q : Colimitᴱ P₀ P₊ step₀ step₊ → Type q) :
         Type (p₀ ⊔ p₊ ⊔ q) where
  no-eta-equality
  field
    ∣∣₀ʳ        : (x : P₀) → Q ∣ x ∣₀
    @0 ∣∣₊ʳ     : (x : P₊ n) → Q ∣ x ∣₊
    @0 ∣∣₊≡∣∣₀ʳ : (x : P₀) →
                  P.[ (λ i → Q (∣∣₊≡∣∣₀ᴾ x i)) ] ∣∣₊ʳ (step₀ x) ≡ ∣∣₀ʳ x
    @0 ∣∣₊≡∣∣₊ʳ : (x : P₊ n) →
                  P.[ (λ i → Q (∣∣₊≡∣∣₊ᴾ x i)) ] ∣∣₊ʳ (step₊ x) ≡ ∣∣₊ʳ x

open Elimᴾ public

elimᴾ :
  {@0 P₊ : ℕ → Type p₊}
  {@0 step₀ : P₀ → P₊ zero}
  {@0 step₊ : ∀ {n} → P₊ n → P₊ (suc n)}
  {Q : Colimitᴱ P₀ P₊ step₀ step₊ → Type q} →
  Elimᴾ Q → (x : Colimitᴱ P₀ P₊ step₀ step₊) → Q x
elimᴾ {P₀ = P₀} {P₊ = P₊} {step₀ = step₀} {step₊ = step₊} {Q = Q} e =
  helper
  where
  module E = Elimᴾ e

  helper : (x : Colimitᴱ P₀ P₊ step₀ step₊) → Q x
  helper ∣ x ∣₀         = E.∣∣₀ʳ x
  helper ∣ x ∣₊         = E.∣∣₊ʳ x
  helper (∣∣₊≡∣∣₀ᴾ x i) = E.∣∣₊≡∣∣₀ʳ x i
  helper (∣∣₊≡∣∣₊ᴾ x i) = E.∣∣₊≡∣∣₊ʳ x i

-- A non-dependent eliminator, expressed using paths.

record Recᴾ
         (P₀ : Type p₀)
         (@0 P₊ : ℕ → Type p₊)
         (@0 step₀ : P₀ → P₊ zero)
         (@0 step₊ : ∀ {n} → P₊ n → P₊ (suc n))
         (B : Type b) : Type (p₀ ⊔ p₊ ⊔ b) where
  no-eta-equality
  field
    ∣∣₀ʳ        : P₀ → B
    @0 ∣∣₊ʳ     : P₊ n → B
    @0 ∣∣₊≡∣∣₀ʳ : (x : P₀) → ∣∣₊ʳ (step₀ x) P.≡ ∣∣₀ʳ x
    @0 ∣∣₊≡∣∣₊ʳ : (x : P₊ n) → ∣∣₊ʳ (step₊ x) P.≡ ∣∣₊ʳ x

open Recᴾ public

recᴾ :
  {@0 P₊ : ℕ → Type p₊}
  {@0 step₀ : P₀ → P₊ zero}
  {@0 step₊ : ∀ {n} → P₊ n → P₊ (suc n)} →
  Recᴾ P₀ P₊ step₀ step₊ B → Colimitᴱ P₀ P₊ step₀ step₊ → B
recᴾ r = elimᴾ λ where
    .∣∣₀ʳ     → R.∣∣₀ʳ
    .∣∣₊ʳ     → R.∣∣₊ʳ
    .∣∣₊≡∣∣₀ʳ → R.∣∣₊≡∣∣₀ʳ
    .∣∣₊≡∣∣₊ʳ → R.∣∣₊≡∣∣₊ʳ
  where
  module R = Recᴾ r

-- A dependent eliminator.

record Elim
         {P₀ : Type p₀}
         {@0 P₊ : ℕ → Type p₊}
         {@0 step₀ : P₀ → P₊ zero}
         {@0 step₊ : ∀ {n} → P₊ n → P₊ (suc n)}
         (Q : Colimitᴱ P₀ P₊ step₀ step₊ → Type q) :
         Type (p₀ ⊔ p₊ ⊔ q) where
  no-eta-equality
  field
    ∣∣₀ʳ        : (x : P₀) → Q ∣ x ∣₀
    @0 ∣∣₊ʳ     : (x : P₊ n) → Q ∣ x ∣₊
    @0 ∣∣₊≡∣∣₀ʳ : (x : P₀) →
                  subst Q (∣∣₊≡∣∣₀ x) (∣∣₊ʳ (step₀ x)) ≡ ∣∣₀ʳ x
    @0 ∣∣₊≡∣∣₊ʳ : (x : P₊ n) →
                  subst Q (∣∣₊≡∣∣₊ x) (∣∣₊ʳ (step₊ x)) ≡ ∣∣₊ʳ x

open Elim public

elim :
  {@0 P₊ : ℕ → Type p₊}
  {@0 step₀ : P₀ → P₊ zero}
  {@0 step₊ : ∀ {n} → P₊ n → P₊ (suc n)}
  {Q : Colimitᴱ P₀ P₊ step₀ step₊ → Type q} →
  Elim Q → (x : Colimitᴱ P₀ P₊ step₀ step₊) → Q x
elim e = elimᴾ λ where
    .∣∣₀ʳ       → E.∣∣₀ʳ
    .∣∣₊ʳ       → E.∣∣₊ʳ
    .∣∣₊≡∣∣₀ʳ x → subst≡→[]≡ (E.∣∣₊≡∣∣₀ʳ x)
    .∣∣₊≡∣∣₊ʳ x → subst≡→[]≡ (E.∣∣₊≡∣∣₊ʳ x)
  where
  module E = Elim e

-- Two "computation" rules.

@0 elim-∣∣₊≡∣∣₀ : dcong (elim e) (∣∣₊≡∣∣₀ x) ≡ Elim.∣∣₊≡∣∣₀ʳ e x
elim-∣∣₊≡∣∣₀ = dcong-subst≡→[]≡ (refl _)

@0 elim-∣∣₊≡∣∣₊ : dcong (elim e) (∣∣₊≡∣∣₊ x) ≡ Elim.∣∣₊≡∣∣₊ʳ e x
elim-∣∣₊≡∣∣₊ = dcong-subst≡→[]≡ (refl _)

-- A non-dependent eliminator.

record Rec
         (P₀ : Type p₀)
         (@0 P₊ : ℕ → Type p₊)
         (@0 step₀ : P₀ → P₊ zero)
         (@0 step₊ : ∀ {n} → P₊ n → P₊ (suc n))
         (B : Type b) : Type (p₀ ⊔ p₊ ⊔ b) where
  no-eta-equality
  field
    ∣∣₀ʳ        : P₀ → B
    @0 ∣∣₊ʳ     : P₊ n → B
    @0 ∣∣₊≡∣∣₀ʳ : (x : P₀) → ∣∣₊ʳ (step₀ x) ≡ ∣∣₀ʳ x
    @0 ∣∣₊≡∣∣₊ʳ : (x : P₊ n) → ∣∣₊ʳ (step₊ x) ≡ ∣∣₊ʳ x

open Rec public

rec :
  {@0 P₊ : ℕ → Type p₊}
  {@0 step₀ : P₀ → P₊ zero}
  {@0 step₊ : ∀ {n} → P₊ n → P₊ (suc n)} →
  Rec P₀ P₊ step₀ step₊ B → Colimitᴱ P₀ P₊ step₀ step₊ → B
rec r = recᴾ λ where
    .∣∣₀ʳ       → R.∣∣₀ʳ
    .∣∣₊ʳ       → R.∣∣₊ʳ
    .∣∣₊≡∣∣₀ʳ x → _↔_.to ≡↔≡ (R.∣∣₊≡∣∣₀ʳ x)
    .∣∣₊≡∣∣₊ʳ x → _↔_.to ≡↔≡ (R.∣∣₊≡∣∣₊ʳ x)
  where
  module R = Rec r

-- Two "computation" rules.

@0 rec-∣∣₊≡∣∣₀ :
  {step₊ : ∀ {n} → P₊ n → P₊ (suc n)}
  {r : Rec P₀ P₊ step₀ step₊ B}
  {x : P₀} →
  cong (rec r) (∣∣₊≡∣∣₀ x) ≡ Rec.∣∣₊≡∣∣₀ʳ r x
rec-∣∣₊≡∣∣₀ = cong-≡↔≡ (refl _)

@0 rec-∣∣₊≡∣∣₊ :
  {step₊ : ∀ {n} → P₊ n → P₊ (suc n)}
  {r : Rec P₀ P₊ step₀ step₊ B}
  {x : P₊ n} →
  cong (rec r) (∣∣₊≡∣∣₊ x) ≡ Rec.∣∣₊≡∣∣₊ʳ r x
rec-∣∣₊≡∣∣₊ = cong-≡↔≡ (refl _)

------------------------------------------------------------------------
-- The universal property

-- The universal property of the sequential colimit.

universal-property :
  {@0 P₊ : ℕ → Type p₊}
  {@0 step₀ : P₀ → P₊ zero}
  {@0 step₊ : ∀ {n} → P₊ n → P₊ (suc n)} →
  (Colimitᴱ P₀ P₊ step₀ step₊ → B)
    ≃
  (∃ λ (f₀ : P₀ → B) →
     Erased (∃ λ (f₊ : ∀ n → P₊ n → B) →
               (∀ x → f₊ zero (step₀ x) ≡ f₀ x) ×
               (∀ n x → f₊ (suc n) (step₊ x) ≡ f₊ n x)))
universal-property
  {P₀ = P₀} {B = B} {P₊ = P₊} {step₀ = step₀} {step₊ = step₊} =
  Eq.↔→≃ to from to∘from from∘to
  where
  to :
    (Colimitᴱ P₀ P₊ step₀ step₊ → B) →
    ∃ λ (f₀ : P₀ → B) →
      Erased (∃ λ (f₊ : ∀ n → P₊ n → B) →
                (∀ x → f₊ zero (step₀ x) ≡ f₀ x) ×
                (∀ n x → f₊ (suc n) (step₊ x) ≡ f₊ n x))
  to h = h ∘ ∣_∣₀
       , [ (λ _ → h ∘ ∣_∣₊)
         , (λ x →
              h ∣ step₀ x ∣₊  ≡⟨ cong h (∣∣₊≡∣∣₀ x) ⟩∎
              h ∣ x ∣₀        ∎)
         , (λ _ x →
              h ∣ step₊ x ∣₊  ≡⟨ cong h (∣∣₊≡∣∣₊ x) ⟩∎
              h ∣ x ∣₊        ∎)
         ]

  from :
    (∃ λ (f₀ : P₀ → B) →
       Erased (∃ λ (f₊ : ∀ n → P₊ n → B) →
                 (∀ x → f₊ zero (step₀ x) ≡ f₀ x) ×
                 (∀ n x → f₊ (suc n) (step₊ x) ≡ f₊ n x))) →
    Colimitᴱ P₀ P₊ step₀ step₊ → B
  from (f₀ , [ f₊ , g₀ , g₊ ]) = rec λ where
    .∣∣₀ʳ     → f₀
    .∣∣₊ʳ     → f₊ _
    .∣∣₊≡∣∣₀ʳ → g₀
    .∣∣₊≡∣∣₊ʳ → g₊ _

  to∘from : ∀ p → to (from p) ≡ p
  to∘from (f₀ , [ f₊ , g₀ , g₊ ]) =
    cong (f₀ ,_) $ []-cong
      [ cong (f₊ ,_) $ cong₂ _,_
          (⟨ext⟩ λ x →
             cong (rec _) (∣∣₊≡∣∣₀ x)  ≡⟨ rec-∣∣₊≡∣∣₀ ⟩∎
             g₀ x                      ∎)
          (⟨ext⟩ λ n → ⟨ext⟩ λ x →
             cong (rec _) (∣∣₊≡∣∣₊ x)  ≡⟨ rec-∣∣₊≡∣∣₊ ⟩∎
             g₊ n x                    ∎)
      ]

  from∘to : ∀ h → from (to h) ≡ h
  from∘to h = ⟨ext⟩ $ elim λ where
    .∣∣₀ʳ _     → refl _
    .∣∣₊ʳ _     → refl _
    .∣∣₊≡∣∣₀ʳ x →
      subst (λ z → from (to h) z ≡ h z) (∣∣₊≡∣∣₀ x) (refl _)  ≡⟨ subst-in-terms-of-trans-and-cong ⟩

      trans (sym (cong (from (to h)) (∣∣₊≡∣∣₀ x)))
        (trans (refl _) (cong h (∣∣₊≡∣∣₀ x)))                 ≡⟨ cong₂ (λ p q → trans (sym p) q)
                                                                   rec-∣∣₊≡∣∣₀
                                                                   (trans-reflˡ _) ⟩

      trans (sym (cong h (∣∣₊≡∣∣₀ x))) (cong h (∣∣₊≡∣∣₀ x))   ≡⟨ trans-symˡ _ ⟩∎

      refl _                                                  ∎
    .∣∣₊≡∣∣₊ʳ x →
      subst (λ z → from (to h) z ≡ h z) (∣∣₊≡∣∣₊ x) (refl _)  ≡⟨ subst-in-terms-of-trans-and-cong ⟩

      trans (sym (cong (from (to h)) (∣∣₊≡∣∣₊ x)))
        (trans (refl _) (cong h (∣∣₊≡∣∣₊ x)))                 ≡⟨ cong₂ (λ p q → trans (sym p) q)
                                                                   rec-∣∣₊≡∣∣₊
                                                                   (trans-reflˡ _) ⟩

      trans (sym (cong h (∣∣₊≡∣∣₊ x))) (cong h (∣∣₊≡∣∣₊ x))   ≡⟨ trans-symˡ _ ⟩∎

      refl _                                                  ∎

-- A dependently typed variant of the sequential colimit's universal
-- property.

universal-property-Π :
  {@0 P₊ : ℕ → Type p₊}
  {@0 step₀ : P₀ → P₊ zero}
  {@0 step₊ : ∀ {n} → P₊ n → P₊ (suc n)}
  {Q : Colimitᴱ P₀ P₊ step₀ step₊ → Type q} →
  ((x : Colimitᴱ P₀ P₊ step₀ step₊) → Q x)
    ≃
  (∃ λ (f₀ : (x : P₀) → Q ∣ x ∣₀) →
     Erased (∃ λ (f₊ : ∀ n (x : P₊ n) → Q ∣ x ∣₊) →
               (∀ x → subst Q (∣∣₊≡∣∣₀ x) (f₊ zero (step₀ x)) ≡ f₀ x) ×
               (∀ n x → subst Q (∣∣₊≡∣∣₊ x) (f₊ (suc n) (step₊ x)) ≡
                        f₊ n x)))
universal-property-Π
  {P₀ = P₀} {P₊ = P₊} {step₀ = step₀} {step₊ = step₊} {Q = Q} =
  Eq.↔→≃ to from to∘from from∘to
  where
  RHS =
    ∃ λ (f₀ : (x : P₀) → Q ∣ x ∣₀) →
      Erased (∃ λ (f₊ : ∀ n (x : P₊ n) → Q ∣ x ∣₊) →
                (∀ x → subst Q (∣∣₊≡∣∣₀ x) (f₊ zero (step₀ x)) ≡ f₀ x) ×
                (∀ n x → subst Q (∣∣₊≡∣∣₊ x) (f₊ (suc n) (step₊ x)) ≡
                         f₊ n x))

  to : ((x : Colimitᴱ P₀ P₊ step₀ step₊) → Q x) → RHS
  to h = h ∘ ∣_∣₀
       , [ (λ _ → h ∘ ∣_∣₊)
         , (λ x →
              subst Q (∣∣₊≡∣∣₀ x) (h ∣ step₀ x ∣₊)  ≡⟨ dcong h (∣∣₊≡∣∣₀ x) ⟩∎
              h ∣ x ∣₀                              ∎)
         , (λ _ x →
              subst Q (∣∣₊≡∣∣₊ x) (h ∣ step₊ x ∣₊)  ≡⟨ dcong h (∣∣₊≡∣∣₊ x) ⟩∎
              h ∣ x ∣₊                              ∎)
         ]

  from :
    RHS → (x : Colimitᴱ P₀ P₊ step₀ step₊) → Q x
  from (f₀ , [ f₊ , g₀ , g₊ ]) = elim λ where
    .∣∣₀ʳ     → f₀
    .∣∣₊ʳ     → f₊ _
    .∣∣₊≡∣∣₀ʳ → g₀
    .∣∣₊≡∣∣₊ʳ → g₊ _

  to∘from : ∀ p → to (from p) ≡ p
  to∘from (f₀ , [ f₊ , g₀ , g₊ ]) =
    cong (f₀ ,_) $ []-cong
      [ cong (f₊ ,_) $ cong₂ _,_
          (⟨ext⟩ λ x →
             dcong (elim _) (∣∣₊≡∣∣₀ x)  ≡⟨ elim-∣∣₊≡∣∣₀ ⟩∎
             g₀ x                        ∎)
          (⟨ext⟩ λ n → ⟨ext⟩ λ x →
             dcong (elim _) (∣∣₊≡∣∣₊ x)  ≡⟨ elim-∣∣₊≡∣∣₊ ⟩∎
             g₊ n x                      ∎)
      ]

  from∘to : ∀ h → from (to h) ≡ h
  from∘to h = ⟨ext⟩ $ elim λ where
    .∣∣₀ʳ _     → refl _
    .∣∣₊ʳ _     → refl _
    .∣∣₊≡∣∣₀ʳ x →
      subst (λ z → from (to h) z ≡ h z) (∣∣₊≡∣∣₀ x) (refl _)   ≡⟨ subst-in-terms-of-trans-and-dcong ⟩

      trans (sym (dcong (from (to h)) (∣∣₊≡∣∣₀ x)))
        (trans (cong (subst Q (∣∣₊≡∣∣₀ x)) (refl _))
           (dcong h (∣∣₊≡∣∣₀ x)))                              ≡⟨ cong₂ (λ p q → trans (sym p) q)
                                                                    elim-∣∣₊≡∣∣₀
                                                                    (trans (cong (flip trans _) $ cong-refl _) $
                                                                     trans-reflˡ _) ⟩

      trans (sym (dcong h (∣∣₊≡∣∣₀ x))) (dcong h (∣∣₊≡∣∣₀ x))  ≡⟨ trans-symˡ _ ⟩∎

      refl _                                                   ∎
    .∣∣₊≡∣∣₊ʳ x →
      subst (λ z → from (to h) z ≡ h z) (∣∣₊≡∣∣₊ x) (refl _)   ≡⟨ subst-in-terms-of-trans-and-dcong ⟩

      trans (sym (dcong (from (to h)) (∣∣₊≡∣∣₊ x)))
        (trans (cong (subst Q (∣∣₊≡∣∣₊ x)) (refl _))
           (dcong h (∣∣₊≡∣∣₊ x)))                              ≡⟨ cong₂ (λ p q → trans (sym p) q)
                                                                    elim-∣∣₊≡∣∣₊
                                                                    (trans (cong (flip trans _) $ cong-refl _) $
                                                                     trans-reflˡ _) ⟩

      trans (sym (dcong h (∣∣₊≡∣∣₊ x))) (dcong h (∣∣₊≡∣∣₊ x))  ≡⟨ trans-symˡ _ ⟩∎

      refl _                                                   ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Agda.Builtin.Nat

data Vec (A : Set) : Nat -> Set where
  [] : Vec A 0
  cons : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

empty : Vec Nat 0
empty = []


text:
------------------------------------------------------------------------------
-- The unary numbers are FOTC total natural numbers
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.UnaryNumbers.TotalityATP where

open import FOTC.Base
open import FOTC.Data.Nat.Type
open import FOTC.Data.Nat.UnaryNumbers

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

postulate
  0-N : N 0'
  1-N : N 1'
  2-N : N 2'
  3-N : N 3'
  4-N : N 4'
  5-N : N 5'
{-# ATP prove 0-N #-}
{-# ATP prove 1-N #-}
{-# ATP prove 2-N #-}
{-# ATP prove 3-N #-}
{-# ATP prove 4-N #-}
{-# ATP prove 5-N #-}

postulate
  10-N : N 10'
  11-N : N 11'
{-# ATP prove 10-N #-}
{-# ATP prove 11-N #-}

postulate 89-N : N 89'
{-# ATP prove 89-N #-}

postulate
  90-N : N 90'
  91-N : N 91'
  92-N : N 92'
  93-N : N 93'
  94-N : N 94'
  95-N : N 95'
  96-N : N 96'
  97-N : N 97'
  98-N : N 98'
  99-N : N 99'
{-# ATP prove 90-N #-}
{-# ATP prove 91-N #-}
{-# ATP prove 92-N #-}
{-# ATP prove 93-N #-}
{-# ATP prove 94-N #-}
{-# ATP prove 95-N #-}
{-# ATP prove 96-N #-}
{-# ATP prove 97-N #-}
{-# ATP prove 98-N #-}
{-# ATP prove 99-N #-}

postulate
  100-N : N 100'
  101-N : N 101'
{-# ATP prove 100-N #-}
{-# ATP prove 101-N #-}

postulate 111-N : N 111'
{-# ATP prove 111-N #-}


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

open import Fragment.Equational.Theory

module Fragment.Equational.Model (Θ : Theory) where

open import Fragment.Equational.Model.Base Θ public
open import Fragment.Equational.Model.Synthetic Θ public
open import Fragment.Equational.Model.Properties Θ public
open import Fragment.Equational.Model.Satisfaction public

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
{-

This file contains:
  - Some alternative inductive definitions of James, and they give the same results.

  The most relevant one is called `𝕁Red` because it is much simpler.
  It has fewer constructors, among which the 2-dimensional constructor `coh`
  has a form essentially more clearer, and it avoids indexes.

-}
{-# OPTIONS --safe #-}
module Cubical.HITs.James.Inductive.Reduced where

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

open import Cubical.Data.Nat
open import Cubical.HITs.SequentialColimit
open import Cubical.HITs.James.Inductive.Base
  renaming (𝕁ames to 𝕁amesConstruction ; 𝕁ames∞ to 𝕁ames∞Construction)

private
  variable
    ℓ : Level

module _
  ((X , x₀) : Pointed ℓ) where

  infixr 5 _∷_

  -- Inductive James with fewer constructors

  data 𝕁Red : Type ℓ where
    [] : 𝕁Red
    _∷_  : X → 𝕁Red → 𝕁Red
    unit : (x : X)(xs : 𝕁Red) → x₀ ∷ x ∷ xs ≡ x ∷ x₀ ∷ xs
    coh  : (xs : 𝕁Red) → refl ≡ unit x₀ xs

  data 𝕁Red∞ : Type ℓ where
    inl : 𝕁Red → 𝕁Red∞
    push : (xs : 𝕁Red) → inl xs ≡ inl (x₀ ∷ xs)

  -- Auxiliary constructions
  -- The following square of types is defined as HIT over I × I.
  -- Notice that the constructor `incl∷` can be seen parametrized by i, `coh` by both i j,
  -- and other constructors are constant.

  data 𝕁Square (i j : I) : Type ℓ where
    []    : 𝕁Square i j
    _∷_   : X → 𝕁Square i j → 𝕁Square i j
    incl  : 𝕁Square i j → 𝕁Square i j
    unit  : (xs : 𝕁Square i j) → incl xs ≡ x₀ ∷ xs
    incl∷ : (x : X)(xs : 𝕁Square i j) → unit (x ∷ xs) i ≡ x ∷ unit xs i
    coh   : (xs : 𝕁Square i j) →
      PathP (λ k → unit (unit xs (i ∨ k)) i ≡ unit (unit xs i) (i ∨ j ∨ k))
            (λ k → unit (unit xs i) (i ∨ j ∧ k)) (incl∷ x₀ xs)

  -- What we need actually is its diagonal.
  𝕁Path : I → Type ℓ
  𝕁Path i = 𝕁Square i (~ i)

  -- If you expand the very definition at end points,
  -- you will find that `𝕁Red` is almost a deformation retraction of `𝕁1`,
  -- and `𝕁0` is almost the same as the original inductive definition of James.
  -- That explains why the isomorphisms given bellow are mainly of c-c, c-v and refls.
  𝕁0 = 𝕁Path i0
  𝕁1 = 𝕁Path i1

  data 𝕁Path∞ (i : I) : Type ℓ where
    inl : 𝕁Path i → 𝕁Path∞ i
    push : (xs : 𝕁Path i) → inl xs ≡ inl (unit xs i)

  𝕁0∞ = 𝕁Path∞ i0
  𝕁1∞ = 𝕁Path∞ i1

  -- The equivalence 𝕁1 ≃ 𝕁Red
  -- This part reduces the constructors.

  𝕁1→𝕁Red : 𝕁1 → 𝕁Red
  𝕁1→𝕁Red [] = []
  𝕁1→𝕁Red (x ∷ xs) = x ∷ 𝕁1→𝕁Red xs
  𝕁1→𝕁Red (incl xs) = x₀ ∷ 𝕁1→𝕁Red xs
  𝕁1→𝕁Red (incl∷ x xs i) = unit x (𝕁1→𝕁Red xs) i
  𝕁1→𝕁Red (unit xs i) = x₀ ∷ 𝕁1→𝕁Red xs
  𝕁1→𝕁Red (coh xs i j) = coh (𝕁1→𝕁Red xs) i j

  𝕁Red→𝕁1 : 𝕁Red → 𝕁1
  𝕁Red→𝕁1 [] = []
  𝕁Red→𝕁1 (x ∷ xs) = x ∷ 𝕁Red→𝕁1 xs
  𝕁Red→𝕁1 (unit x xs i) = incl∷ x (𝕁Red→𝕁1 xs) i
  𝕁Red→𝕁1 (coh xs i j) = coh (𝕁Red→𝕁1 xs) i j

  𝕁Red→𝕁1→𝕁Red : (xs : 𝕁Red) → 𝕁1→𝕁Red (𝕁Red→𝕁1 xs) ≡ xs
  𝕁Red→𝕁1→𝕁Red [] = refl
  𝕁Red→𝕁1→𝕁Red (x ∷ xs) t = x ∷ 𝕁Red→𝕁1→𝕁Red xs t
  𝕁Red→𝕁1→𝕁Red (unit x xs i) t = unit x (𝕁Red→𝕁1→𝕁Red xs t) i
  𝕁Red→𝕁1→𝕁Red (coh xs i j) t = coh (𝕁Red→𝕁1→𝕁Red xs t) i j

  𝕁1→𝕁Red→𝕁1 : (xs : 𝕁1) → 𝕁Red→𝕁1 (𝕁1→𝕁Red xs) ≡ xs
  𝕁1→𝕁Red→𝕁1 [] = refl
  𝕁1→𝕁Red→𝕁1 (x ∷ xs) t = x ∷ 𝕁1→𝕁Red→𝕁1 xs t
  𝕁1→𝕁Red→𝕁1 (incl xs) = (λ t → x₀ ∷ 𝕁1→𝕁Red→𝕁1 xs t) ∙ sym (unit xs)
  𝕁1→𝕁Red→𝕁1 (incl∷ x xs i) t = incl∷ x (𝕁1→𝕁Red→𝕁1 xs t) i
  𝕁1→𝕁Red→𝕁1 (unit xs i) j =
    hcomp (λ k → λ
      { (i = i0) → compPath-filler (λ t → x₀ ∷ 𝕁1→𝕁Red→𝕁1 xs t) (sym (unit xs)) k j
      ; (i = i1) → x₀ ∷ 𝕁1→𝕁Red→𝕁1 xs j
      ; (j = i0) → x₀ ∷ 𝕁Red→𝕁1 (𝕁1→𝕁Red xs)
      ; (j = i1) → unit xs (i ∨ ~ k)})
    (x₀ ∷ 𝕁1→𝕁Red→𝕁1 xs j)
  𝕁1→𝕁Red→𝕁1 (coh xs i j) t = coh (𝕁1→𝕁Red→𝕁1 xs t) i j

  𝕁Red∞→𝕁1∞ : 𝕁Red∞ → 𝕁1∞
  𝕁Red∞→𝕁1∞ (inl xs) = inl (𝕁Red→𝕁1 xs)
  𝕁Red∞→𝕁1∞ (push xs i) = push (𝕁Red→𝕁1 xs) i

  𝕁1∞→𝕁Red∞ : 𝕁1∞ → 𝕁Red∞
  𝕁1∞→𝕁Red∞ (inl xs) = inl (𝕁1→𝕁Red xs)
  𝕁1∞→𝕁Red∞ (push xs i) = push (𝕁1→𝕁Red xs) i

  𝕁Red∞→𝕁1∞→𝕁Red∞ : (xs : 𝕁Red∞) → 𝕁1∞→𝕁Red∞ (𝕁Red∞→𝕁1∞ xs) ≡ xs
  𝕁Red∞→𝕁1∞→𝕁Red∞ (inl xs) t = inl (𝕁Red→𝕁1→𝕁Red xs t)
  𝕁Red∞→𝕁1∞→𝕁Red∞ (push xs i) t = push (𝕁Red→𝕁1→𝕁Red xs t) i

  𝕁1∞→𝕁Red∞→𝕁1∞ : (xs : 𝕁1∞) → 𝕁Red∞→𝕁1∞ (𝕁1∞→𝕁Red∞ xs) ≡ xs
  𝕁1∞→𝕁Red∞→𝕁1∞ (inl xs) t = inl (𝕁1→𝕁Red→𝕁1 xs t)
  𝕁1∞→𝕁Red∞→𝕁1∞ (push xs i) t = push (𝕁1→𝕁Red→𝕁1 xs t) i

  𝕁1∞≃𝕁Red∞ : 𝕁1∞ ≃ 𝕁Red∞
  𝕁1∞≃𝕁Red∞ = isoToEquiv (iso 𝕁1∞→𝕁Red∞ 𝕁Red∞→𝕁1∞ 𝕁Red∞→𝕁1∞→𝕁Red∞ 𝕁1∞→𝕁Red∞→𝕁1∞)

  -- The equivalence 𝕁ames ≃ 𝕁0
  -- This part removes the indexes.

  private
    𝕁ames  = 𝕁amesConstruction  (X , x₀)
    𝕁ames∞ = 𝕁ames∞Construction (X , x₀)

  index : 𝕁0 → ℕ
  index [] = 0
  index (x ∷ xs) = 1 + index xs
  index (incl xs) = 1 + index xs
  index (incl∷ x xs i) = 2 + index xs
  index (unit xs i) = 1 + index xs
  index (coh xs i j) = 2 + index xs

  𝕁ames→𝕁0 : {n : ℕ} → 𝕁ames n → 𝕁0
  𝕁ames→𝕁0 [] = []
  𝕁ames→𝕁0 (x ∷ xs) = x ∷ 𝕁ames→𝕁0 xs
  𝕁ames→𝕁0 (incl xs) = incl (𝕁ames→𝕁0 xs)
  𝕁ames→𝕁0 (incl∷ x xs i) = incl∷ x (𝕁ames→𝕁0 xs) i
  𝕁ames→𝕁0 (unit xs i) = unit (𝕁ames→𝕁0 xs) i
  𝕁ames→𝕁0 (coh xs i j) = coh (𝕁ames→𝕁0 xs) i j

  𝕁0→𝕁ames : (xs : 𝕁0) → 𝕁ames (index xs)
  𝕁0→𝕁ames [] = []
  𝕁0→𝕁ames (x ∷ xs) = x ∷ 𝕁0→𝕁ames xs
  𝕁0→𝕁ames (incl xs) = incl (𝕁0→𝕁ames xs)
  𝕁0→𝕁ames (incl∷ x xs i) = incl∷ x (𝕁0→𝕁ames xs) i
  𝕁0→𝕁ames (unit xs i) = unit (𝕁0→𝕁ames xs) i
  𝕁0→𝕁ames (coh xs i j) = coh (𝕁0→𝕁ames xs) i j

  𝕁0→𝕁ames→𝕁0 : (xs : 𝕁0) → 𝕁ames→𝕁0 (𝕁0→𝕁ames xs) ≡ xs
  𝕁0→𝕁ames→𝕁0 [] = refl
  𝕁0→𝕁ames→𝕁0 (x ∷ xs) t = x ∷ 𝕁0→𝕁ames→𝕁0 xs t
  𝕁0→𝕁ames→𝕁0 (incl xs) t = incl (𝕁0→𝕁ames→𝕁0 xs t)
  𝕁0→𝕁ames→𝕁0 (incl∷ x xs i) t = incl∷ x (𝕁0→𝕁ames→𝕁0 xs t) i
  𝕁0→𝕁ames→𝕁0 (unit xs i) t = unit (𝕁0→𝕁ames→𝕁0 xs t) i
  𝕁0→𝕁ames→𝕁0 (coh xs i j) t = coh (𝕁0→𝕁ames→𝕁0 xs t) i j

  index-path : {n : ℕ}(xs : 𝕁ames n) → index (𝕁ames→𝕁0 xs) ≡ n
  index-path [] = refl
  index-path (x ∷ xs) t = 1 + index-path xs t
  index-path (incl xs) t = 1 + index-path xs t
  index-path (incl∷ x xs i) t = 2 + index-path xs t
  index-path (unit xs i) t = 1 + index-path xs t
  index-path (coh xs i j) t = 2 + index-path xs t

  𝕁ames→𝕁0→𝕁ames : {n : ℕ}(xs : 𝕁ames n)
    → PathP (λ i → 𝕁ames (index-path xs i)) (𝕁0→𝕁ames (𝕁ames→𝕁0 xs)) xs
  𝕁ames→𝕁0→𝕁ames [] = refl
  𝕁ames→𝕁0→𝕁ames (x ∷ xs) t = x ∷ 𝕁ames→𝕁0→𝕁ames xs t
  𝕁ames→𝕁0→𝕁ames (incl xs) t = incl (𝕁ames→𝕁0→𝕁ames xs t)
  𝕁ames→𝕁0→𝕁ames (incl∷ x xs i) t = incl∷ x (𝕁ames→𝕁0→𝕁ames xs t) i
  𝕁ames→𝕁0→𝕁ames (unit xs i) t = unit (𝕁ames→𝕁0→𝕁ames xs t) i
  𝕁ames→𝕁0→𝕁ames (coh xs i j) t = coh (𝕁ames→𝕁0→𝕁ames xs t) i j

  𝕁ames∞→𝕁0∞ : 𝕁ames∞ → 𝕁0∞
  𝕁ames∞→𝕁0∞ (inl xs) = inl (𝕁ames→𝕁0 xs)
  𝕁ames∞→𝕁0∞ (push xs i) = push (𝕁ames→𝕁0 xs) i

  𝕁0∞→𝕁ames∞ : 𝕁0∞ → 𝕁ames∞
  𝕁0∞→𝕁ames∞ (inl xs) = inl (𝕁0→𝕁ames xs)
  𝕁0∞→𝕁ames∞ (push xs i) = push (𝕁0→𝕁ames xs) i

  𝕁ames∞→𝕁0∞→𝕁ames∞ : (xs : 𝕁ames∞) → 𝕁0∞→𝕁ames∞ (𝕁ames∞→𝕁0∞ xs) ≡ xs
  𝕁ames∞→𝕁0∞→𝕁ames∞ (inl xs) t = inl (𝕁ames→𝕁0→𝕁ames xs t)
  𝕁ames∞→𝕁0∞→𝕁ames∞ (push xs i) t = push (𝕁ames→𝕁0→𝕁ames xs t) i

  𝕁0∞→𝕁ames∞→𝕁0∞ : (xs : 𝕁0∞) → 𝕁ames∞→𝕁0∞ (𝕁0∞→𝕁ames∞ xs) ≡ xs
  𝕁0∞→𝕁ames∞→𝕁0∞ (inl xs) t = inl (𝕁0→𝕁ames→𝕁0 xs t)
  𝕁0∞→𝕁ames∞→𝕁0∞ (push xs i) t = push (𝕁0→𝕁ames→𝕁0 xs t) i

  𝕁ames∞≃𝕁0∞ : 𝕁ames∞ ≃ 𝕁0∞
  𝕁ames∞≃𝕁0∞ = isoToEquiv (iso 𝕁ames∞→𝕁0∞ 𝕁0∞→𝕁ames∞ 𝕁0∞→𝕁ames∞→𝕁0∞ 𝕁ames∞→𝕁0∞→𝕁ames∞)

  -- The main equivalence:

  𝕁ames∞≃𝕁Red∞ : 𝕁ames∞ ≃ 𝕁Red∞
  𝕁ames∞≃𝕁Red∞ = compEquiv 𝕁ames∞≃𝕁0∞ (compEquiv (pathToEquiv (λ i → 𝕁Path∞ i)) 𝕁1∞≃𝕁Red∞)

  -- Test of canonicity
  private
    -- It's good for [].
    eq1 : 𝕁ames∞≃𝕁Red∞ .fst (inl []) ≡ inl []
    eq1 = refl

    -- Without regularity, "obvious" equality doesn't hold definitionally.
    eq2 : (x : X) → 𝕁ames∞≃𝕁Red∞ .fst (inl (x ∷ [])) ≡ inl (x ∷ [])
    eq2 _ = transportRefl _

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

module Issue3256.B where

f : (a : Set) -> a -> a
f a y = {!!} y


text:
module examplesPaperJFP.SpaceShipAdvanced where

open import SizedIO.Base
open import StateSizedIO.GUI.BaseStateDependent

open import Data.Bool.Base
open import Data.List.Base
open import Data.Integer

open import Data.Product hiding (map)
open import SizedIO.Object
open import SizedIO.IOObject

open import NativeIO
open import Size

open import StateSizedIO.GUI.WxBindingsFFI
open import StateSizedIO.GUI.VariableList

open import StateSizedIO.GUI.WxGraphicsLib

open import StateSized.GUI.BitMaps

data GraphicServerMethod : Set where
  onPaintM               :   DC     →  Rect → GraphicServerMethod
  moveSpaceShipM         :   Frame  →  GraphicServerMethod
  callRepaintM           :   Frame  →  GraphicServerMethod

GraphicServerResult : GraphicServerMethod  →  Set
GraphicServerResult _ = Unit

GraphicServerInterface : Interface
Method  GraphicServerInterface  =  GraphicServerMethod
Result  GraphicServerInterface  =  GraphicServerResult

GraphicServerObject : ∀{i} → Set
GraphicServerObject {i} = IOObject GuiLev1Interface GraphicServerInterface i

graphicServerObject : ∀{i} → ℤ → GraphicServerObject {i}
method (graphicServerObject z) (onPaintM dc rect) =
            exec (drawBitmap dc ship (z , (+ 150)) true) λ _ →
            return (unit , graphicServerObject z)
method (graphicServerObject z) (moveSpaceShipM fra) =
            return (unit , graphicServerObject (z + (+ 20)))
method (graphicServerObject z) (callRepaintM fra) =
            exec (repaint fra)                λ _ →
            return (unit , graphicServerObject z)

VarType = GraphicServerObject {∞}

varInit : VarType
varInit = graphicServerObject (+ 150)

onPaint  : ∀{i} → VarType   → DC → Rect → IO GuiLev1Interface i VarType
onPaint obj dc rect = mapIO proj₂  (method obj (onPaintM dc rect))

moveSpaceShip : ∀{i} → Frame → VarType  → IO GuiLev1Interface i VarType
moveSpaceShip fra obj =  mapIO proj₂ (method obj (moveSpaceShipM fra))

callRepaint  : ∀{i} → Frame → VarType  → IO GuiLev1Interface i VarType
callRepaint fra obj = mapIO proj₂ (method obj (callRepaintM fra))

buttonHandler : ∀{i} → Frame → List (VarType  → IO GuiLev1Interface i VarType)
buttonHandler fra = moveSpaceShip fra ∷ [ callRepaint fra ]

program : ∀{i} → IOˢ GuiLev2Interface i (λ _ → Unit) []
program =  execˢ  (level1C makeFrame)           λ fra →
           execˢ  (level1C (makeButton fra))    λ bt →
           execˢ  (level1C (addButton fra bt))  λ _ →
           execˢ  (createVar varInit)     λ _ →
           execˢ  (setButtonHandler bt
                (moveSpaceShip fra ∷ [ callRepaint fra ])) λ _ →
           execˢ  (setOnPaint fra [ onPaint  ])
           returnˢ

main : NativeIO Unit
main = start (translateLev2 program)

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

pattern plus-two n = suc (suc n)

f : Nat → Nat
f (plus-two n) = f n
f (suc zero) = plus-two zero
f zero = zero