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

module finiteSetUtil  where

open import Data.Nat hiding ( _≟_ )
open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ )
open import Data.Fin.Properties hiding ( <-trans ) renaming ( <-cmp to <-fcmp )
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality
open import logic
open import nat
open import finiteSet
open import fin
open import Data.Nat.Properties as NatP  hiding ( _≟_ )
open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )

record Found ( Q : Set ) (p : Q → Bool ) : Set where
     field
       found-q : Q
       found-p : p found-q ≡ true

open Bijection

open import Axiom.Extensionality.Propositional
open import Level hiding (suc ; zero)
postulate f-extensionality : { n : Level}  → Axiom.Extensionality.Propositional.Extensionality n n -- (Level.suc n)

module _ {Q : Set } (F : FiniteSet Q) where
     open FiniteSet F
     equal?-refl  : { x : Q } → equal? x x ≡ true
     equal?-refl {x} with F←Q x ≟ F←Q x
     ... | yes refl = refl
     ... | no ne = ⊥-elim (ne refl)
     equal→refl  : { x y : Q } → equal? x y ≡ true → x ≡ y
     equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1
     equal→refl {q0} {q1} refl | yes eq = begin
            q0
        ≡⟨ sym ( finiso→ q0) ⟩
            Q←F (F←Q q0)
        ≡⟨ cong (λ k → Q←F k ) eq ⟩
            Q←F (F←Q q1)
        ≡⟨  finiso→   q1 ⟩
            q1
        ∎  where open ≡-Reasoning
     eqP : (x y : Q) → Dec ( x ≡ y )
     eqP x y with F←Q x ≟ F←Q y
     ... | yes eq = yes (subst₂ (λ j k → j ≡ k ) (finiso→ x) (finiso→ y) (cong Q←F eq) )
     ... | no n = no (λ eq → n (cong F←Q eq))
     End : (m : ℕ ) → (p : Q → Bool ) → Set
     End m p = (i : Fin finite) → m ≤ toℕ i → p (Q←F i )  ≡ false
     first-end :  ( p : Q → Bool ) → End finite p
     first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {finite} {i}) )
     next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p
              → (m<n : m < finite ) → p (Q←F (fromℕ< m<n )) ≡ false
              → End m p
     next-end {m} p prev m<n np i m<i with NatP.<-cmp m (toℕ i)
     next-end p prev m<n np i m<i | tri< a ¬b ¬c = prev i a
     next-end p prev m<n np i m<i | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c )
     next-end {m} p prev m<n np i m<i | tri≈ ¬a b ¬c = subst ( λ k → p (Q←F k) ≡ false) (m<n=i i b m<n ) np where
              m<n=i : {n : ℕ } (i : Fin n) {m : ℕ } → m ≡ (toℕ i) → (m<n : m < n )  → fromℕ< m<n ≡ i
              m<n=i i refl m<n = fromℕ<-toℕ i m<n
     found : { p : Q → Bool } → (q : Q ) → p q ≡ true → exists p ≡ true
     found {p} q pt = found1 finite  (NatP.≤-refl ) ( first-end p ) where
         found1 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → ((i : Fin finite) → m ≤ toℕ i → p (Q←F i )  ≡ false ) →  exists1 m m<n p ≡ true
         found1 0 m<n end = ⊥-elim ( ¬-bool (subst (λ k → k ≡ false ) (cong (λ k → p k) (finiso→ q) ) (end (F←Q q) z≤n )) pt )
         found1 (suc m)  m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true
         found1 (suc m)  m<n end | yes eq = subst (λ k → k \/ exists1 m (<to≤  m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (<to≤  m<n) p} )
         found1 (suc m)  m<n end | no np = begin
                 p (Q←F (fromℕ< m<n)) \/ exists1 m (<to≤  m<n) p
              ≡⟨ bool-or-1 (¬-bool-t np ) ⟩
                 exists1 m (<to≤  m<n) p
              ≡⟨ found1 m (<to≤  m<n) (next-end p end m<n (¬-bool-t np )) ⟩
                 true
              ∎  where open ≡-Reasoning
     not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false
     not-found {p} pn = not-found2 finite NatP.≤-refl where
         not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ finite ) → exists1 m m<n p ≡ false
         not-found2  zero  _ = refl
         not-found2 ( suc m ) m<n with pn (Q←F (fromℕ< {m} {finite} m<n))
         not-found2 (suc m) m<n | eq = begin
                  p (Q←F (fromℕ< m<n)) \/ exists1 m (<to≤ m<n) p
              ≡⟨ bool-or-1 eq ⟩
                  exists1 m (<to≤ m<n) p
              ≡⟨ not-found2 m (<to≤ m<n)  ⟩
                  false
              ∎  where open ≡-Reasoning
     found← : { p : Q → Bool } → exists p ≡ true → Found Q p
     found← {p} exst = found2 finite NatP.≤-refl  (first-end p ) where
         found2 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → End m p →  Found Q p
         found2 0 m<n end = ⊥-elim ( ¬-bool (not-found (λ q → end (F←Q q)  z≤n ) ) (subst (λ k → exists k ≡ true) (sym lemma) exst ) ) where
             lemma : (λ z → p (Q←F (F←Q z))) ≡ p
             lemma = f-extensionality ( λ q → subst (λ k → p k ≡ p q ) (sym (finiso→ q)) refl )
         found2 (suc m)  m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true
         found2 (suc m)  m<n end | yes eq = record { found-q = Q←F (fromℕ< m<n) ; found-p = eq }
         found2 (suc m)  m<n end | no np =
               found2 m (<to≤ m<n) (next-end p end m<n (¬-bool-t np ))
     not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false
     not-found← {p} np q = ¬-bool-t ( contra-position {_} {_} {_} {exists p ≡ true} (found q) (λ ep → ¬-bool np ep ) )

iso-fin : {A B : Set} → FiniteSet A  → Bijection A B → FiniteSet B
iso-fin {A} {B}  fin iso = record {
   Q←F = λ f → fun→ iso ( FiniteSet.Q←F fin f )
     ; F←Q = λ b → FiniteSet.F←Q fin (fun← iso b )
     ; finiso→ = finiso→
     ; finiso← = finiso←
   } where
   finiso→ : (q : B) → fun→ iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (Bijection.fun← iso q))) ≡ q
   finiso→ q = begin
             fun→ iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (Bijection.fun← iso q)))
           ≡⟨ cong (λ k → fun→ iso k ) (FiniteSet.finiso→ fin _ ) ⟩
             fun→ iso (Bijection.fun← iso q)
           ≡⟨ fiso→ iso _ ⟩
              q
           ∎  where open ≡-Reasoning
   finiso← : (f : Fin (FiniteSet.finite fin ))→ FiniteSet.F←Q fin (Bijection.fun← iso (Bijection.fun→ iso (FiniteSet.Q←F fin f))) ≡ f
   finiso← f = begin
              FiniteSet.F←Q fin (Bijection.fun← iso (Bijection.fun→ iso (FiniteSet.Q←F fin f)))
           ≡⟨ cong (λ k → FiniteSet.F←Q fin k ) (Bijection.fiso← iso _) ⟩
              FiniteSet.F←Q fin (FiniteSet.Q←F fin f)
           ≡⟨ FiniteSet.finiso← fin _  ⟩
              f
           ∎  where
           open ≡-Reasoning

data One : Set where
   one : One

fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B)
fin-∨1 {B} fb =  record {
   Q←F = Q←F
 ; F←Q =  F←Q
 ; finiso→ = finiso→
 ; finiso← = finiso←
   }  where
   b = FiniteSet.finite fb
   Q←F : Fin (suc b) → One ∨ B
   Q←F zero = case1 one
   Q←F (suc f) = case2 (FiniteSet.Q←F fb f)
   F←Q : One ∨ B → Fin (suc b)
   F←Q (case1 one) = zero
   F←Q (case2 f ) = suc (FiniteSet.F←Q fb f)
   finiso→ : (q : One ∨ B) → Q←F (F←Q q) ≡ q
   finiso→ (case1 one) = refl
   finiso→ (case2 b) = cong (λ k → case2 k ) (FiniteSet.finiso→ fb b)
   finiso← : (q : Fin (suc b)) → F←Q (Q←F q) ≡ q
   finiso← zero = refl
   finiso← (suc f) = cong ( λ k → suc k ) (FiniteSet.finiso← fb f)

fin-∨2 : {B : Set} → ( a : ℕ ) → FiniteSet B  → FiniteSet (Fin a ∨ B)
fin-∨2 {B} zero  fb = iso-fin fb iso where
 iso : Bijection B (Fin zero ∨ B)
 iso =  record {
        fun← = fun←1
      ; fun→ = λ b → case2 b
      ; fiso→ = fiso→1
      ; fiso← = λ _ → refl
    } where
     fun←1 : Fin zero ∨ B → B
     fun←1 (case2 x) = x
     fiso→1 : (f : Fin zero ∨ B ) → case2 (fun←1 f) ≡ f
     fiso→1 (case2 x)  = refl
fin-∨2 {B} (suc a) fb =  iso-fin (fin-∨1 (fin-∨2 a fb) ) iso
    where
 iso : Bijection (One ∨ (Fin a ∨ B) ) (Fin (suc a) ∨ B)
 fun← iso (case1 zero) = case1 one
 fun← iso (case1 (suc f)) = case2 (case1 f)
 fun← iso (case2 b) = case2 (case2 b)
 fun→ iso (case1 one) = case1 zero
 fun→ iso (case2 (case1 f)) = case1 (suc f)
 fun→ iso (case2 (case2 b)) = case2 b
 fiso← iso (case1 one) = refl
 fiso← iso (case2 (case1 x)) = refl
 fiso← iso (case2 (case2 x)) = refl
 fiso→ iso (case1 zero) = refl
 fiso→ iso (case1 (suc x)) = refl
 fiso→ iso (case2 x) = refl

FiniteSet→Fin : {A : Set} → (fin : FiniteSet A  ) → Bijection (Fin (FiniteSet.finite fin)) A
fun← (FiniteSet→Fin fin) f = FiniteSet.F←Q fin f
fun→ (FiniteSet→Fin fin) f = FiniteSet.Q←F fin f
fiso← (FiniteSet→Fin fin) = FiniteSet.finiso← fin
fiso→ (FiniteSet→Fin fin) =  FiniteSet.finiso→ fin

fin-∨ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∨ B)
fin-∨ {A} {B}  fa fb = iso-fin (fin-∨2 a  fb ) iso2 where
    a = FiniteSet.finite fa
    ia = FiniteSet→Fin fa
    iso2 : Bijection (Fin a ∨ B ) (A ∨ B)
    fun← iso2 (case1 x) = case1 (fun← ia x )
    fun← iso2 (case2 x) = case2 x
    fun→ iso2 (case1 x) = case1 (fun→ ia x )
    fun→ iso2 (case2 x) = case2 x
    fiso← iso2 (case1 x) = cong ( λ k → case1 k ) (Bijection.fiso← ia x)
    fiso← iso2 (case2 x) = refl
    fiso→ iso2 (case1 x) = cong ( λ k → case1 k ) (Bijection.fiso→ ia x)
    fiso→ iso2 (case2 x) = refl

open import Data.Product hiding ( map )

fin-× : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A × B)
fin-× {A} {B}  fa fb with FiniteSet→Fin fa
... | a=f = iso-fin (fin-×-f a ) iso-1 where
   a = FiniteSet.finite fa
   b = FiniteSet.finite fb
   iso-1 : Bijection (Fin a × B) ( A × B )
   fun← iso-1 x = ( FiniteSet.F←Q fa (proj₁ x)  , proj₂ x)
   fun→ iso-1 x = ( FiniteSet.Q←F fa (proj₁ x)  , proj₂ x)
   fiso← iso-1 x  =  lemma  where
     lemma : (FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj₁ x)) , proj₂ x) ≡ ( proj₁ x , proj₂ x )
     lemma = cong ( λ k → ( k ,  proj₂ x ) )  (FiniteSet.finiso← fa _ )
   fiso→ iso-1 x = cong ( λ k → ( k ,  proj₂ x ) )  (FiniteSet.finiso→ fa _ )

   iso-2 : {a : ℕ } → Bijection (B ∨ (Fin a × B)) (Fin (suc a) × B)
   fun← iso-2 (zero , b ) = case1 b
   fun← iso-2 (suc fst , b ) = case2 ( fst , b )
   fun→ iso-2 (case1 b) = ( zero , b )
   fun→ iso-2 (case2 (a , b )) = ( suc a , b )
   fiso← iso-2 (case1 x) = refl
   fiso← iso-2 (case2 x) = refl
   fiso→ iso-2 (zero , b ) = refl
   fiso→ iso-2 (suc a , b ) = refl

   fin-×-f : ( a  : ℕ ) → FiniteSet ((Fin a) × B)
   fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 }
   fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2

open _∧_

fin-∧ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∧ B)
fin-∧ {A} {B} fa fb with FiniteSet→Fin fa    -- same thing for our tool
... | a=f = iso-fin (fin-×-f a ) iso-1 where
   a = FiniteSet.finite fa
   b = FiniteSet.finite fb
   iso-1 : Bijection (Fin a ∧ B) ( A ∧ B )
   fun← iso-1 x = record { proj1 = FiniteSet.F←Q fa (proj1 x)  ; proj2 =  proj2 x}
   fun→ iso-1 x = record { proj1 = FiniteSet.Q←F fa (proj1 x)  ; proj2 =  proj2 x}
   fiso← iso-1 x  =  lemma  where
     lemma : record { proj1 = FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj1 x)) ; proj2 =  proj2 x} ≡ record {proj1 =  proj1 x ; proj2 =  proj2 x }
     lemma = cong ( λ k → record {proj1 = k ;  proj2 = proj2 x } )  (FiniteSet.finiso← fa _ )
   fiso→ iso-1 x = cong ( λ k → record {proj1 =  k ; proj2 =  proj2 x } )  (FiniteSet.finiso→ fa _ )

   iso-2 : {a : ℕ } → Bijection (B ∨ (Fin a ∧ B)) (Fin (suc a) ∧ B)
   fun← iso-2 (record { proj1 = zero ; proj2 =  b }) = case1 b
   fun← iso-2 (record { proj1 = suc fst ; proj2 =  b }) = case2 ( record { proj1 = fst ; proj2 =  b } )
   fun→ iso-2 (case1 b) = record {proj1 =  zero ; proj2 =  b }
   fun→ iso-2 (case2 (record { proj1 = a ; proj2 =  b })) = record { proj1 =  suc a ; proj2 =  b }
   fiso← iso-2 (case1 x) = refl
   fiso← iso-2 (case2 x) = refl
   fiso→ iso-2 (record { proj1 = zero ; proj2 =  b }) = refl
   fiso→ iso-2 (record { proj1 = suc a ; proj2 =  b }) = refl

   fin-×-f : ( a  : ℕ ) → FiniteSet ((Fin a) ∧ B)
   fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 }
   fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2

-- import Data.Nat.DivMod

open import Data.Vec hiding ( map ; length )
import Data.Product

exp2 : (n : ℕ ) → exp 2 (suc n) ≡ exp 2 n Data.Nat.+ exp 2 n
exp2 n = begin
      exp 2 (suc n)
   ≡⟨⟩
      2 * ( exp 2 n )
   ≡⟨ *-comm 2 (exp 2 n)  ⟩
      ( exp 2 n ) * 2
   ≡⟨ *-suc ( exp 2 n ) 1 ⟩
      (exp 2 n ) Data.Nat.+ ( exp 2 n ) * 1
   ≡⟨ cong ( λ k →  (exp 2 n ) Data.Nat.+  k ) (proj₂ *-identity (exp 2 n) ) ⟩
      exp 2 n Data.Nat.+ exp 2 n
   ∎  where
       open ≡-Reasoning
       open Data.Product

cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → cast eq ( cast (sym eq ) f)  ≡ f
cast-iso refl zero =  refl
cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f )

fin2List : {n : ℕ } → FiniteSet (Vec Bool n)
fin2List {zero} = record {
   Q←F = λ _ → Vec.[]
 ; F←Q =  λ _ → # 0
 ; finiso→ = finiso→
 ; finiso← = finiso←
   } where
   Q = Vec Bool zero
   finiso→ : (q : Q) → [] ≡ q
   finiso→ [] = refl
   finiso← : (f : Fin (exp 2 zero)) → # 0 ≡ f
   finiso← zero = refl
fin2List {suc n} = subst (λ k → FiniteSet (Vec Bool (suc n)) ) (sym (exp2 n)) ( iso-fin (fin-∨ (fin2List ) (fin2List )) iso )
    where
   QtoR : Vec Bool (suc  n) →  Vec Bool n ∨ Vec Bool n
   QtoR ( true ∷ x ) = case1 x
   QtoR ( false ∷ x ) = case2 x
   RtoQ : Vec Bool n ∨ Vec Bool n → Vec Bool (suc  n)
   RtoQ ( case1 x ) = true ∷ x
   RtoQ ( case2 x ) = false ∷ x
   isoRQ : (x : Vec Bool (suc  n) ) → RtoQ ( QtoR x ) ≡ x
   isoRQ (true ∷ _ ) = refl
   isoRQ (false ∷ _ ) = refl
   isoQR : (x : Vec Bool n ∨ Vec Bool n ) → QtoR ( RtoQ x ) ≡ x
   isoQR (case1 x) = refl
   isoQR (case2 x) = refl
   iso : Bijection (Vec Bool n ∨ Vec Bool n) (Vec Bool (suc n))
   iso = record { fun← = QtoR ; fun→ = RtoQ ; fiso← = isoQR ; fiso→ = isoRQ  }

F2L : {Q : Set } {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → ( (q : Q) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool ) → Vec Bool n
F2L  {Q} {zero} fin _ Q→B = []
F2L  {Q} {suc n} fin (s≤s n<m) Q→B = Q→B (FiniteSet.Q←F fin (fromℕ< n<m)) lemma6 ∷ F2L {Q} fin (NatP.<-trans n<m a<sa ) qb1 where
   lemma6 : toℕ (FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m))) < suc n
   lemma6 = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fin _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ< n<m ))  a<sa )
   qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool
   qb1 q q<n = Q→B q (NatP.<-trans q<n a<sa)

List2Func : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin)  → Vec Bool n →  Q → Bool
List2Func {Q} {zero} fin (s≤s z≤n) [] q = false
List2Func {Q} {suc n} fin (s≤s n<m) (h ∷ t) q with  FiniteSet.F←Q fin q ≟ fromℕ< n<m
... | yes _ = h
... | no _ = List2Func {Q} fin (NatP.<-trans n<m a<sa ) t q

open import Level renaming ( suc to Suc ; zero to Zero)
open import Axiom.Extensionality.Propositional
-- postulate f-extensionality : { n : Level}  →  Axiom.Extensionality.Propositional.Extensionality n n

F2L-iso : { Q : Set } → (fin : FiniteSet Q ) → (x : Vec Bool (FiniteSet.finite fin) ) → F2L fin a<sa (λ q _ → List2Func fin a<sa x q ) ≡ x
F2L-iso {Q} fin x = f2l m a<sa x where
  m = FiniteSet.finite fin
  f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → F2L fin n<m (λ q q<n → List2Func fin n<m x q )  ≡ x
  f2l zero (s≤s z≤n) [] = refl
  f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3f where
    lemma1 : {n : ℕ } → {h h1 : Bool } → {t t1 : Vec Bool n } → h ≡ h1 → t ≡ t1 →  h ∷ t ≡ h1 ∷ t1
    lemma1 refl refl = refl
    lemma2 : List2Func fin (s≤s n<m) (h ∷ t) (FiniteSet.Q←F fin (fromℕ< n<m)) ≡ h
    lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m))  ≟ fromℕ< n<m
    lemma2 | yes p = refl
    lemma2 | no ¬p = ⊥-elim ( ¬p (FiniteSet.finiso← fin _) )
    lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func fin (s≤s n<m) (h ∷ t) q ≡ List2Func fin (NatP.<-trans n<m a<sa) t q
    lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ< n<m
    lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ< n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where
        lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n
        lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s  z≤n
        lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl)
    lemma4 q _ | no ¬p = refl
    lemma3f :  F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q  ) ≡ t
    lemma3f = begin
         F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q )
       ≡⟨ cong (λ k → F2L fin (NatP.<-trans n<m a<sa) ( λ q q<n → k q q<n ))
              (f-extensionality ( λ q →
              (f-extensionality ( λ q<n →  lemma4 q q<n )))) ⟩
         F2L fin (NatP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NatP.<-trans n<m a<sa) t q )
       ≡⟨ f2l n (NatP.<-trans n<m a<sa ) t ⟩
         t
       ∎  where
         open ≡-Reasoning

L2F : {Q : Set } {n : ℕ } → (fin : FiniteSet Q )  → n < suc (FiniteSet.finite fin) → Vec Bool n → (q :  Q ) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool
L2F fin n<m x q q<n = List2Func fin n<m x q

L2F-iso : { Q : Set } → (fin : FiniteSet Q ) → (f : Q → Bool ) → (q : Q ) → (L2F fin a<sa (F2L fin a<sa (λ q _ → f q) )) q (toℕ<n _) ≡ f q
L2F-iso {Q} fin f q = l2f m a<sa (toℕ<n _) where
  m = FiniteSet.finite fin
  lemma11f : {n : ℕ } → (n<m : n < m )  → ¬ ( FiniteSet.F←Q fin q ≡ fromℕ< n<m ) → toℕ (FiniteSet.F←Q fin q) ≤ n → toℕ (FiniteSet.F←Q fin q) < n
  lemma11f  n<m ¬q=n q≤n = lemma13 n<m (contra-position (lemma12 n<m _) ¬q=n ) q≤n where
     lemma13 : {n nq : ℕ } → (n<m : n < m )  → ¬ ( nq ≡ n ) → nq  ≤ n → nq < n
     lemma13 {0} {0} (s≤s z≤n) nt z≤n = ⊥-elim ( nt refl )
     lemma13 {suc _} {0} (s≤s (s≤s n<m)) nt z≤n = s≤s z≤n
     lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (NatP.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n)
     lemma3f : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt)
     lemma3f (s≤s lt) = refl
     lemma12f : {n m : ℕ } → (n<m : n < m ) → (f : Fin m )  → toℕ f ≡ n → f ≡ fromℕ< n<m
     lemma12f {zero} {suc m} (s≤s z≤n) zero refl = refl
     lemma12f {suc n} {suc m} (s≤s n<m) (suc f) refl = subst ( λ k → suc f ≡ k ) (sym (lemma3f n<m) ) ( cong ( λ k → suc k ) ( lemma12f {n} {m} n<m f refl  ) )
  l2f :  (n : ℕ ) → (n<m : n < suc m ) → (q<n : toℕ (FiniteSet.F←Q fin q ) < n )  →  (L2F fin n<m (F2L fin n<m  (λ q _ → f q))) q q<n ≡ f q
  l2f zero (s≤s z≤n) ()
  l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ< n<m
  l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p = begin
        f (FiniteSet.Q←F fin (fromℕ< n<m))
     ≡⟨ cong ( λ k → f (FiniteSet.Q←F fin k )) (sym p)  ⟩
        f (FiniteSet.Q←F fin ( FiniteSet.F←Q fin q ))
     ≡⟨ cong ( λ k → f k ) (FiniteSet.finiso→ fin _ ) ⟩
        f q
     ∎  where
       open ≡-Reasoning
  l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (NatP.<-trans n<m a<sa) (lemma11f n<m ¬p n<q)

fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool )
fin→ {A}  fin = iso-fin fin2List iso where
    a = FiniteSet.finite fin
    iso : Bijection (Vec Bool a ) (A → Bool)
    fun← iso x = F2L fin a<sa ( λ q _ → x q )
    fun→ iso x = List2Func fin a<sa x
    fiso← iso x  =  F2L-iso fin x
    fiso→ iso x = lemma where
      lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → x q)) ≡ x
      lemma = f-extensionality ( λ q → L2F-iso fin x q )

Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n)
Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }

data fin-less { n : ℕ } { A : Set }  (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa ) : Set where
  elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → fin-less fa n<m

get-elm : { n : ℕ }  { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa } → fin-less fa n<m → A
get-elm (elm1 a _ ) = a

get-< : { n : ℕ }  { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa }→ (f : fin-less fa n<m ) → toℕ (FiniteSet.F←Q fa (get-elm f )) < n
get-< (elm1 _ b ) = b

fin-less-cong : { n : ℕ }  { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa )
   → (x y : fin-less fa n<m ) → get-elm {n} {A} {fa} x ≡ get-elm {n} {A} {fa} y → get-< x ≅  get-< y → x ≡ y
fin-less-cong fa n<m (elm1 elm x) (elm1 elm x) refl HE.refl = refl

fin-< : {A : Set} → { n : ℕ } → (fa : FiniteSet A ) → (n<m : n < FiniteSet.finite fa ) → FiniteSet (fin-less fa n<m )
fin-< {A}  {n} fa n<m = iso-fin (Fin2Finite n) iso where
    m = FiniteSet.finite fa
    iso : Bijection (Fin n) (fin-less fa n<m )
    lemma8f : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n
    lemma8f {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
    lemma8f {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8f {i} {i}  refl  )
    lemma10f : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
    lemma10f  refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8f refl  ))
    lemma3f : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
    lemma3f {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8f refl)
    lemma11f : {n : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
    lemma11f {n} {x} n<m  = begin
         toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
      ≡⟨ toℕ-fromℕ< _ ⟩
         toℕ x
      ∎  where
          open ≡-Reasoning
    fun← iso (elm1 elm x) = fromℕ< x
    fun→ iso x = elm1 (FiniteSet.Q←F fa (fromℕ< (NatP.<-trans x<n n<m ))) to<n where
      x<n : toℕ x < n
      x<n = toℕ<n x
      to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ< (NatP.<-trans x<n n<m)))) < n
      to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ< (NatP.<-trans x<n n<m) )) x<n )
    fiso← iso x  = lemma2 where
      lemma2 : fromℕ< (subst (λ k → toℕ k < n) (sym
       (FiniteSet.finiso← fa (fromℕ< (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
       (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x
      lemma2 = begin
        fromℕ< (subst (λ k → toℕ k < n) (sym
          (FiniteSet.finiso← fa (fromℕ< (NatP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
               (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x)))
        ≡⟨⟩
           fromℕ< ( subst (λ k → toℕ ( k ) < n ) (sym (FiniteSet.finiso← fa _ )) lemma6 )
        ≡⟨ lemma10 (cong (λ k → toℕ k) (FiniteSet.finiso← fa _ ) ) ⟩
           fromℕ< lemma6
        ≡⟨ lemma10 (lemma11 n<m ) ⟩
           fromℕ< ( toℕ<n x )
        ≡⟨ fromℕ<-toℕ _ _ ⟩
           x
        ∎  where
          open ≡-Reasoning
          lemma6 : toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) < n
          lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ< (NatP.<-trans (toℕ<n x) n<m))) (toℕ<n x )
    fiso→ iso (elm1 elm x) = fin-less-cong fa n<m _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where
      lemma13 : toℕ (fromℕ< x) ≡ toℕ (FiniteSet.F←Q fa elm)
      lemma13 = begin
            toℕ (fromℕ< x)
         ≡⟨ toℕ-fromℕ< _ ⟩
            toℕ (FiniteSet.F←Q fa elm)
         ∎  where open ≡-Reasoning
      lemma : FiniteSet.Q←F fa (fromℕ< (NatP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m)) ≡ elm
      lemma = begin
           FiniteSet.Q←F fa (fromℕ< (NatP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m))
         ≡⟨⟩
           FiniteSet.Q←F fa (fromℕ< ( NatP.<-trans (toℕ<n ( fromℕ< x ) ) n<m))
         ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩
            FiniteSet.Q←F fa (fromℕ< ( NatP.<-trans x n<m))
         ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) (HE.≅-to-≡ (lemma8 refl)) ⟩
           FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm)))
         ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩
           FiniteSet.Q←F fa (FiniteSet.F←Q fa elm )
         ≡⟨ FiniteSet.finiso→ fa _ ⟩
            elm
         ∎  where open ≡-Reasoning

open import Data.List

open FiniteSet

memberQ : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
memberQ {Q} finq q [] = false
memberQ {Q} finq q (q0 ∷ qs) with equal? finq q q0
... | true = true
... | false = memberQ finq q qs

--
-- there is a duplicate element in finite list
--

phase2 : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
phase2 finq q [] = false
phase2 finq q (x ∷ qs) with equal? finq q x
... | true = true
... | false = phase2 finq q qs
phase1 : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
phase1 finq q [] = false
phase1 finq q (x ∷ qs) with equal? finq q x
... | true = phase2 finq q qs
... | false = phase1 finq q qs

dup-in-list : { Q : Set }  (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool
dup-in-list {Q} finq q qs = phase1 finq q qs

--
-- if length of the list is longer than kinds of a finite set, there is a duplicate
-- prove this based on the theorem on Data.Fin
--

dup-in-list+fin : { Q : Set }  (finq : FiniteSet Q)
   → (q : Q) (qs : List Q )
   → fin-dup-in-list (F←Q  finq q) (map (F←Q finq) qs) ≡ true
   → dup-in-list finq q qs ≡ true
dup-in-list+fin {Q} finq q qs p = i-phase1 qs p where
    i-phase2 : (qs : List Q) →   fin-phase2 (F←Q  finq q) (map (F←Q finq) qs) ≡ true
        → phase2 finq q qs ≡ true
    i-phase2 (x ∷ qs) p with equal? finq q x | inspect (equal? finq q ) x | <-fcmp  (F←Q finq q)  (F←Q finq x)
    ... | true | _ | t = refl
    ... | false | _ | tri< a ¬b ¬c = i-phase2 qs p
    ... | false | record { eq = eq }  | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq
        (subst₂ (λ j k → equal? finq j k ≡ true) (finiso→ finq q) (subst (λ k →  Q←F finq k ≡ x) (sym b) (finiso→ finq x)) ( equal?-refl finq  )))
    ... | false | _ | tri> ¬a ¬b c = i-phase2 qs p
    i-phase1 : (qs : List Q) → fin-phase1 (F←Q  finq q) (map (F←Q finq) qs) ≡ true
        → phase1 finq q qs ≡ true
    i-phase1 (x ∷ qs) p with equal? finq q x |  inspect (equal? finq q ) x | <-fcmp  (F←Q finq q)  (F←Q finq x)
    ... | true | record { eq = eq }  | tri< a ¬b ¬c =  ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) ( equal→refl finq eq )) a )
    ... | true | _ | tri≈ ¬a b ¬c = i-phase2 qs p
    ... | true | record { eq = eq}  | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) (sym ( equal→refl finq eq ))) c )
    ... | false | _ | tri< a ¬b ¬c = i-phase1 qs p
    ... | false | record {eq = eq} | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq
        (subst₂ (λ j k → equal? finq j k ≡ true) (finiso→ finq q) (subst (λ k →  Q←F finq k ≡ x) (sym b) (finiso→ finq x)) ( equal?-refl finq  )))
    ... | false | _ | tri> ¬a ¬b c = i-phase1 qs p

record Dup-in-list {Q : Set } (finq : FiniteSet Q) (qs : List Q)  : Set where
   field
      dup : Q
      is-dup : dup-in-list finq dup qs ≡ true

dup-in-list>n : {Q : Set } → (finq : FiniteSet Q) → (qs : List Q)  → (len> : length qs > finite finq ) → Dup-in-list finq qs
dup-in-list>n {Q} finq qs lt = record { dup = Q←F finq (FDup-in-list.dup dl)
  ; is-dup = dup-in-list+fin finq (Q←F finq (FDup-in-list.dup dl)) qs dl01 } where
     maplen : (qs : List Q) → length (map (F←Q finq) qs) ≡ length qs
     maplen [] = refl
     maplen (x ∷ qs) = cong suc (maplen qs)
     dl : FDup-in-list (finite finq ) (map (F←Q finq) qs)
     dl = fin-dup-in-list>n (map (F←Q finq) qs) (subst (λ k → k > finite finq ) (sym (maplen qs)) lt)
     dl01 :  fin-dup-in-list (F←Q finq (Q←F finq (FDup-in-list.dup dl))) (map (F←Q finq) qs) ≡ true
     dl01 = subst (λ k →  fin-dup-in-list k (map (F←Q finq) qs) ≡ true )
         (sym (finiso← finq _)) ( FDup-in-list.is-dup dl )

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
module STLC.Lib.MaybeElim where

open import Level
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Unit.Base
open import Data.Bool.Base
open import Data.Maybe.Base

infixl 1  _>>=ᵀ_ _>>=ᵗ_ _>>=⊤_
infixl 4  _<$>ᵗ_
infixr 1  _>=>ᵗ_
infixr 10 _<∘>ᵗ_

data _>>=ᵀ_ {α β} {A : Set α} : (mx : Maybe A) -> (∀ x -> mx ≡ just x -> Set β) -> Set β where
  nothingᵗ : ∀ {B}   ->             nothing >>=ᵀ B
  justᵗ    : ∀ {x B} -> B x refl -> just x  >>=ᵀ B

-- We could write (Set (maybe (const β) zero mx)),
-- but I don't want to introduce dependency at the type level.
FromJustᵗ : ∀ {α β} {A : Set α} {mx : Maybe A} {B : ∀ x -> mx ≡ just x -> Set β}
          -> mx >>=ᵀ B -> Set β
FromJustᵗ  nothingᵗ         = Lift ⊤
FromJustᵗ (justᵗ {x} {B} y) = B x refl

fromJustᵗ : ∀ {α β} {A : Set α} {mx : Maybe A} {B : ∀ x -> mx ≡ just x -> Set β}
          -> (yᵗ : mx >>=ᵀ B) -> FromJustᵗ yᵗ
fromJustᵗ  nothingᵗ = _
fromJustᵗ (justᵗ y) = y

_>>=ᵗ_ : ∀ {α β} {A : Set α} {B : A -> Set β}
       -> (mx : Maybe A) -> (∀ x -> B x) -> mx >>=ᵀ λ x _ -> B x
nothing >>=ᵗ f = nothingᵗ
just  x >>=ᵗ f = justᵗ (f x)

_>>=⊤_ : ∀ {α β} {A : Set α} {B : A -> Set β}
       -> (mx : Maybe A) -> (g : ∀ x -> B x) -> FromJustᵗ (mx >>=ᵗ g)
mx >>=⊤ g = fromJustᵗ $ mx >>=ᵗ g

runᵗ : ∀ {α β} {A : Set α} {mx : Maybe A} {B : ∀ x -> mx ≡ just x -> Set β} {x}
     -> mx >>=ᵀ B -> (p : mx ≡ just x) -> B x p
runᵗ (justᵗ y) refl = y

_<$>ᵗ_ : ∀ {α β γ} {A : Set α} {mx : Maybe A}
           {B : ∀ x -> mx ≡ just x -> Set β}
           {C : ∀ {x} {p : mx ≡ just x} -> B x p -> Set γ}
       -> (∀ {x} {p : mx ≡ just x} -> (y : B x p) -> C y)
       -> (yᵗ : mx >>=ᵀ B)
       -> mx >>=ᵀ λ _ -> C ∘ runᵗ yᵗ
g <$>ᵗ nothingᵗ = nothingᵗ
g <$>ᵗ justᵗ y  = justᵗ (g y)

_>=>ᵗ_ : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : ∀ {x} -> B x -> Set γ}
       -> (f : ∀ x -> Maybe (B x))
       -> (∀ {x} -> (y : B x) -> C y)
       -> ∀ x -> f x >>=ᵀ λ y _ -> C y
(f >=>ᵗ g) x = f x >>=ᵗ g

_<∘>ᵗ_ : ∀ {α β γ δ} {A : Set α} {B : A -> Set β} {f : ∀ x -> Maybe (B x)}
           {C : ∀ x y -> f x ≡ just y -> Set γ}
           {D : ∀ {x y} {p : f x ≡ just y} -> C x y p -> Set δ}
       -> (∀ {x y} {p : f x ≡ just y} -> (z : C x y p) -> D z)
       -> (g : ∀ x -> f x >>=ᵀ C x)
       -> ∀ x -> f x >>=ᵀ λ _ -> D ∘ runᵗ (g x)
(h <∘>ᵗ g) x = h <$>ᵗ g x

ext: agda

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some code related to indexed containers that uses heterogeneous
-- equality
------------------------------------------------------------------------

-- The notation and presentation here is perhaps close to those used
-- by Hancock and Hyvernat in "Programming interfaces and basic
-- topology" (2006).

{-# OPTIONS --with-K --safe --guardedness #-}

module Data.Container.Indexed.WithK where

open import Axiom.Extensionality.Heterogeneous using (Extensionality)
open import Data.Container.Indexed hiding (module PlainMorphism)
open import Data.Product as Prod hiding (map)
open import Function renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
open import Level
open import Relation.Unary using (Pred; _⊆_)
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
open import Relation.Binary.HeterogeneousEquality as H using (_≅_; refl)
open import Relation.Binary.Indexed.Heterogeneous

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

-- Equality, parametrised on an underlying relation.

Eq : ∀ {i o c r ℓ} {I : Set i} {O : Set o} (C : Container I O c r)
     (X Y : Pred I ℓ) → IREL X Y ℓ → IREL (⟦ C ⟧ X) (⟦ C ⟧ Y) _
Eq C _ _ _≈_ {o₁} {o₂} (c , k) (c′ , k′) =
  o₁ ≡ o₂ × c ≅ c′ × (∀ r r′ → r ≅ r′ → k r ≈ k′ r′)

private

  -- Note that, if propositional equality were extensional, then Eq _≅_
  -- and _≅_ would coincide.

  Eq⇒≅ : ∀ {i o c r ℓ} {I : Set i} {O : Set o}
         {C : Container I O c r} {X : Pred I ℓ} {o₁ o₂ : O}
         {xs : ⟦ C ⟧ X o₁} {ys : ⟦ C ⟧ X o₂} → Extensionality r ℓ →
         Eq C X X (λ x₁ x₂ → x₁ ≅ x₂) xs ys → xs ≅ ys
  Eq⇒≅ {xs = c , k} {.c , k′} ext (refl , refl , k≈k′) =
    H.cong (_,_ c) (ext (λ _ → refl) (λ r → k≈k′ r r refl))

setoid : ∀ {i o c r s} {I : Set i} {O : Set o} →
         Container I O c r → IndexedSetoid I s _ → IndexedSetoid O _ _
setoid C X = record
  { Carrier       = ⟦ C ⟧ X.Carrier
  ; _≈_           = _≈_
  ; isEquivalence = record
    { refl  = refl , refl , λ { r .r refl → X.refl }
    ; sym   = sym
    ; trans = λ { {_} {i = xs} {ys} {zs} → trans {_} {i = xs} {ys} {zs}  }
    }
  }
  where
  module X = IndexedSetoid X

  _≈_ : IRel (⟦ C ⟧ X.Carrier) _
  _≈_ = Eq C X.Carrier X.Carrier X._≈_

  sym : Symmetric (⟦ C ⟧ X.Carrier) _≈_
  sym {_} {._} {_ , _} {._ , _} (refl , refl , k) =
    refl , refl , λ { r .r refl → X.sym (k r r refl) }

  trans : Transitive (⟦ C ⟧ X.Carrier) _≈_
  trans {._} {_} {._} {_ , _} {._ , _} {._ , _}
    (refl , refl , k) (refl , refl , k′) =
      refl , refl , λ { r .r refl → X.trans (k r r refl) (k′ r r refl) }

------------------------------------------------------------------------
-- Functoriality

module Map where

  identity : ∀ {i o c r s} {I : Set i} {O : Set o} (C : Container I O c r)
             (X : IndexedSetoid I s _) → let module X = IndexedSetoid X in
             ∀ {o} {xs : ⟦ C ⟧ X.Carrier o} → Eq C X.Carrier X.Carrier
             X._≈_ xs (map C {X.Carrier} ⟨id⟩ xs)
  identity C X = IndexedSetoid.refl (setoid C X)

  composition : ∀ {i o c r s ℓ₁ ℓ₂} {I : Set i} {O : Set o}
                (C : Container I O c r) {X : Pred I ℓ₁} {Y : Pred I ℓ₂}
                (Z : IndexedSetoid I s _) → let module Z = IndexedSetoid Z in
                {f : Y ⊆ Z.Carrier} {g : X ⊆ Y} {o : O} {xs : ⟦ C ⟧ X o} →
                Eq C Z.Carrier Z.Carrier Z._≈_
                  (map C {Y} f (map C {X} g xs))
                  (map C {X} (f ⟨∘⟩ g) xs)
  composition C Z = IndexedSetoid.refl (setoid C Z)

------------------------------------------------------------------------
-- Plain morphisms

module PlainMorphism {i o c r} {I : Set i} {O : Set o} where

  open Data.Container.Indexed.PlainMorphism

  -- Naturality.

  Natural : ∀ {ℓ} {C₁ C₂ : Container I O c r} →
            ((X : Pred I ℓ) → ⟦ C₁ ⟧ X ⊆ ⟦ C₂ ⟧ X) → Set _
  Natural {C₁ = C₁} {C₂} m =
    ∀ {X} Y → let module Y = IndexedSetoid Y in (f : X ⊆ Y.Carrier) →
    ∀ {o} (xs : ⟦ C₁ ⟧ X o) →
      Eq C₂ Y.Carrier Y.Carrier Y._≈_
        (m Y.Carrier $ map C₁ {X} f xs) (map C₂ {X} f $ m X xs)

  -- Natural transformations.

  NT : ∀ {ℓ} (C₁ C₂ : Container I O c r) → Set _
  NT {ℓ} C₁ C₂ = ∃ λ (m : (X : Pred I ℓ) → ⟦ C₁ ⟧ X ⊆ ⟦ C₂ ⟧ X) →
                 Natural m

  -- Container morphisms are natural.

  natural : ∀ {ℓ} (C₁ C₂ : Container I O c r) (m : C₁ ⇒ C₂) → Natural {ℓ} ⟪ m ⟫
  natural _ _ m {X} Y f _ = refl , refl , λ { r .r refl → lemma (coherent m) }
    where
    module Y = IndexedSetoid Y

    lemma : ∀ {i j} (eq : i ≡ j) {x} →
            P.subst Y.Carrier eq (f x) Y.≈ f (P.subst X eq x)
    lemma refl = Y.refl

  -- In fact, all natural functions of the right type are container
  -- morphisms.

  complete : ∀ {C₁ C₂ : Container I O c r} (nt : NT C₁ C₂) →
             ∃ λ m → (X : IndexedSetoid I _ _) →
                     let module X = IndexedSetoid X in
                     ∀ {o} (xs : ⟦ C₁ ⟧ X.Carrier o) →
                     Eq C₂ X.Carrier X.Carrier X._≈_
                       (proj₁ nt X.Carrier xs) (⟪ m ⟫ X.Carrier {o} xs)
  complete {C₁} {C₂} (nt , nat) = m , (λ X xs → nat X
    (λ { (r , eq) → P.subst (IndexedSetoid.Carrier X) eq (proj₂ xs r) })
    (proj₁ xs , (λ r → r , refl)))
    where

    m : C₁ ⇒ C₂
    m = record
      { command  = λ      c₁       → proj₁        (lemma c₁)
      ; response = λ {_} {c₁}  r₂  → proj₁ (proj₂ (lemma c₁) r₂)
      ; coherent = λ {_} {c₁} {r₂} → proj₂ (proj₂ (lemma c₁) r₂)
      }
      where
      lemma : ∀ {o} (c₁ : Command C₁ o) → Σ[ c₂ ∈ Command C₂ o ]
              ((r₂ : Response C₂ c₂) → Σ[ r₁ ∈ Response C₁ c₁ ]
              next C₁ c₁ r₁ ≡ next C₂ c₂ r₂)
      lemma c₁ = nt (λ i → Σ[ r₁ ∈ Response C₁ c₁ ] next C₁ c₁ r₁ ≡ i)
                    (c₁ , λ r₁ → r₁ , refl)

  -- Composition commutes with ⟪_⟫.

  ∘-correct : {C₁ C₂ C₃ : Container I O c r}
              (f : C₂ ⇒ C₃) (g : C₁ ⇒ C₂) (X : IndexedSetoid I (c ⊔ r) _) →
              let module X = IndexedSetoid X in
              ∀ {o} {xs : ⟦ C₁ ⟧ X.Carrier o} →
              Eq C₃ X.Carrier X.Carrier X._≈_
                (⟪ f ∘ g ⟫ X.Carrier xs)
                (⟪ f ⟫ X.Carrier (⟪ g ⟫ X.Carrier xs))
  ∘-correct f g X = refl , refl , λ { r .r refl → lemma (coherent g)
                                                        (coherent f) }
    where
    module X = IndexedSetoid X

    lemma : ∀ {i j k} (eq₁ : i ≡ j) (eq₂ : j ≡ k) {x} →
      P.subst X.Carrier (P.trans eq₁ eq₂) x
      X.≈
      P.subst X.Carrier eq₂ (P.subst X.Carrier eq₁ x)
    lemma refl refl = X.refl

------------------------------------------------------------------------
-- All and any

-- Membership.

infix 4 _∈_

_∈_ : ∀ {i o c r ℓ} {I : Set i} {O : Set o}
      {C : Container I O c r} {X : Pred I (i ⊔ ℓ)} → IREL X (⟦ C ⟧ X) _
_∈_ {C = C} {X} x xs = ◇ C {X = X} ((x ≅_) ⟨∘⟩ proj₂) (-, xs)


text:
module Logic.Classical.DoubleNegated where

open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Logic.Names
open import Logic.Propositional as Constructive using (¬¬_)
import      Logic.Predicate     as Constructive
open import Logic
import      Lvl
open import Syntax.Type
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable X Y Z W : Stmt{ℓ}
private variable P : X → Stmt{ℓ}

-- Classical propositions are expressed as propositions wrapped in double negation.
-- TODO: I am not sure, but I think this works? My reasoning is the following:
-- • [¬¬]-elim ↔ excluded-middle
--     Double negation elimination is equivalent to excluded middle in constructive logic.
-- • Theory(ClassicalLogic) = Theory(ConstructiveLogic ∪ {excludedMiddle})
--     Constructive logic is classical logic without EM.
--     EM is the difference between classical and constructive.
--     • Theory(ClassicalLogic) ⊈ Theory(ConstructiveLogic)
--     • Theory(ClassicalLogic) ⊇ Theory(ConstructiveLogic)
--     This seems to be a common description of constructive logic.
-- • [¬¬]-intro ∈ Theory(ConstructiveLogic)
--     Double negation introduction exists in constructive logic.
-- • (∀φ. ¬¬¬¬φ → ¬¬φ) ∈ Theory(ConstructiveLogic)
--     Double negation elimination exists inside a double negation in constructive logic.
-- • Every natural deduction introduction/elimination rule in constructive logic can be expressed inside a double negation.
-- Therefore:
-- • Theory(ClassicalLogic) = Theory(ConstructiveLogic ∪ {[¬¬]-elim}).
-- • The theory inside double negation in constructive logic is (at least) a classical logic.
--     Because every intro/elim rule exists in there,
--     the propositions inside a double negation are at least a constructive logic.
--     But [¬¬]-elim also exists in there.
--     Therefore it is at least a classical logic.
-- This cannot be done with predicate logic because the translation for [∀] does not hold in both directions.
module _ where
  infixl 1011 •_
  infixl 1010 ¬_
  infixl 1005 _∧_
  infixl 1004 _∨_
  infixl 1000 _⟵_ _⟷_ _⟶_

  •_ : Stmt{ℓ} → Stmt
  •_ = ¬¬_

  _∧_ : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
  _∧_ = (¬¬_) ∘₂ (Constructive._∧_)

  _⟶_ : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
  _⟶_ = (¬¬_) ∘₂ (_→ᶠ_)

  _⟵_ : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
  _⟵_ = (¬¬_) ∘₂ (_←_)

  _⟷_ : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
  _⟷_ = (¬¬_) ∘₂ (Constructive._↔_)

  _∨_ : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
  _∨_ = (¬¬_) ∘₂ (Constructive._∨_)

  ⊥ : Stmt
  ⊥ = ¬¬ Constructive.⊥

  ⊤ : Stmt
  ⊤ = ¬¬ Constructive.⊤

  ¬_ : Stmt{ℓ} → Stmt
  ¬_ = (¬¬_) ∘ Constructive.¬_

  ∀ₗ : (X → Stmt{ℓ}) → Stmt
  ∀ₗ = (¬¬_) ∘ Constructive.∀ₗ ∘ ((¬¬_) ∘_)

  ∃ : (X → Stmt{ℓ}) → Stmt
  ∃ = (¬¬_) ∘ Constructive.∃

  import      Logic.Propositional.Theorems as Constructive
  import      Logic.Predicate.Theorems     as Constructive

  [→]ₗ-[¬¬]-elim : ((¬¬ X) → Y) → (X → Y)
  [→]ₗ-[¬¬]-elim = liftᵣ(Constructive.[¬¬]-intro)

  [→]ᵣ-[¬¬]-move-out : (X → (¬¬ Y)) → ¬¬(X → Y)
  [→]ᵣ-[¬¬]-move-out xnny nxy = nxy (x ↦ Constructive.[⊥]-elim(xnny x (y ↦ nxy (const y))))

  double-contrapositiveᵣ : (X → Y) → ((¬¬ X) → (¬¬ Y)) -- DoubleNegated(X → Y) → DoubleNegated(¬¬ X → ¬¬ Y)
  double-contrapositiveᵣ = Constructive.contrapositiveᵣ ∘ Constructive.contrapositiveᵣ

  [¬¬]-double-contrapositiveₗ : ¬¬(X → Y) ← ((¬¬ X) → (¬¬ Y))
  [¬¬]-double-contrapositiveₗ p = [→]ᵣ-[¬¬]-move-out ([→]ₗ-[¬¬]-elim p)

  -- Also called: Double-negation shift.
  [¬¬][→]-preserving : ¬¬(X → Y) Constructive.↔ ((¬¬ X) → (¬¬ Y))
  [¬¬][→]-preserving{X = X}{Y = Y} = Constructive.[↔]-intro l r where
    l : ¬¬(X → Y) ← ((¬¬ X) → (¬¬ Y))
    l = [→]ᵣ-[¬¬]-move-out ∘ [→]ₗ-[¬¬]-elim

    r : ¬¬(X → Y) → ((¬¬ X) → (¬¬ Y))
    r(nnxy)(nnx)(ny) =
      ((Constructive.[→]-elim
        ((xy ↦
          ((Constructive.[→]-elim
            ((Constructive.[→]-elim
              ((Constructive.[⊥]-elim
                ((Constructive.[→]-elim
                  ((x ↦
                    ((Constructive.[→]-elim
                      ((Constructive.[→]-elim x xy) :of: Y)
                      (ny :of: (Y → Constructive.⊥))
                    ) :of: Constructive.⊥)
                  ) :of: (X → Constructive.⊥))
                  (nnx :of: ((X → Constructive.⊥) → Constructive.⊥))
                ) :of: Constructive.⊥)
              ) :of: X)
              (xy :of: (X → Y))
            ) :of: Y)
            (ny :of: (Y → Constructive.⊥))
          ) :of: Constructive.⊥)
        ) :of: ((X → Y) → Constructive.⊥))
        (nnxy :of: ¬¬(X → Y))
      ) :of: Constructive.⊥)

  ------------------------------------------
  -- Converting theorems with implication in constructive logic to classical logic

  prop-intro : X → (¬¬ X)
  prop-intro = Constructive.[¬¬]-intro

  [→]₁-intro : (X → Y) → ((¬¬ X) → (¬¬ Y))
  [→]₁-intro = double-contrapositiveᵣ

  [→]₂-intro : (X → Y → Z) → ((¬¬ X) → (¬¬ Y) → (¬¬ Z))
  [→]₂-intro(xyz) = (Constructive.[↔]-to-[→] [¬¬][→]-preserving) ∘ ([→]₁-intro(xyz))

  [→]₃-intro : (X → Y → Z → W) → ((¬¬ X) → (¬¬ Y) → (¬¬ Z) → (¬¬ W))
  [→]₃-intro(xyzw) = (Constructive.[↔]-to-[→] [¬¬][→]-preserving) ∘₂ ([→]₂-intro(xyzw))

  ------------------------------------------
  -- Theorems

  [→][∧]-assumptionₗ : ¬¬((X Constructive.∧ Y) → Z) ← ¬¬(X → Y → Z)
  [→][∧]-assumptionₗ = [→]₁-intro(Tuple.uncurry)

  [→][∧]-assumptionᵣ : ¬¬((X Constructive.∧ Y) → Z) → ¬¬(X → Y → Z)
  [→][∧]-assumptionᵣ = [→]₁-intro(Tuple.curry)

  [¬¬]-intro : (¬¬ X) → ¬¬(¬¬ X)
  [¬¬]-intro = Constructive.[¬¬]-intro

  ------------------------------------------
  -- Conjunction (AND)

  [∧]-intro : (• X) → (• Y) → (X ∧ Y)
  [∧]-intro = [→]₂-intro Constructive.[∧]-intro

  [∧]-elimₗ : (X ∧ Y) → (• X)
  [∧]-elimₗ = [→]₁-intro Constructive.[∧]-elimₗ

  [∧]-elimᵣ : (X ∧ Y) → (• Y)
  [∧]-elimᵣ = [→]₁-intro Constructive.[∧]-elimᵣ

  ------------------------------------------
  -- Implication

  [→]-elim : (X ⟶ Y) → (• X) → (• Y)
  [→]-elim = [→]₂-intro(swap Constructive.[→]-elim)

  [→]-intro : ((• X) → (• Y)) → (X ⟶ Y)
  [→]-intro = [¬¬]-double-contrapositiveₗ

  ------------------------------------------
  -- Reverse implication

  [←]-intro : ((• Y) ← (• X)) → (Y ⟵ X)
  [←]-intro = [¬¬]-double-contrapositiveₗ

  [←]-elim : (• X) → (Y ⟵ X) → (• Y)
  [←]-elim = [→]₂-intro(Constructive.[←]-elim)

  ------------------------------------------
  -- Equivalence

  [↔]-intro : ((• X) ← (• Y)) → ((• X) → (• Y)) → (X ⟷ Y)
  [↔]-intro yx xy = ([→]₂-intro(Constructive.[↔]-intro)) ([→]-intro yx) ([→]-intro xy)

  [↔]-elimₗ : (X ⟷ Y) → (• X) ← (• Y)
  [↔]-elimₗ = [→]-elim ∘ ([→]₁-intro(Constructive.[↔]-to-[←]))

  [↔]-elimᵣ : (X ⟷ Y) → (• X) → (• Y)
  [↔]-elimᵣ = [→]-elim ∘ ([→]₁-intro(Constructive.[↔]-to-[→]))

  ------------------------------------------
  -- Disjunction (OR)

  [∨]-introₗ : (• X) → (X ∨ Y)
  [∨]-introₗ = [→]₁-intro(Constructive.[∨]-introₗ)

  [∨]-introᵣ : (• Y) → (X ∨ Y)
  [∨]-introᵣ = [→]₁-intro(Constructive.[∨]-introᵣ)

  [∨]-elim : ((• X) → (• Z)) → ((• Y) → (• Z)) → (X ∨ Y) → (¬¬ Z)
  [∨]-elim xz yz = ([→]₃-intro(Constructive.[∨]-elim)) ([→]-intro xz) ([→]-intro yz)

  ------------------------------------------
  -- Bottom (false, absurdity, empty, contradiction)

  [⊥]-intro : (• X) → (¬ X) → ⊥
  [⊥]-intro = [→]₂-intro(Constructive.[⊥]-intro)

  [⊥]-elim : ⊥ → (• X)
  [⊥]-elim = [→]₁-intro(Constructive.[⊥]-elim)

  ------------------------------------------
  -- Top (true, truth, unit, validity)

  [⊤]-intro : ⊤
  [⊤]-intro = prop-intro(Constructive.[⊤]-intro)

  ------------------------------------------
  -- Negation

  [¬]-intro : ((• X) → ⊥) → (¬ X)
  [¬]-intro = ([→]₁-intro(Constructive.[¬]-intro)) ∘ [→]-intro

  [¬]-elim : ((¬ X) → ⊥) → (• X)
  [¬]-elim nnx nx = nnx (apply nx) id

  ------------------------------------------
  -- For-all quantification

  [∀]-intro : (∀{x} → • P(x)) → (∀ₗ P)
  [∀]-intro = apply

  [∀]-elim : (∀ₗ P) → ∀{x} → • P(x)
  [∀]-elim apx npx = apx(\px → apply npx px)

  ------------------------------------------
  -- Existential quantification

  [∃]-intro : ∀{x} → • P(x) → (∃ P)
  [∃]-intro {x = x} = [→]₁-intro(proof ↦ Constructive.[∃]-intro (x) ⦃ proof ⦄)

  [∃]-elim : (∀{x} → • P(x) → • X) → (∃ P) → • X
  [∃]-elim apx nnep nx = nnep (Constructive.[∃]-elim (p ↦ apx (apply p) nx))

  ------------------------------------------
  -- Theorems exclusive to classic logic (compared to constructive logic)

  [¬¬]-elim : ¬¬(¬¬ X) → (• X)
  [¬¬]-elim = Constructive.[¬¬¬]-elim

  excluded-middle : (X ∨ (Constructive.¬ X))
  excluded-middle{X = X} = Constructive.[¬¬]-excluded-middle

  [→]-disjunctive-formᵣ : (X ⟶ Y) → (Constructive.¬ X ∨ Y)
  [→]-disjunctive-formᵣ n-n-x→y n-nx∨y = (n-nx∨y ∘ Constructive.[∨]-introₗ) (n-n-x→y ∘ (n-nx∨y ∘ Constructive.[∨]-introᵣ ∘₂ apply))

  -- contrapositiveₗ : (X ⟶ Y) ← ((Constructive.¬ X) ⟵ (Constructive.¬ Y))
  -- contrapositiveₗ n-n-ny→nx = {!!}
  -- Constructive.[→]-intro ([¬¬]-elim ∘ Constructive.contrapositiveᵣ(Constructive.[→]-elim n-n-ny→nx) ∘ Constructive.[¬¬]-intro)

module _ where
  _∨ʷᵉᵃᵏ_ : Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
  X ∨ʷᵉᵃᵏ Y = Constructive.¬((Constructive.¬ X) Constructive.∧ (Constructive.¬ Y))

  [∨ʷᵉᵃᵏ]-introₗ : X → (X ∨ʷᵉᵃᵏ Y)
  [∨ʷᵉᵃᵏ]-introₗ = swap Constructive.[∧]-elimₗ

  [∨ʷᵉᵃᵏ]-introᵣ : Y → (X ∨ʷᵉᵃᵏ Y)
  [∨ʷᵉᵃᵏ]-introᵣ = swap Constructive.[∧]-elimᵣ

  [∨ʷᵉᵃᵏ]-elim : (X → Z) → (Y → Z) → DoubleNegationOn(Z) → (X ∨ʷᵉᵃᵏ Y) → Z
  [∨ʷᵉᵃᵏ]-elim xz yz nnzz xy = nnzz(nz ↦ xy(Constructive.[∧]-intro (nz ∘ xz) (nz ∘ yz)))

  ∃ʷᵉᵃᵏ : (X → Stmt{ℓ}) → Stmt
  ∃ʷᵉᵃᵏ P = Constructive.¬(∀{x} → (Constructive.¬ P(x)))

  [∃ʷᵉᵃᵏ]-intro : ∀(x) → ⦃ proof : P(x) ⦄ → (∃ʷᵉᵃᵏ P)
  [∃ʷᵉᵃᵏ]-intro _ ⦃ px ⦄ axnpx = axnpx px

  [∃ʷᵉᵃᵏ]-elim : (∀{x} → P(x) → X) → DoubleNegationOn(X) → (∃ʷᵉᵃᵏ P) → X
  [∃ʷᵉᵃᵏ]-elim axpxx nnxx ep = nnxx(ep ∘ (_∘ axpxx))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Identity
open import HoTT.Identity.Boolean
open import HoTT.Identity.Coproduct
open import HoTT.Identity.Sigma
open import HoTT.Identity.Identity
open import HoTT.Identity.Pi
open import HoTT.Identity.NaturalNumber
open import HoTT.Transport.Identity
open import HoTT.Equivalence
open import HoTT.Equivalence.Lift
open import HoTT.Equivalence.Transport
open import HoTT.Homotopy

module HoTT.HLevel where

open variables
private variable n : ℕ

isContr : 𝒰 i → 𝒰 i
isContr A = Σ[ a ∶ A ] Π[ x ∶ A ] (a == x)

-- Use a record so that we can use instances (technique from HoTT-Agda)
record hlevel (n : ℕ) (A : 𝒰 i) : 𝒰 i

hlevel-type : ℕ → 𝒰 i → 𝒰 i
hlevel-type zero = isContr
hlevel-type (succ n) A = {x y : A} → hlevel n (x == y)

record hlevel n A where
  inductive
  eta-equality
  constructor hlevel-in
  field hlevel-out : hlevel-type n A
open hlevel public

center : ⦃ hlevel 0 A ⦄ → A
center ⦃ hlevel-in (c , _) ⦄ = c

contr : ⦃ _ : hlevel 0 A ⦄ {x : A} → center == x
contr ⦃ hlevel-in (_ , p) ⦄ = p _

isProp : 𝒰 i → 𝒰 i
isProp A = (x y : A) → x == y

record hlevel𝒰 (n : ℕ) (i : _) : 𝒰 (lsuc i) where
  constructor type
  infix 90 _ty
  field
    _ty : 𝒰 i
    ⦃ h ⦄ : hlevel n _ty
open hlevel𝒰 using (_ty) public

Prop𝒰 = hlevel𝒰 1
Prop𝒰₀ = Prop𝒰 lzero

isSet : 𝒰 i → 𝒰 i
isSet A = {x y : A} → isProp (x == y)

Set𝒰 = hlevel𝒰 2
Set𝒰₀ = Set𝒰 lzero

instance
  =-hlevel : {x y : A} → ⦃ hlevel (succ n) A ⦄ → hlevel n (x == y)
  =-hlevel ⦃ hlevel-in h ⦄ = h

_◃_ : 𝒰 i → 𝒰 j → 𝒰 (i ⊔ j)
A ◃ B = Σ (A → B) rinv
infixr 5 _◃_

-- Theorem 7.1.4
retract-hlevel : A ◃ B → ⦃ hlevel n A ⦄ → hlevel n B
retract-hlevel {n = zero} (p , s , ε) = hlevel-in (p center , λ b → ap p contr ∙ ε b)
retract-hlevel {A = A} {B = B} {n = succ n} (p , s , ε) =
  hlevel-in (retract-hlevel {n = n} r)
  where
  -- t =
  r : {y y' : B} → (s y == s y') ◃ (y == y')
  r {y} {y'} = t , ap s , λ u →
    ε y ⁻¹ ∙ ap p (ap s u) ∙ ε y'  =⟨ _ ∙ₗ ap-∘ p s u ⁻¹ ∙ᵣ _ ⟩
    ε y ⁻¹ ∙ ap (p ∘ s) u ∙ ε y'   =⟨ assoc ⁻¹ ⟩
    ε y ⁻¹ ∙ (ap (p ∘ s) u ∙ ε y') =⟨ pivotₗ (~-natural-id ε u) ⁻¹ ⟩
    u                              ∎
    where
    open =-Reasoning
    t : _
    t q = ε y ⁻¹ ∙ ap p q ∙ ε y'

equiv-hlevel : A ≃ B → ⦃ hlevel n A ⦄ → hlevel n B
equiv-hlevel e = retract-hlevel (pr₁ e , qinv→rinv (isequiv→qinv (pr₂ e)))

Π-implicit-equiv : ({x : A} → P x) ≃ Π A P
Π-implicit-equiv = iso→eqv λ{.f x _ → x ; .g h → h _ ; .η _ → refl ; .ε _ → refl}
  where open Iso

raise : ⦃ {_ : A} → hlevel n A ⦄ → hlevel (succ n) A
raise {n = zero} ⦃ f ⦄ = hlevel-in λ {x} →
  hlevel-in (contr ⦃ f {x} ⦄ ⁻¹ ∙ contr , λ{refl → invₗ})
raise {n = succ n} ⦃ f ⦄ = hlevel-in λ {x} →
  raise ⦃ =-hlevel ⦃ f {x} ⦄ ⦄

add : ℕ → ℕ → ℕ
add n zero = n
add n (succ m) = succ (add n m)

raise* : {A : 𝒰 i} → ⦃ hlevel n A ⦄ → {m : ℕ} → hlevel (add n (succ m)) A
raise* {m = zero} = raise
raise* {m = succ m} = raise ⦃ raise* ⦄

instance
  Lift-hlevel : ⦃ hlevel n A ⦄ → hlevel n (Lift {i} A)
  Lift-hlevel = equiv-hlevel (Lift-equiv ⁻¹ₑ)

  𝟎-hlevel : hlevel (succ n) (𝟎 {i})
  𝟎-hlevel {zero} = hlevel-in λ where {()}
  𝟎-hlevel {succ _} = raise

  𝟏-hlevel : hlevel n (𝟏 {i})
  𝟏-hlevel {zero} = hlevel-in (★ , λ where ★ → refl)
  𝟏-hlevel {succ _} = raise

  𝟐-hlevel : hlevel (succ (succ n)) 𝟐
  𝟐-hlevel {n} = hlevel-in (equiv-hlevel (=𝟐-equiv ⁻¹ₑ))
    where
    code-hlevel : {x y : 𝟐} → hlevel (succ n) (x =𝟐 y)
    code-hlevel {0₂} {0₂} = ⟨⟩
    code-hlevel {0₂} {1₂} = ⟨⟩
    code-hlevel {1₂} {0₂} = ⟨⟩
    code-hlevel {1₂} {1₂} = ⟨⟩
    instance _ = code-hlevel

  Π-hlevel : ⦃ {x : A} → hlevel n (P x) ⦄ → hlevel n (Π A P)
  Π-hlevel {n = zero} = hlevel-in ((λ _ → center) , (λ _ → funext λ _ → contr))
  Π-hlevel {n = succ n} = hlevel-in (equiv-hlevel (=Π-equiv ⁻¹ₑ))

  Π-implicit-hlevel : ⦃ {x : A} → hlevel n (P x) ⦄ → hlevel n ({x : A} → P x)
  Π-implicit-hlevel = equiv-hlevel (Π-implicit-equiv ⁻¹ₑ)

  +-hlevel : ⦃ hlevel (succ (succ n)) A ⦄ → ⦃ hlevel (succ (succ n)) B ⦄ →
             hlevel (succ (succ n)) (A + B)
  +-hlevel {n} {A = A} {B = B} = hlevel-in (equiv-hlevel (=+-equiv ⁻¹ₑ))
    where
    code-hlevel : {x y : A + B} → hlevel (succ n) (x =+ y)
    code-hlevel {inl _} {inl _} = ⟨⟩
    code-hlevel {inl _} {inr _} = ⟨⟩
    code-hlevel {inr _} {inl _} = ⟨⟩
    code-hlevel {inr _} {inr _} = ⟨⟩
    instance _ = code-hlevel

  ℕ-hlevel : hlevel 2 ℕ
  hlevel-out ℕ-hlevel {x} = equiv-hlevel (=ℕ-equiv ⁻¹ₑ)
    where
    code-hlevel : {x y : ℕ} → hlevel 1 (x =ℕ y)
    code-hlevel {zero} {zero} = ⟨⟩
    code-hlevel {zero} {succ y} = ⟨⟩
    code-hlevel {succ x} {zero} = ⟨⟩
    code-hlevel {succ x} {succ y} = code-hlevel {x}
    instance _ = code-hlevel {x}

-- Make Σ-hlevel a private instance so it can be installed as-needed.
-- There are too many cases where we want to use some other instance
-- instead.
Σ-hlevel : ⦃ h₁ : hlevel n A ⦄ → ⦃ h₂ : {x : A} → hlevel n (P x) ⦄ → hlevel n (Σ A P)
private instance _ = Σ-hlevel
Σ-hlevel {n = zero} = hlevel-in ((center , center) , λ x → pair⁼' (contr , contr))
Σ-hlevel {n = succ n} = hlevel-in (equiv-hlevel (=Σ-equiv ⁻¹ₑ))

→-hlevel : ⦃ hlevel n B ⦄ → hlevel n (A → B)
→-hlevel = ⟨⟩

×-hlevel : ⦃ h₁ : hlevel n A ⦄ → ⦃ h₂ : hlevel n B ⦄ → hlevel n (A × B)
×-hlevel = ⟨⟩

isContr-hlevel : hlevel 1 (isContr A)
hlevel-out (isContr-hlevel {A = A}) {h} = ⟨⟩
  where instance _ = raise* ⦃ hlevel-in h ⦄

hlevel-equiv : hlevel-type n A ≃ hlevel n A
hlevel-equiv = hlevel-in , qinv→isequiv (hlevel-out , (λ _ → refl) , (λ _ → refl))

instance
  hlevel-hlevel : hlevel 1 (hlevel n A)
  hlevel-hlevel {zero} = equiv-hlevel hlevel-equiv ⦃ isContr-hlevel ⦄
  hlevel-hlevel {succ n} = equiv-hlevel hlevel-equiv

hlevel⁼ : ⦃ h₁ : hlevel n A ⦄ ⦃ h₂ : hlevel n B ⦄ → A == B → type A == type B
hlevel⁼ ⦃ h₁ ⦄ ⦃ h₂ ⦄ refl rewrite center ⦃ =-hlevel {x = h₁} {h₂} ⦄ = refl

hlevel1→isProp : ⦃ hlevel 1 A ⦄ → isProp A
hlevel1→isProp = center

hlevel2→isSet : ⦃ hlevel 2 A ⦄ → isSet A
hlevel2→isSet = center

isProp→hlevel1 : isProp A → hlevel 1 A
hlevel-out (isProp→hlevel1 f) {x} {y} = ⟨⟩
  where instance _ = raise ⦃ hlevel-in (x , f x) ⦄

isProp-hlevel1 : hlevel 1 (isProp A)
hlevel-out isProp-hlevel1 {f} = ⟨⟩
  where instance _ = raise ⦃ isProp→hlevel1 f ⦄

isProp-prop : isProp (isProp A)
isProp-prop = hlevel1→isProp ⦃ isProp-hlevel1 ⦄

isProp→isSet : isProp A → isSet A
isProp→isSet A-prop {x} {y} p q = center
  where instance _ = raise ⦃ isProp→hlevel1 A-prop ⦄

isContr-prop : isProp (isContr A)
isContr-prop (a , p) (a' , p') = pair⁼ (p a' , center)
  where instance _ = raise* ⦃ hlevel-in (a , p) ⦄

prop-equiv : ⦃ h₁ : hlevel 1 A ⦄ → ⦃ h₂ : hlevel 1 B ⦄ →
             (A → B) → (B → A) → A ≃ B
prop-equiv f g = f , qinv→isequiv (g , (λ _ → center) , (λ _ → center))

Σ-contr₁ : ⦃ _ : hlevel 0 A ⦄ → Σ A P ≃ P center
Σ-contr₁ {A = A} {P = P} ⦃ h ⦄ = let open Iso in iso→eqv λ where
  .f   → transport P (contr ⁻¹) ∘ pr₂
  .g y → center , y
  .η x → pair⁼ (contr , Eqv.ε (transport-equiv (contr {A = A})) _)
  .ε y → ap {x = contr ⁻¹} (λ p → transport P p y)
    let instance _ = raise* ⦃ h ⦄ in center

Σ-contr₂ : ⦃ {x : A} → hlevel 0 (P x) ⦄ → Σ A P ≃ A
Σ-contr₂ = let open Iso in iso→eqv λ where
  .f   → pr₁
  .g x → x , center
  .η _ → pair⁼ (refl , contr)
  .ε _ → refl

×-contr₁ : ⦃ hlevel 0 A ⦄ → A × B ≃ B
×-contr₁ = Σ-contr₁

×-contr₂ : ⦃ hlevel 0 B ⦄ → A × B ≃ A
×-contr₂ = Σ-contr₂

Π-contr₁ : ⦃ _ : hlevel 0 A ⦄ → Π A P ≃ P center
Π-contr₁ {A = A} {P = P} ⦃ h ⦄ = let open Iso in iso→eqv λ where
  .f h   → h center
  .g x _ → transport P contr x
  .η h   → funext (λ _ → apd h contr)
  .ε x   → ap {x = contr} (λ p → transport P p x)
    let instance _ = raise* ⦃ h ⦄ in center

=-contrₗ : (a : A) → hlevel 0 (Σ A (a ==_))
=-contrₗ a = hlevel-in ((a , refl) , λ (_ , p) →
  pair⁼ (p , transport=-const-id p a refl ∙ unitₗ ⁻¹))

=-contrᵣ : (a : A) → hlevel 0 (Σ A (_== a))
=-contrᵣ a = hlevel-in ((a , refl) , λ (_ , p) →
  pair⁼ (p ⁻¹ , transport=-id-const a (p ⁻¹) refl ∙ unitᵣ ⁻¹ ∙ invinv))

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
------------------------------------------------------------------------
-- Parsing of mixfix operators
------------------------------------------------------------------------

-- This module defines a grammar for the precedence graph g. The
-- grammar is neither left nor right recursive.

open import Mixfix.Expr
open import Mixfix.Acyclic.PrecedenceGraph
  using (acyclic; precedence)

module Mixfix.Acyclic.Grammar
         (g : PrecedenceGraphInterface.PrecedenceGraph acyclic)
         where

open import Codata.Musical.Notation
open import Data.List using (List; []; _∷_)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.List.NonEmpty using (foldr; foldl)
open import Data.Product
open import Data.Bool
import Data.String as String
import Relation.Binary.PropositionalEquality as P

open PrecedenceCorrect acyclic g

import StructurallyRecursiveDescentParsing.Simplified as Simplified
open Simplified hiding (Parser; ⟦_⟧)
open import Mixfix.Fixity
open import Mixfix.Operator
open import Mixfix.Acyclic.Lib renaming (ParserProg to Parser)

-- The following definition uses a lexicographic combination of
-- guarded corecursion and structural recursion. The only "corecursive
-- call", where the size of the inductive input can increase
-- arbitrarily, is the one in expr.

mutual

  -- Expressions.

  expr : ∞ (Parser (Expr g))
  expr = ♯ precs g

  -- Expressions corresponding to zero or more nodes in the precedence
  -- graph: operator applications where the outermost operator has one
  -- of the precedences ps. The graph g is used for internal
  -- expressions.

  precs : (ps : List Precedence) → Parser (Expr ps)
  precs []       = fail
  precs (p ∷ ps) = (λ e → here P.refl ∙ proj₂ e) <$> prec p
                 ∣ weakenE                       <$> precs ps

  -- Expressions corresponding to one node in the precedence graph:
  -- operator applications where the outermost operator has
  -- precedence p. The graph g is used for internal expressions.

  prec : (p : Precedence) → Parser (∃ (ExprIn p))
  prec (precedence ops sucs) =
      ⟪_⟫    <$>       [ closed   ]
    ∥ _⟨_⟩_  <$>  p↑ ⊛ [ infx non ] ⊛ p↑
    ∥ appʳ   <$>       preRight +   ⊛ p↑
    ∥ appˡ   <$>  p↑ ⊛ postLeft +
    ∥ fail
    module Prec where
    p = precedence ops sucs

    -- [ fix ] parses the internal parts of operators with the
    -- current precedence level and fixity fix.
    [_] = λ (fix : Fixity) → inner (ops fix)

    -- Operator applications where the outermost operator binds
    -- tighter than the current precedence level.
    p↑ = precs sucs

    -- Right associative and prefix operators.
    preRight : Parser (Outer p right → ExprIn p right)
    preRight =  ⟪_⟩_  <$>      [ prefx      ]
             ∣ _⟨_⟩ʳ_ <$> p↑ ⊛ [ infx right ]

    -- Left associative and postfix operators.
    postLeft : Parser (Outer p left → ExprIn p left)
    postLeft = (λ op    e₁ → e₁ ⟨ op ⟫    ) <$> [ postfx    ]
             ∣ (λ op e₂ e₁ → e₁ ⟨ op ⟩ˡ e₂) <$> [ infx left ] ⊛ p↑

    -- Post-processing for the non-empty lists returned by _+.
    appʳ = λ fs e → foldr (λ f e → f (similar e)) (λ f → f (tighter e)) fs
    appˡ = λ e fs → foldl (λ e f → f (similar e)) (λ f → f (tighter e)) fs

  -- Internal parts (all name parts plus internal expressions) of
  -- operators of the given precedence and fixity.

  inner : ∀ {fix} (ops : List (∃ (Operator fix))) →
          Parser (Inner ops)
  inner []               = fail
  inner ((_ , op) ∷ ops) =
      (λ args → here P.refl ∙ args) <$> (expr between nameParts op)
    ∣ weakenI                       <$> inner ops

-- Expression parsers.

expression : Simplified.Parser NamePart false (Expr g)
expression = ⟦ ♭ expr ⟧

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module Numeral.Finite.LinearSearch where -- TODO: Maybe move to Numeral.CoordinateVector.LinearSearch

open import Data.Boolean
open import Data.Boolean.Stmt
open import Data.List
import      Data.List.Functions as List
open import Data.Option
import      Data.Option.Functions as Option
open import Functional
open import Logic
open import Numeral.Finite
open import Numeral.Finite.Bound
open import Numeral.Natural
open import Structure.Relator.Ordering

private variable n : ℕ
private variable i j min max : 𝕟(n)
private variable f : 𝕟(n) → Bool

-- Finds the maximal argument satisfying the given decidable predicate by searching linearly.
-- Examples:
--   findMax{5}   (10 ∣?_) = None
--   findMax{10}  (10 ∣?_) = None
--   findMax{20}  (10 ∣?_) = Some 10
--   findMax{21}  (10 ∣?_) = Some 20
--   findMax{22}  (10 ∣?_) = Some 20
--   findMax{100} (10 ∣?_) = Some 90
--   findMax{102} (10 ∣?_) = Some 100
-- Alternative implementation: findMax f = Option.map Wrapping.[−]_ (findMin(f ∘ Wrapping.[−]_))
findMax : (𝕟(n) → Bool) → Option(𝕟(n))
findMax {𝟎}    f = None
findMax {𝐒(n)} f with f(maximum)
findMax {𝐒(n)} f | 𝑇 = Some maximum
findMax {𝐒(n)} f | 𝐹 = Option.map bound-𝐒 (findMax{n} (f ∘ bound-𝐒))

-- Finds the minimal argument satisfying the given decidable predicate by searching linearly.
-- Examples:
--   findMin{5}   (10 ∣?_) = None
--   findMin{10}  (10 ∣?_) = None
--   findMin{20}  (10 ∣?_) = Some 10
--   findMin{21}  (10 ∣?_) = Some 10
--   findMin{22}  (10 ∣?_) = Some 10
--   findMin{100} (10 ∣?_) = Some 10
--   findMax{102} (10 ∣?_) = Some 10
findMin : (𝕟(n) → Bool) → Option(𝕟(n))
findMin{𝟎}    f = None
findMin{𝐒(n)} f with f(𝟎)
findMin{𝐒(n)} f | 𝑇 = Some 𝟎
findMin{𝐒(n)} f | 𝐹 = Option.map 𝐒 (findMin{n} (f ∘ 𝐒))

-- Finds all arguments satisfying the given decidable predicate by searching linearly.
-- Examples:
--   findAll{10} (2 ∣?_) = [0,2,4,6,8]
findAll : (𝕟(n) → Bool) → List(𝕟(n))
findAll{𝟎}    f = ∅
findAll{𝐒(n)} f = (if f(𝟎) then (𝟎 ⊰_) else id) (List.map 𝐒 (findAll{n} (f ∘ 𝐒)))

open import Data
open import Data.Boolean.Stmt.Proofs
open import Data.List.Relation.Membership using (_∈_)
open import Data.List.Relation.Membership.Proofs
open import Data.List.Relation.Pairwise
open import Data.List.Relation.Pairwise.Proofs
open import Data.List.Relation.Quantification
open import Data.List.Relation.Quantification.Proofs
open import Data.List.Sorting
open import Data.Option.Equiv.Id
open import Lang.Inspect
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Numeral.Finite.Oper.Comparisons
open import Numeral.Finite.Oper.Comparisons.Proofs
open import Numeral.Finite.Proofs
open import Numeral.Finite.Relation.Order as 𝕟 using (_≤_ ; _>_ ; _<_ ; [≤]-minimum ; [≤]-maximum)
import      Numeral.Natural.Relation.Order as ℕ
open import Numeral.Natural.Relation.Order.Proofs as ℕ
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Relator.Properties
open import Structure.Relator
open import Type.Properties.Decidable
open import Type.Properties.Decidable.Proofs

{-
open import Syntax.Number
test : 𝕟(5) → Bool
test 𝟎 = 𝐹
test (𝐒 𝟎) = 𝐹
test (𝐒 (𝐒 𝟎)) = 𝑇
test (𝐒 (𝐒 (𝐒 𝟎))) = 𝐹
test (𝐒 (𝐒 (𝐒 (𝐒 𝟎)))) = 𝐹
test2 : 𝕟(1) → Bool
test2 𝟎 = 𝑇
test3 : findMax test2 ≡ Some 0
test3 = [≡]-intro
tst4 = {!Option.map bound-𝐒 (findMax (test ∘ bound-𝐒))!}
-}

findMax-None-correctness : (findMax f ≡ None) ↔ (∀{i} → IsFalse(f(i)))
findMax-None-correctness = [↔]-intro l r where
  l : (findMax f ≡ None) ← (∀{i} → IsFalse(f(i)))
  l {𝟎} {f} p = [≡]-intro
  l {𝐒 n} {f} p with f(maximum) | inspect f(maximum)
  ... | 𝑇 | intro fmax with () ← disjointness p ([↔]-to-[←] IsTrue.is-𝑇 fmax)
  ... | 𝐹 | intro fmax = congruence₁(Option.map bound-𝐒) (l p)

  r-result : IsFalse(f(maximum)) → (∀{i : 𝕟(n)} → IsFalse((f ∘ bound-𝐒) i)) → (∀{i : 𝕟(n)} → IsFalse(f(𝐒 i)))
  r-result {𝐒 n}     {f} p q {𝐒 i} = r-result {n}{f ∘ 𝐒} p (\{i} → q{𝐒 i}) {i}
  r-result {𝐒 𝟎}     {f} p q {𝟎}   = p
  r-result {𝐒 (𝐒 n)} {f} p q {𝟎}   = q{𝐒 𝟎}

  r : (findMax f ≡ None) → (∀{i} → IsFalse(f(i)))
  r {𝐒 n}     {f} p {i} with f(maximum) | inspect f(maximum)
  r {𝐒 n}     {f} p {𝐒 i} | 𝐹 | intro fmax = r-result {f = f} ([↔]-to-[←] IsFalse.is-𝐹 fmax) (\{i} → r {n}{f ∘ bound-𝐒} (map-None p) {i}) {i}
  r {𝐒 𝟎}     {f} p {𝟎}   | 𝐹 | intro fmax = [↔]-to-[←] IsFalse.is-𝐹 fmax
  r {𝐒 (𝐒 n)} {f} p {𝟎}   | 𝐹 | intro fmax = r {𝐒 n} {f ∘ bound-𝐒} (map-None p) {𝟎}

findMax-Some-correctness : (findMax f ≡ Some(i)) → IsTrue(f(i))
findMax-Some-correctness {𝐒 n} {f} {i}        eq with f(maximum) | inspect f(maximum)
findMax-Some-correctness {𝐒 n} {f} {.maximum} [≡]-intro | 𝑇 | intro fmax = [↔]-to-[←] IsTrue.is-𝑇 fmax
findMax-Some-correctness {𝐒 n} {f} {i}        eq        | 𝐹 | intro fmax with findMax(f ∘ bound-𝐒) | inspect findMax(f ∘ bound-𝐒)
findMax-Some-correctness {𝐒 n} {f} {.(_)}     [≡]-intro | 𝐹 | intro fmax | Some x | intro p = findMax-Some-correctness {f = f ∘ bound-𝐒} p

findMin-None-correctness : (findMin f ≡ None) ↔ (∀{i} → IsFalse(f(i)))
findMin-None-correctness = [↔]-intro l r where
  l : (findMin f ≡ None) ← (∀{i} → IsFalse(f(i)))
  l {𝟎} {f} p = [≡]-intro
  l {𝐒 n} {f} p with f(𝟎) | inspect f(𝟎)
  ... | 𝑇 | intro f0 with () ← disjointness p ([↔]-to-[←] IsTrue.is-𝑇 f0)
  ... | 𝐹 | intro f0 = congruence₁(Option.map 𝐒) (l p)

  r : (findMin f ≡ None) → (∀{i} → IsFalse(f(i)))
  r {𝐒 n} {f} p {i} with f(𝟎) | inspect f(𝟎)
  r {𝐒 n} {f} p {𝟎}   | 𝐹 | intro f0 = [↔]-to-[←] IsFalse.is-𝐹 f0
  r {𝐒 n} {f} p {𝐒 i} | 𝐹 | intro f0 = r {f = f ∘ 𝐒} (injective(Option.map 𝐒) ⦃ map-injectivity ⦄ p)

findMin-Some-correctness : (findMin f ≡ Some(min)) → IsTrue(f(min))
findMin-Some-correctness {𝐒 n} {f} {min} eq with f(𝟎) | inspect f(𝟎)
findMin-Some-correctness {𝐒 n} {f} {𝟎}     [≡]-intro | 𝑇 | intro f0 = [↔]-to-[←] IsTrue.is-𝑇 f0
findMin-Some-correctness {𝐒 n} {f} {𝟎}     eq        | 𝐹 | intro f0 with findMin{n} (f ∘ 𝐒)
findMin-Some-correctness {𝐒 n} {f} {𝟎}     ()        | 𝐹 | intro f0 | None
findMin-Some-correctness {𝐒 n} {f} {𝟎}     ()        | 𝐹 | intro f0 | Some _
findMin-Some-correctness {𝐒 n} {f} {𝐒 min} eq        | 𝐹 | intro f0 = findMin-Some-correctness {n} {f ∘ 𝐒} {min} (injective(Option.map 𝐒) ⦃ map-injectivity ⦄ eq)

findMin-minimal-true : (findMin f ≡ Some(min)) → IsTrue(f(i)) → (min ≤ i)
findMin-minimal-true {𝐒 n} {f} {min}   {i}   eq        p with f(𝟎) | inspect f(𝟎)
findMin-minimal-true {𝐒 n} {f} {.𝟎}    {i}   [≡]-intro p | 𝑇 | intro f0 = 𝕟.[≤]-minimum {a = i}
findMin-minimal-true {𝐒 n} {f} {𝟎}     {i}   eq        p | 𝐹 | intro f0 with findMin{n} (f ∘ 𝐒)
findMin-minimal-true {𝐒 n} {f} {𝟎}     {i}   ()        p | 𝐹 | intro f0 | None
findMin-minimal-true {𝐒 n} {f} {𝟎}     {i}   ()        p | 𝐹 | intro f0 | Some _
findMin-minimal-true {𝐒 n} {f} {𝐒 min} {𝟎}   eq        p | 𝐹 | intro f0 = disjointness p ([↔]-to-[←] IsFalse.is-𝐹 f0)
findMin-minimal-true {𝐒 n} {f} {𝐒 min} {𝐒 i} eq        p | 𝐹 | intro f0 = findMin-minimal-true {n} {f ∘ 𝐒} {min} {i} (injective(Option.map 𝐒) ⦃ map-injectivity ⦄ eq) p

findMin-minimal-false : (findMin f ≡ Some(min)) → (min > i) → IsFalse(f(i))
findMin-minimal-false {n}{f}{min}{i} eq =
  [↔]-to-[←] false-true-opposites
  ∘ contrapositiveᵣ(findMin-minimal-true{n}{f}{min}{i} eq)
  ∘ [↔]-to-[←] decider-true ∘ substitute₁ₗ(IsTrue) (⋚-elim₃-negation-distribution {x = min}{y = i})

{-
instance
  [≤]-with-[𝐒]-injective : ∀{a b} → Injective(\p → ℕ.[≤]-with-[𝐒] {a}{b} ⦃ p ⦄)
  Injective.proof [≤]-with-[𝐒]-injective [≡]-intro = [≡]-intro

import      Structure.Function.Names as Names
open import Function.Equals
bound-[≤]-injective : ∀{a b} → Injective ⦃ [≡]-equiv ⦄ ⦃ [⊜]-equiv ⦄ (bound-[≤] {a}{b})
bound-[≤]-injective {a}{b} = intro proof where
  proof : Names.Injective ⦃ [≡]-equiv ⦄ ⦃ [⊜]-equiv ⦄ (bound-[≤] {a}{b})
  proof {ℕ.[≤]-minimum} {ℕ.[≤]-minimum} p = [≡]-intro
  proof {ℕ.[≤]-with-[𝐒] ⦃ x ⦄} {ℕ.[≤]-with-[𝐒] ⦃ y ⦄} (intro p) = {!(injective ⦃ ? ⦄ ⦃ ? ⦄ (𝕟.𝐒) ⦃ ? ⦄ {x = bound-[≤] x}{y = bound-[≤] y} p)!}
--Injective.proof bound-[≤]-injective {ℕ.[≤]-minimum} {ℕ.[≤]-minimum} p = [≡]-intro
--Injective.proof bound-[≤]-injective {ℕ.[≤]-with-[𝐒] {y = _} ⦃ x ⦄} {ℕ.[≤]-with-[𝐒] {y = _} ⦃ y ⦄} (intro p) = {!injective(𝐒) ⦃ ? ⦄ p!}
-- injective(𝐒) ⦃ [≤]-with-[𝐒]-injective ⦄

bound-𝐒-injective : Injective(bound-𝐒 {n})
Injective.proof bound-𝐒-injective {𝟎} {𝟎} p = [≡]-intro
Injective.proof bound-𝐒-injective {𝐒 x} {𝐒 y} p = congruence₁(𝐒) (Injective.proof bound-𝐒-injective {x} {y} (injective(𝐒) p))
-}

-- TODO
postulate findMax-maximal-true : (findMax f ≡ Some(max)) → IsTrue(f(i)) → (i ≤ max)
{-findMax-maximal {𝐒 n}{f} eq p with f(maximum) | inspect f(maximum)
findMax-maximal {𝐒 n} {f} {i = i} [≡]-intro p | 𝑇 | intro m = [≤]-maximum {𝐒 n}{i} (reflexivity(ℕ._≤_))
findMax-maximal {𝐒 n} {f} {i = i} eq p | 𝐹 | intro m with findMax{n} (f ∘ bound-𝐒) | inspect (findMax{n}) (f ∘ bound-𝐒)
findMax-maximal {𝐒 n} {f} {i = i} eq p | 𝐹 | intro m | Some x | intro findMax-x = {!findMax-maximal {n} {f ∘ bound-𝐒} {i = ?} !}
-}

{- TODO
test : ∀{i : 𝕟(𝐒(n))} → ¬(maximum{n} < i)
test {𝟎}   {𝟎}   p = p
test {𝐒 n} {𝟎}   p = p
test {𝐒 n} {𝐒 i} p = test {n}{i} p

{-
findMax-maximal2 : (findMax f ≡ Some(max)) → (i > max) → IsFalse(f(i))
findMax-maximal2 {𝐒 n} {f} {max} {i} eq p with f(maximum) | inspect f(maximum)
findMax-maximal2 {𝐒 n} {f} {𝟎} {𝐒 i} eq p | 𝑇 | intro fmax with maximum-0(injective(Some) eq)
findMax-maximal2 {𝐒 .0} {f} {𝟎} {𝐒 ()} eq p | 𝑇 | intro fmax | [≡]-intro
findMax-maximal2 {𝐒 (𝐒 n)} {f} {𝐒 max} {𝐒 i} eq p | 𝑇 | intro fmax with f(bound-𝐒 maximum) | inspect (f ∘ bound-𝐒)(maximum)
findMax-maximal2 {𝐒 (𝐒 n)} {f} {𝐒 .maximum} {𝐒 i} [≡]-intro p | 𝑇 | intro fmax | 𝑇 | intro x with () ← test{n} p
findMax-maximal2 {𝐒 (𝐒 n)} {f} {𝐒 {.(𝐒 n)} .(maximum {n})} {𝐒 {.(𝐒 n)} i} ([≡]-intro {x = .(Some (𝐒 {𝐒 n} (maximum {n})))}) p | 𝑇 | intro fmax | 𝐹 | intro x with () ← test{n} p
findMax-maximal2 {𝐒 n} {f} {𝟎} {𝐒 i} eq p | 𝐹 | intro fmax = {!!}
findMax-maximal2 {𝐒 n} {f} {𝐒 max} {𝐒 i} eq p | 𝐹 | intro fmax = {!!}
-}

test2 : (bound-𝐒 i ≡ 𝟎) → (i ≡ 𝟎)
test2 {i = 𝟎} p = [≡]-intro

findMax-maximal : (findMax f ≡ Some(max)) → IsTrue(f(i)) → (i ≤ max)
findMax-maximal {𝐒 n}{f} eq p with f(maximum) | inspect f(maximum)
findMax-maximal {𝐒 n} {f} {_}{i} [≡]-intro p | 𝑇 | intro fmax = [≤]-maximum {𝐒 n}{i} (reflexivity(ℕ._≤_))
findMax-maximal {𝐒 n} {f} {max} {𝟎} eq p | 𝐹 | intro fmax = [≤]-minimum {a = max}
findMax-maximal {𝐒 (𝐒 n)} {f} {max} {𝐒 i} eq p | 𝐹 | intro fmax with f(bound-𝐒 maximum) | inspect (f ∘ bound-𝐒)(maximum)
findMax-maximal {𝐒 (𝐒 n)} {f} {𝟎} {𝐒 i} eq p | 𝐹 | intro fmax | 𝑇 | intro x = {!maximum-0(test2(injective(Some) eq))!}
findMax-maximal {𝐒 (𝐒 n)} {f} {𝐒 max} {𝐒 i} eq p | 𝐹 | intro fmax | 𝑇 | intro x = {!!}
... | 𝐹 | intro x = {!!}
-- findMax-maximal {f = f ∘ bound-𝐒} {i = i} (injective(Option.map bound-𝐒) ⦃ map-injectivity ⦃ ? ⦄ ⦄ {findMax(f ∘ bound-𝐒)} {Some 𝟎} eq)
{-findMax-maximal {𝐒 n} {f} {max} {i} eq p with f(maximum) | inspect f(maximum)
findMax-maximal {𝐒 n} {f} {.maximum} {i} [≡]-intro p | 𝑇 | intro fmax = [≤]-maximum {𝐒 n}{i}{n = n} (reflexivity(ℕ._≤_))
findMax-maximal {𝐒 n} {f} {max} {i} eq p | 𝐹 | intro fmax with findMax{n} (f ∘ bound-𝐒)
findMax-maximal {𝐒 n} {f} {max} {i} () p | 𝐹 | intro fmax | None
-}
{-findMax-maximal {𝐒 n} {f} {𝟎}     {𝟎}   eq p | 𝐹 | intro fmax | Some x = <>
findMax-maximal {𝐒 n} {f} {𝐒 max} {𝟎}   eq p | 𝐹 | intro fmax | Some x = <>
findMax-maximal {𝐒(𝐒 n)} {f} {𝟎} {𝐒 i} eq p | 𝐹 | intro fmax | Some 𝟎 = {!findMax-maximal!}
findMax-maximal {𝐒 n} {f} {𝐒 max} {𝐒 i} eq p | 𝐹 | intro fmax | Some x = {!!}
-}
{-findMax-maximal {𝐒 n} {f} {.(bound-[≤] ([≤]-successor ([≡]-to-[≤] [≡]-intro)) x)} {𝟎} [≡]-intro p | 𝐹 | intro fmax | Some x = [≤]-minimum {a = bound-𝐒(x)}
findMax-maximal {𝐒 .(𝐒 _)} {f} {.(bound-[≤] ([≤]-successor ([≡]-to-[≤] [≡]-intro)) 𝟎)} {𝐒 i} [≡]-intro p | 𝐹 | intro fmax | Some 𝟎 = {!!}
findMax-maximal {𝐒 .(𝐒 _)} {f} {.(bound-[≤] ([≤]-successor ([≡]-to-[≤] [≡]-intro)) (𝐒 x))} {𝐒 i} [≡]-intro p | 𝐹 | intro fmax | Some (𝐒 x) = {!!}-}
-}

{-
open import Numeral.Finite.Oper
findMax-findMin : findMax f ≡ Option.map Wrapping.[−]_ (findMin(f ∘ Wrapping.[−]_))
findMax-findMin {𝟎} {f} = [≡]-intro
findMax-findMin {𝐒 n} {f} with f(maximum) | inspect f(maximum)
... | 𝑇 | intro fmax = [≡]-intro
... | 𝐹 | intro fmax = {!!}
-}

findAll-correctness : AllElements(IsTrue ∘ f)(findAll f)
findAll-correctness {𝟎}   {f} = ∅
findAll-correctness {𝐒 n} {f} with f(𝟎) | inspect f(𝟎)
... | 𝑇 | intro f0 = ([↔]-to-[←] IsTrue.is-𝑇 f0) ⊰ (AllElements-mapᵣ 𝐒 id (findAll-correctness {n}{f ∘ 𝐒}))
... | 𝐹 | intro _  = AllElements-mapᵣ 𝐒 id (findAll-correctness {n}{f ∘ 𝐒})

findAll-completeness : IsTrue(f(i)) → (i ∈ findAll f)
findAll-completeness {𝐒 n} {f} {i}   p with f(𝟎) | inspect f(𝟎)
findAll-completeness {𝐒 n} {f} {𝟎}   p | 𝑇 | intro _  = • [≡]-intro
findAll-completeness {𝐒 n} {f} {𝐒 i} p | 𝑇 | intro _  = ⊰ [∈]-map (findAll-completeness{n}{f ∘ 𝐒}{i} p)
findAll-completeness {𝐒 n} {f} {𝟎}   p | 𝐹 | intro f0 with () ← disjointness p ([↔]-to-[←] IsFalse.is-𝐹 f0)
findAll-completeness {𝐒 n} {f} {𝐒 i} p | 𝐹 | intro _  = [∈]-map (findAll-completeness {n} {f ∘ 𝐒} {i} p)

findAll-sorted : Sorted(_≤?_)(findAll f)
findAll-sorted {𝟎}      {f} = AdjacentlyPairwise.empty
findAll-sorted {𝐒 𝟎} {f} with f(𝟎) | inspect f(𝟎)
findAll-sorted {𝐒 𝟎} {f} | 𝑇 | intro f0 = AdjacentlyPairwise.single
findAll-sorted {𝐒 𝟎} {f} | 𝐹 | intro f0 = AdjacentlyPairwise.empty
findAll-sorted {𝐒(𝐒 n)} {f} with f(𝟎) | f(𝐒 𝟎) | AdjacentlyPairwise-map {_▫₁_ = IsTrue ∘₂ _≤?_}{f = 𝐒}{_▫₂_ = IsTrue ∘₂ _≤?_} id (findAll-sorted {𝐒 n}{f ∘ 𝐒})
... | 𝑇 | 𝑇 | prev = AdjacentlyPairwise.step ⦃ <> ⦄ ⦃ prev ⦄
... | 𝑇 | 𝐹 | prev = AdjacentlyPairwise-prepend (\{ {𝟎} → <> ; {𝐒 _} → <>}) prev
... | 𝐹 | 𝑇 | prev = prev
... | 𝐹 | 𝐹 | prev = prev


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.FreeAbGroup.Base where

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

infixl 7 _·_
infix 20 _⁻¹

private variable
  ℓ ℓ' : Level
  A : Type ℓ

data FreeAbGroup (A : Type ℓ) : Type ℓ where
  ⟦_⟧       : A → FreeAbGroup A
  ε         : FreeAbGroup A
  _·_       : FreeAbGroup A → FreeAbGroup A → FreeAbGroup A
  _⁻¹       : FreeAbGroup A → FreeAbGroup A
  assoc     : ∀ x y z → x · (y · z) ≡ (x · y) · z
  comm      : ∀ x y   → x · y       ≡ y · x
  identityᵣ : ∀ x     → x · ε       ≡ x
  invᵣ      : ∀ x     → x · x ⁻¹    ≡ ε
  trunc     : isSet (FreeAbGroup A)

module Elim {B : FreeAbGroup A → Type ℓ'}
  (⟦_⟧*       : (x : A) → B ⟦ x ⟧)
  (ε*         : B ε)
  (_·*_       : ∀ {x y}   → B x → B y → B (x · y))
  (_⁻¹*       : ∀ {x}     → B x → B (x ⁻¹))
  (assoc*     : ∀ {x y z} → (xs : B x) (ys : B y) (zs : B z)
    → PathP (λ i → B (assoc x y z i)) (xs ·* (ys ·* zs)) ((xs ·* ys) ·* zs))
  (comm*      : ∀ {x y}   → (xs : B x) (ys : B y)
    → PathP (λ i → B (comm x y i)) (xs ·* ys) (ys ·* xs))
  (identityᵣ* : ∀ {x}     → (xs : B x)
    → PathP (λ i → B (identityᵣ x i)) (xs ·* ε*) xs)
  (invᵣ* : ∀ {x} → (xs : B x)
    → PathP (λ i → B (invᵣ x i)) (xs ·* (xs ⁻¹*)) ε*)
  (trunc*     : ∀ xs → isSet (B xs)) where

  f : (xs : FreeAbGroup A) → B xs
  f ⟦ x ⟧ = ⟦ x ⟧*
  f ε = ε*
  f (xs · ys) = f xs ·* f ys
  f (xs ⁻¹) = f xs ⁻¹*
  f (assoc xs ys zs i) = assoc* (f xs) (f ys) (f zs) i
  f (comm xs ys i) = comm* (f xs) (f ys) i
  f (identityᵣ xs i) = identityᵣ* (f xs) i
  f (invᵣ xs i) = invᵣ* (f xs) i
  f (trunc xs ys p q i j) = isOfHLevel→isOfHLevelDep 2 trunc*  (f xs) (f ys)
    (cong f p) (cong f q) (trunc xs ys p q) i j

module ElimProp {B : FreeAbGroup A → Type ℓ'}
  (BProp : {xs : FreeAbGroup A} → isProp (B xs))
  (⟦_⟧*       : (x : A) → B ⟦ x ⟧)
  (ε*         : B ε)
  (_·*_       : ∀ {x y}   → B x → B y → B (x · y))
  (_⁻¹*       : ∀ {x}     → B x → B (x ⁻¹)) where

  f : (xs : FreeAbGroup A) → B xs
  f = Elim.f ⟦_⟧* ε* _·*_ _⁻¹*
    (λ {x y z} xs ys zs → toPathP (BProp (transport (λ i → B (assoc x y z i)) (xs ·* (ys ·* zs))) ((xs ·* ys) ·* zs)))
    (λ {x y} xs ys → toPathP (BProp (transport (λ i → B (comm x y i)) (xs ·* ys)) (ys ·* xs)))
    (λ {x} xs → toPathP (BProp (transport (λ i → B (identityᵣ x i)) (xs ·* ε*)) xs))
    (λ {x} xs → toPathP (BProp (transport (λ i → B (invᵣ x i)) (xs ·* (xs ⁻¹*))) ε*))
    (λ _ → (isProp→isSet BProp))

module Rec {B : Type ℓ'} (BType : isSet B)
  (⟦_⟧*       : (x : A) → B)
  (ε*         : B)
  (_·*_       : B → B → B)
  (_⁻¹*       : B → B)
  (assoc*     : (x y z : B) → x ·* (y ·* z) ≡ (x ·* y) ·* z)
  (comm*      : (x y : B)   → x ·* y        ≡ y ·* x)
  (identityᵣ* : (x : B)     → x ·* ε*       ≡ x)
  (invᵣ*      : (x : B)     → x ·* (x ⁻¹*)  ≡ ε*)
  where

  f : FreeAbGroup A → B
  f = Elim.f ⟦_⟧* ε* _·*_ _⁻¹* assoc* comm* identityᵣ* invᵣ* (const BType)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --type-in-type #-}
module chu where
open import functors
open import prelude

record Chu : Set where
  constructor _,_!_
  field
    _⁺ _⁻ : Set
    _Ω_ : _⁺ → _⁻ → Set

module _ (A@(A⁺ , A⁻ ! _Ω₁_) B@(B⁺ , B⁻ ! _Ω₂_) : Chu) where
    record Chu[_,_] :  Set where -- Morphisms of chu spaces
      constructor _↔_!_
      field
        to : A⁺ → B⁺
        from : B⁻ → A⁻
        adj : ∀ a⁺ b⁻ → to a⁺ Ω₂ b⁻ ≡ a⁺ Ω₁ from b⁻
module _ {A@(A⁺ , A⁻ ! _Ω₁_)
          B@(B⁺ , B⁻ ! _Ω₂_)
          C@(C⁺ , C⁻ ! _Ω₃_) : Chu}
         (F@(f  ↔ fᵗ ! _†₁_) : Chu[ A , B ])
         (G@(g  ↔ gᵗ ! _†₂_) : Chu[ B , C ]) where
    adj-comp : ∀ a⁺ c⁻ → (g ∘ f) a⁺ Ω₃ c⁻ ≡ a⁺ Ω₁ (fᵗ ∘ gᵗ) c⁻
    adj-comp a⁺ c⁻ = trans (f a⁺ †₂    c⁻)  -- g (f a⁺) Ω₃        c⁻
                           (  a⁺ †₁ gᵗ c⁻)  --    f a⁺  Ω₂     gᵗ c⁻
                                            --      a⁺  Ω₁ fᵗ (gᵗ c⁻)
    chu-comp : Chu[ A , C ]
    chu-comp = (g ∘ f) ↔ (fᵗ ∘ gᵗ) ! adj-comp

instance
    chu-cat : Category Chu[_,_]
    chu-cat = 𝒾: (id ↔ id ! λ _ _ → refl)
              ▸: chu-comp
              𝒾▸: (λ (_ ↔ _ ! _†_) → (λ x → _ ↔ _ ! x) ⟨$⟩
                    extensionality2 λ a⁺ b⁻ → trans-refl (a⁺ † b⁻))
              ▸𝒾: (λ _ → refl)

max_stars_repo_name: mstone/poly

max_issues_repo_name: dspivak/poly

max_forks_repo_name: dspivak/poly


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

module Agda.Builtin.IO where

postulate IO : ∀ {a} → Set a → Set a
{-# BUILTIN IO IO #-}

{-# FOREIGN GHC type AgdaIO a b = IO b #-}
{-# COMPILE GHC IO = type MAlonzo.Code.Agda.Builtin.IO.AgdaIO #-}

max_stars_repo_name: Blaisorblade/Agda

max_issues_repo_name: Blaisorblade/Agda

max_forks_repo_name: Blaisorblade/Agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Structures.Semigroup where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma

open import Cubical.Foundations.SIP renaming (SNS-PathP to SNS)
open import Cubical.Structures.NAryOp

private
  variable
    ℓ ℓ' : Level

raw-semigroup-structure : Type ℓ → Type ℓ
raw-semigroup-structure X = X → X → X

raw-semigroup-is-SNS : SNS {ℓ} raw-semigroup-structure _
raw-semigroup-is-SNS = nAryFunSNS 2

semigroup-axioms : (X : Type ℓ) → raw-semigroup-structure X → Type ℓ
semigroup-axioms X _·_ = isSet X ×
                         ((x y z : X) → (x · (y · z)) ≡ ((x · y) · z))

semigroup-structure : Type ℓ → Type ℓ
semigroup-structure = add-to-structure (raw-semigroup-structure) semigroup-axioms

Semigroup : Type (ℓ-suc ℓ)
Semigroup {ℓ} = TypeWithStr ℓ semigroup-structure

-- Operations for extracting components

⟨_⟩ : Semigroup → Type ℓ
⟨ G , _ ⟩ = G

semigroup-operation : (G : Semigroup {ℓ}) → ⟨ G ⟩ → ⟨ G ⟩ → ⟨ G ⟩
semigroup-operation (_ , f , _) = f

module semigroup-operation-syntax where

  semigroup-operation-syntax : (G : Semigroup {ℓ}) → ⟨ G ⟩ → ⟨ G ⟩ → ⟨ G ⟩
  semigroup-operation-syntax = semigroup-operation

  infixl 20 semigroup-operation-syntax
  syntax semigroup-operation-syntax G x y = x ·⟨ G ⟩ y

open semigroup-operation-syntax

semigroup-isSet : (G : Semigroup {ℓ}) → isSet ⟨ G ⟩
semigroup-isSet (_ , _ , P , _) = P

semigroup-assoc : (G : Semigroup {ℓ})
                → (x y z : ⟨ G ⟩) → (x ·⟨ G ⟩ (y ·⟨ G ⟩ z)) ≡ ((x ·⟨ G ⟩ y) ·⟨ G ⟩ z)
semigroup-assoc (_ , _ , _ , P) = P

-- Semigroup equivalences

semigroup-iso : StrIso semigroup-structure ℓ
semigroup-iso = add-to-iso (nAryFunIso 2) semigroup-axioms

semigroup-axiom-isProp : (X : Type ℓ)
                       → (s : raw-semigroup-structure X)
                       → isProp (semigroup-axioms X s)
semigroup-axiom-isProp X _·_ = isPropΣ isPropIsSet
                               λ isSetX →  isPropΠ (λ x → isPropΠ (λ y → isPropΠ (λ z → isSetX _ _)))

semigroup-is-SNS : SNS {ℓ} semigroup-structure semigroup-iso
semigroup-is-SNS = add-axioms-SNS _ semigroup-axiom-isProp (nAryFunSNS 2)

SemigroupPath : (M N : Semigroup {ℓ}) → (M ≃[ semigroup-iso ] N) ≃ (M ≡ N)
SemigroupPath = SIP semigroup-is-SNS

-- Semigroup ·syntax

module semigroup-·syntax (G : Semigroup {ℓ}) where

  infixr 18 _·_

  _·_ : ⟨ G ⟩ → ⟨ G ⟩ → ⟨ G ⟩
  _·_ = semigroup-operation G


text:
open import Data.Char using ( Char )
open import Data.Bool using ( Bool )

module Data.Char.Classifier.Primitive where

postulate
  isAscii  : Char → Bool
  isLatin1 : Char → Bool
  isControl : Char → Bool
  isSpace : Char → Bool
  isLower : Char → Bool
  isUpper : Char → Bool
  isAlpha : Char → Bool
  isAlphaNum : Char → Bool
  isPrint : Char → Bool
  isDigit : Char → Bool
  isOctDigit : Char → Bool
  isHexDigit : Char → Bool

{-# IMPORT Data.Char #-}
{-# COMPILED isAscii Data.Char.isAscii  #-}
{-# COMPILED isLatin1 Data.Char.isLatin1 #-}
{-# COMPILED isControl Data.Char.isControl #-}
{-# COMPILED isSpace Data.Char.isSpace #-}
{-# COMPILED isLower Data.Char.isLower #-}
{-# COMPILED isUpper Data.Char.isUpper #-}
{-# COMPILED isAlpha Data.Char.isAlpha #-}
{-# COMPILED isAlphaNum Data.Char.isAlphaNum #-}
{-# COMPILED isPrint Data.Char.isPrint #-}
{-# COMPILED isDigit Data.Char.isDigit #-}
{-# COMPILED isOctDigit Data.Char.isOctDigit #-}
{-# COMPILED isHexDigit Data.Char.isHexDigit #-}

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Presheaf.Base where

open import Cubical.Foundations.Prelude

open import Cubical.Categories.Category
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.Instances.Functors

PreShv : ∀ {ℓ ℓ'} → Category ℓ ℓ' → (ℓS : Level)
       → Category (ℓ-max (ℓ-max ℓ ℓ') (ℓ-suc ℓS))
                  (ℓ-max (ℓ-max ℓ ℓ') ℓS)
PreShv C ℓS = FUNCTOR (C ^op) (SET ℓS)

max_stars_repo_name: FernandoLarrain/cubical


text:
------------------------------------------------------------------------------
-- Issue 12
------------------------------------------------------------------------------

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

module Issue12 where

postulate
  D : Set
  ∃ : (A : D → Set) → Set

postulate foo : (B C : D → Set) → ∃ C → ∃ C
{-# ATP prove foo #-}

postulate bar : (B C : D → Set) → ∃ B → ∃ B
{-# ATP prove bar #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
-- Andreas, 2012-04-18, bug reported by sanzhiyan
-- {-# OPTIONS -v tc.with:100 #-}
module Issue610-4 where

import Common.Level
open import Common.Equality

data ⊥ : Set where
record ⊤ : Set where

record A : Set₁ where
  constructor set
  field
    .a : Set

.ack : A → Set
ack x = A.a x

hah : set ⊤ ≡ set ⊥
hah = refl

-- SHOULD FAIL for the same reason that the next decl fails
.moo : ⊥
moo with cong ack hah
moo | q = subst (λ x → x) q _

{- FAILS
.moo' : ⊥
moo' = subst (λ x → x) (cong ack hah) _
-}

baa : .⊥ → ⊥
baa ()

yoink : ⊥
yoink = baa moo

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2012-11-13 issue reported by joshkos
module Issue754 where

data RDesc (I : Set) : Set₁ where
  ∎  : RDesc I
  ṿ  : (i : I) → RDesc I
  σ  : (S : Set) (D : S → RDesc I) → RDesc I

data ROrn {I J} (e : J → I) : RDesc I → RDesc J → Set₁ where
  ∎ : ROrn e ∎ ∎
  ṿ : ∀ j i → ROrn e (ṿ i) (ṿ j)
  σ : (S : Set) → ∀ {D E} (O : ∀ s → ROrn e (D s) (E s)) → ROrn e (σ S D) (σ S E)
  Δ : (T : Set) → ∀ {D E} (O : ∀ t → ROrn e D (E t)) → ROrn e D (σ T E)

scROrn : ∀ {I J K} {e : J → I} {f : K → J} {D E F} → ROrn e D E → ROrn f E F → ROrn (λ x → e (f x)) D F
scROrn         ∎        ∎        = ∎
scROrn {e = e} ∎        (Δ T P)  = Δ T λ t → scROrn {e = e} ∎ (P t)  -- culprit?
scROrn         (ṿ j i)  (ṿ k .j) = ṿ k i
scROrn {e = e} (ṿ j i)  (Δ T P)  = Δ T λ t → scROrn {e = e} (ṿ j i) (P t)  -- culprit?
scROrn         (σ S O)  (σ .S P) = σ S λ s → scROrn (O s) (P s)
scROrn         (σ S O)  (Δ T P)  = Δ T λ t → scROrn (σ S O) (P t)  -- culprit?
scROrn         (Δ T O)  (σ .T P) = Δ T λ t → scROrn (O t) (P t)
scROrn         (Δ T O)  (Δ T' P) = Δ T' λ t → scROrn (Δ T O) (P t)

-- Internal error message was:
-- blowUpSparseVec (n = 2) aux i=3 j=3 length l = 2

-- The error was triggered by some operations on matrix-shaped orders
-- which did not preserve the internal invariants of sparse matrices.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
---------------------------------------------------------------
-- This file contains the definitions of several versions of --
-- subcategories.                                            --
---------------------------------------------------------------
module Category.Subcategory where

open import Level
open import Data.Product

open import Setoid.Total
open import Relation.Relation
open import Category.Category

open Setoid
open SetoidFun
open Pred
open Subcarrier
open EqRel
open Cat

-- Categorical Predicate: A predicate on objects, and morphisms such
-- that the latter is closed under identities and composition.
record CatPred {l : Level} (ℂ : Cat {l}) : Set (lsuc l) where
  field
      oinc : Obj ℂ → Set l
      minc : ∀{A B} → oinc A → oinc B → Pred {l} (Hom ℂ A B)
      cp-idPf : ∀{A} → {p : oinc A} → pf (minc p p) (id ℂ {A})
      cp-compPf : ∀{A B C} → (op₁ : (oinc A))
                        → (op₂ : (oinc B))
                        → (op₃ : (oinc C))
                        → {f : el (Hom ℂ A B)}
                        → {g : el (Hom ℂ B C)}
                        → (pf (minc op₁ op₂) f)
                        → (pf (minc op₂ op₃) g)
                        → (pf (minc op₁ op₃) (f ○[ comp ℂ ] g))
open CatPred

-- Subcategories:

-- The restriction of a category ℂ to the category determined by the
-- categorical predicate P.  Note that the objects of this category
-- are pairs of an object and a proof that the object belongs in the
-- category, and morphisms are similarly defined but using setoid
-- predicates.
subcatPred : {l : Level}{ℂ : Cat {l}}
  → (P : CatPred ℂ)
  → Cat {l}
subcatPred {_}{ℂ} P =
  record
    { Obj = Σ[ x ∈ Obj ℂ ]( oinc P x)
    ; Hom = λ AP BP → let A = proj₁ AP
                          B = proj₁ BP
                          op₁ = proj₂ AP
                          op₂ = proj₂ BP
                      in Subsetoid (Hom ℂ A B) (minc P op₁ op₂)
    ; comp = λ {AP}{BP}{CP} →
             let A = proj₁ AP
                 B = proj₁ BP
                 C = proj₁ CP
                 op₁ = proj₂ AP
                 op₂ = proj₂ BP
                 op₃ = proj₂ CP
             in record {
                  appT = λ x →
                           record {
                             appT = λ x₁ →
                                      record { subel = (subel x) ○[ comp ℂ ] (subel x₁) ;
                                               insub = cp-compPf P op₁ op₂ op₃ (insub x) (insub x₁) } ;
                             extT = λ {y} {z} x₂ → eq-comp-right {_}{ℂ}{A}{B}{C}{subel x}{subel y}{subel z} x₂ } ;
                  extT = λ {f₁}{f₂} pf g₂ → extT (comp ℂ) pf (subel g₂) }
    ; id = λ {AP} → let A = proj₁ AP
                        A-op = proj₂ AP
                    in record { subel = id ℂ ; insub = cp-idPf P {_}{A-op} }
    ; assocPf = assocPf ℂ
    ; idPfCom = idPfCom ℂ
    ; idPf = idPf ℂ
    }

-- Subcategories using subsetoids.
subcat : {l : Level}
  → (ℂ : Cat {l})(O : Set l)
  → (oinc : O → Obj ℂ)
  → (minc : ∀{A B} → Pred {l} (Hom ℂ (oinc A) (oinc B)))
  → (∀{A} → pf (minc {A}{A}) (id ℂ {oinc A}))
  → (∀{A B C}
         → {f : el (Hom ℂ (oinc A) (oinc B))}
         → {g : el (Hom ℂ (oinc B) (oinc C))}
         → (pf minc f)
         → (pf minc g)
         → (pf minc (f ○[ comp ℂ ] g)))
  → Cat {l}
subcat ℂ O oinc minc idPF compPF =
  record {
    Obj = O;
    Hom = λ A B → Subsetoid (Hom ℂ (oinc A) (oinc B)) (minc {A}{B});
    comp = λ {A} {B} {C} →
      record { appT = λ x →
                record { appT = λ x₁ →
                              record { subel = (subel x) ○[ comp ℂ ] (subel x₁);
                                       insub = compPF {f = subel x}{subel x₁} (insub x) (insub x₁) };
                         extT =  λ {y}{z} p → extT (appT (comp ℂ {oinc A}{oinc B}{oinc C}) (subel x)) {subel y}{subel z} p };
               extT = λ {y}{z} x₁ x₂ → extT (comp ℂ {oinc A} {oinc B} {oinc C}) x₁ (subel x₂) };
    id = λ {A} → record { subel = id ℂ {oinc A}; insub = idPF {A} };
    assocPf = assocPf ℂ;
    idPf = idPf ℂ;
    idPfCom = idPfCom ℂ
  }

-- An alternate definition of a subcategory where the predicate is not
-- a setoid predicate.
subcat-pred : {l : Level}
  → (ℂ : Cat {l})(O : Set l)
  → (oinc : O → Obj ℂ)
  → (minc : ∀{A B} → el (Hom ℂ (oinc A) (oinc B)) → Set l)
  → (∀{A} → minc (id ℂ {oinc A}))
  → (∀{A B C}
         → {f : el (Hom ℂ (oinc A) (oinc B))}
         → {g : el (Hom ℂ (oinc B) (oinc C))}
         → (minc f)
         → (minc g)
         → (minc (f ○[ comp ℂ ] g)))
  → Cat {l}
subcat-pred ℂ O oinc minc idPF compPF =
    record {
      Obj = O;
      Hom = λ A B → ↓Setoid (Hom ℂ (oinc A) (oinc B)) (minc {A}{B});
     comp = λ {A} {B} {C} → ↓BinSetoidFun (comp ℂ) compPF;
       id = (id ℂ , idPF);
  assocPf = assocPf ℂ;
     idPf = idPf ℂ;
     idPfCom = idPfCom ℂ}

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
-- Andreas, 2019-06-26, issue #3872, make --no-forcing a pragma option

{-# OPTIONS --no-forcing #-}

open import Agda.Builtin.Nat

data List {a} (A : Set a) : Set a where
  [] : List A
  _∷_ : A → List A → List A

pattern [_] x = x ∷ []

module _ {a} {A : Set a} where

  _++_ : List A → List A → List A
  []       ++ ys = ys
  (x ∷ xs) ++ ys = x ∷ (xs ++ ys)

  variable
    x y z : A
    @0 xs ys zs : List A

  data FSet : List A → Set a where
    ∅   : FSet []
    _∪_ : FSet xs → FSet ys → FSet (xs ++ ys)
    sg  : (x : A) → FSet [ x ]
    -- x is forced here, but this is not wanted.
    -- We need a way to tell the forcing machinery to not erase x.

  -- Since xs is erased, we cannot get x from sg x : FSet xs (with xs = [ x ])
  -- unless x is retained in sg x.
  elements : {@0 xs : List A} → FSet xs → List A
  elements ∅       = []
  elements (s ∪ t) = elements s ++ elements t
  elements (sg x)  = [ x ]

-- ERROR WAS:
-- Variable x is declared erased, so it cannot be used here
-- when checking that the expression x has type A

mySet = (sg 1 ∪ sg 2) ∪ (sg 3 ∪ sg 4)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly-Quotient where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat
open import Cubical.Data.Vec
open import Cubical.Data.Vec.OperationsNat
open import Cubical.Data.FinData

open import Cubical.Relation.Nullary

open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.QuotientRing
open import Cubical.Algebra.CommRing.Instances.Int renaming (ℤCommRing to ℤCR)

open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly
  renaming (PolyCommRing to A[X1,···,Xn] ; Poly to A[x1,···,xn])

private variable
  ℓ : Level

-----------------------------------------------------------------------------
-- General Nth polynome / quotient
-- Better to declare an alias

PolyCommRing-Quotient : (A : CommRing ℓ) → {n m : ℕ} → FinVec (fst (A[X1,···,Xn] A n)) m → CommRing ℓ
PolyCommRing-Quotient A {n} {m} v = A[X1,···,Xn] A n / genIdeal (A[X1,···,Xn] A n) v

-----------------------------------------------------------------------------
-- Notation in the general case and some real cases 1, 2, 3

module _
  (Ar@(A , Astr) : CommRing ℓ)
  (n : ℕ)
  where

  <Xkʲ> : (k j : ℕ) →  FinVec (A[x1,···,xn] Ar n) 1
  <Xkʲ> k j zero = base (genδℕ-Vec n k j 0) (CommRingStr.1r Astr)

  A[X1,···,Xn]/<Xkʲ> : (k j : ℕ) → CommRing ℓ
  A[X1,···,Xn]/<Xkʲ> k j = (A[X1,···,Xn] Ar n) / (genIdeal ((A[X1,···,Xn] Ar n)) (<Xkʲ> k j))

  A[x1,···,xn]/<xkʲ> : (k j : ℕ) → Type ℓ
  A[x1,···,xn]/<xkʲ> k j = fst (A[X1,···,Xn]/<Xkʲ> k j)

  <X1,···,Xn> : FinVec (A[x1,···,xn] Ar n) n
  <X1,···,Xn> = λ k → base (δℕ-Vec n (toℕ k)) (CommRingStr.1r Astr)

  A[X1,···,Xn]/<X1,···,Xn> : CommRing ℓ
  A[X1,···,Xn]/<X1,···,Xn> = (A[X1,···,Xn] Ar n) / (genIdeal ((A[X1,···,Xn] Ar n)) <X1,···,Xn>)

  A[x1,···,xn]/<x1,···,xn> : Type ℓ
  A[x1,···,xn]/<x1,···,xn> = fst A[X1,···,Xn]/<X1,···,Xn>


text:
------------------------------------------------------------------------
-- Examples showing how Tree-sort can be used
------------------------------------------------------------------------

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

open import Equality

module Tree-sort.Examples
  {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Prelude

open import Bag-equivalence eq
import Nat eq as Nat

-- Comparison functions for natural numbers.

_≤?_ : ℕ → ℕ → Bool
m ≤? n with Nat.total m n
... | inj₁ m≤n = true
... | inj₂ n<m = false

import Tree-sort.Partial eq _≤?_ as P
open import Tree-sort.Full eq Nat._≤_ Nat.total as F using (cons; nil)

-- The sort functions return ordered lists.

orderedP : P.tree-sort (3 ∷ 1 ∷ 2 ∷ []) ≡ 1 ∷ 2 ∷ 3 ∷ []
orderedP = refl _

orderedF : F.tree-sort (3 ∷ 1 ∷ 2 ∷ []) ≡
           cons 1 (cons 2 (cons 3 (nil _) _) _) _
orderedF = refl _

-- The sort functions return lists which are bag equivalent to the
-- input. This property can be used to establish bag equivalences
-- between concrete lists.

a-bag-equivalenceP : 1 ∷ 2 ∷ 3 ∷ [] ≈-bag 3 ∷ 1 ∷ 2 ∷ []
a-bag-equivalenceP = P.tree-sort-permutes (3 ∷ 1 ∷ 2 ∷ [])

a-bag-equivalenceF : 1 ∷ 2 ∷ 3 ∷ [] ≈-bag 3 ∷ 1 ∷ 2 ∷ []
a-bag-equivalenceF = F.tree-sort-permutes (3 ∷ 1 ∷ 2 ∷ [])

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality