text:
-- Limits.
-- Heavily inspired by https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/limits/graphs/limits.v
-- (except we're using categories instead of graphs to index limits)

{-# OPTIONS --safe #-}
module Cubical.Categories.Limits.Limits where

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

open import Cubical.Data.Sigma.Base

open import Cubical.Categories.Category
open import Cubical.Categories.Functor

open import Cubical.HITs.PropositionalTruncation.Base

module _ {ℓJ ℓJ' ℓC ℓC' : Level} {J : Category ℓJ ℓJ'} {C : Category ℓC ℓC'} where
  open Category
  open Functor

  private
    ℓ = ℓ-max (ℓ-max (ℓ-max ℓJ ℓJ') ℓC) ℓC'

  record Cone (D : Functor J C) (c : ob C) : Type (ℓ-max (ℓ-max ℓJ ℓJ') ℓC') where
    constructor cone

    field
      coneOut : (v : ob J) → C [ c , F-ob D v ]
      coneOutCommutes : {u v : ob J} (e : J [ u , v ]) →
                        coneOut u ⋆⟨ C ⟩ D .F-hom e ≡ coneOut v

  open Cone

  cone≡ : {D : Functor J C} {c : ob C} → {c1 c2 : Cone D c}
        → ((v : ob J) → coneOut c1 v ≡ coneOut c2 v) → c1 ≡ c2
  coneOut (cone≡ h i) v = h v i
  coneOutCommutes (cone≡ {D} {_} {c1} {c2} h i) {u} {v} e =
    isProp→PathP (λ j → isSetHom C (h u j ⋆⟨ C ⟩ D .F-hom e) (h v j))
                 (coneOutCommutes c1 e) (coneOutCommutes c2 e) i

  -- TODO: can we automate this a bit?
  isSetCone : (D : Functor J C) (c : ob C) → isSet (Cone D c)
  isSetCone D c = isSetRetract toConeΣ fromConeΣ (λ _ → refl)
                               (isSetΣSndProp (isSetΠ (λ _ → isSetHom C))
                                              (λ _ → isPropImplicitΠ2 (λ _ _ → isPropΠ (λ _ → isSetHom C _ _))))
    where
    ConeΣ = Σ[ f ∈ ((v : ob J) → C [ c , F-ob D v ]) ]
               ({u v : ob J} (e : J [ u , v ]) → f u ⋆⟨ C ⟩ D .F-hom e ≡ f v)

    toConeΣ : Cone D c → ConeΣ
    fst (toConeΣ x) = coneOut x
    snd (toConeΣ x) = coneOutCommutes x

    fromConeΣ : ConeΣ → Cone D c
    coneOut (fromConeΣ x) = fst x
    coneOutCommutes (fromConeΣ x) = snd x

  isConeMor : {c1 c2 : ob C} {D : Functor J C}
              (cc1 : Cone D c1) (cc2 : Cone D c2)
            → C [ c1 , c2 ] → Type (ℓ-max ℓJ ℓC')
  isConeMor cc1 cc2 f = (v : ob J) → f ⋆⟨ C ⟩ coneOut cc2 v ≡ coneOut cc1 v

  isPropIsConeMor : {c1 c2 : ob C} {D : Functor J C}
                    (cc1 : Cone D c1) (cc2 : Cone D c2) (f : C [ c1 , c2 ])
                  → isProp (isConeMor cc1 cc2 f)
  isPropIsConeMor cc1 cc2 f = isPropΠ (λ _ → isSetHom C _ _)

  isLimCone : (D : Functor J C) (c0 : ob C) → Cone D c0 → Type ℓ
  isLimCone D c0 cc0 = (c : ob C) → (cc : Cone D c)
                     → ∃![ f ∈ C [ c , c0 ] ] isConeMor cc cc0 f

  isPropIsLimCone : (D : Functor J C) (c0 : ob C) (cc0 : Cone D c0)
                  → isProp (isLimCone D c0 cc0)
  isPropIsLimCone D c0 cc0 = isPropΠ2 λ _ _ → isProp∃!

  record LimCone (D : Functor J C) : Type ℓ where
    constructor climCone

    field
      lim : ob C
      limCone : Cone D lim
      univProp : isLimCone D lim limCone

    limOut : (v : ob J) → C [ lim , D .F-ob v ]
    limOut = coneOut limCone

    limOutCommutes : {u v : ob J} (e : J [ u , v ])
                   → limOut u ⋆⟨ C ⟩ D .F-hom e ≡ limOut v
    limOutCommutes = coneOutCommutes limCone

    limArrow : (c : ob C) → (cc : Cone D c) → C [ c , lim ]
    limArrow c cc = univProp c cc .fst .fst

    limArrowCommutes : (c : ob C) → (cc : Cone D c) (u : ob J)
                     → limArrow c cc ⋆⟨ C ⟩ limOut u ≡ coneOut cc u
    limArrowCommutes c cc = univProp c cc .fst .snd

    limArrowUnique : (c : ob C) → (cc : Cone D c) (k : C [ c , lim ])
                   → isConeMor cc limCone k → limArrow c cc ≡ k
    limArrowUnique c cc k hk = cong fst (univProp c cc .snd (k , hk))

  open LimCone
  limOfArrows : (D₁ D₂ : Functor J C)
                (CC₁ : LimCone D₁) (CC₂ : LimCone D₂)
                (f : (u : ob J) → C [ D₁ .F-ob u , D₂ .F-ob u ])
                (fNat : {u v : ob J} (e : J [ u , v ])
                      →  f u ⋆⟨ C ⟩ D₂ .F-hom e ≡ D₁ .F-hom e ⋆⟨ C ⟩ f v)
              → C [ CC₁ .lim , CC₂ .lim ]
  limOfArrows D₁ D₂ CC₁ CC₂ f fNat = limArrow CC₂ (CC₁ .lim) coneD₂Lim₁
   where
   coneD₂Lim₁ : Cone D₂ (CC₁ .lim)
   coneOut coneD₂Lim₁ v = limOut CC₁ v ⋆⟨ C ⟩ f v
   coneOutCommutes coneD₂Lim₁ {u = u} {v = v} e =
     limOut CC₁ u ⋆⟨ C ⟩ f u ⋆⟨ C ⟩ D₂ .F-hom e   ≡⟨ ⋆Assoc C _ _ _ ⟩
     limOut CC₁ u ⋆⟨ C ⟩ (f u ⋆⟨ C ⟩ D₂ .F-hom e) ≡⟨ cong (λ x → seq' C (limOut CC₁ u) x) (fNat e) ⟩
     limOut CC₁ u ⋆⟨ C ⟩ (D₁ .F-hom e ⋆⟨ C ⟩ f v) ≡⟨ sym (⋆Assoc C _ _ _) ⟩
     limOut CC₁ u ⋆⟨ C ⟩ D₁ .F-hom e ⋆⟨ C ⟩ f v   ≡⟨ cong (λ x → x ⋆⟨ C ⟩ f v) (limOutCommutes CC₁ e) ⟩
     limOut CC₁ v ⋆⟨ C ⟩ f v ∎

-- A category is complete if it has all limits
Limits : {ℓJ ℓJ' ℓC ℓC' : Level} → Category ℓC ℓC' → Type _
Limits {ℓJ} {ℓJ'} C = (J : Category ℓJ ℓJ') → (D : Functor J C) → LimCone D

hasLimits : {ℓJ ℓJ' ℓC ℓC' : Level} → Category ℓC ℓC' → Type _
hasLimits {ℓJ} {ℓJ'} C = (J : Category ℓJ ℓJ') → (D : Functor J C) → ∥ LimCone D ∥

-- Limits of a specific shape J in a category C
LimitsOfShape : {ℓJ ℓJ' ℓC ℓC' : Level} → Category ℓJ ℓJ' → Category ℓC ℓC' → Type _
LimitsOfShape J C = (D : Functor J C) → LimCone D

-- Preservation of limits

module _ {ℓJ ℓJ' ℓC1 ℓC1' ℓC2 ℓC2' : Level}
         {C1 : Category ℓC1 ℓC1'} {C2 : Category ℓC2 ℓC2'}
         (F : Functor C1 C2) where
  open Category
  open Functor
  open Cone

  private
    ℓ = ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓJ ℓJ') ℓC1) ℓC1') ℓC2) ℓC2'

  mapCone : {J : Category ℓJ ℓJ'} (D : Functor J C1) {x : ob C1} (ccx : Cone D x) → Cone (funcComp F D) (F .F-ob x)
  coneOut (mapCone D ccx) v = F .F-hom (coneOut ccx v)
  coneOutCommutes (mapCone D ccx) e =
    sym (F-seq F (coneOut ccx _) (D ⟪ e ⟫)) ∙ cong (F .F-hom) (coneOutCommutes ccx e)

  preservesLimit : {J : Category ℓJ ℓJ'} (D : Functor J C1)
                 → (L : ob C1) → Cone D L → Type ℓ
  preservesLimit D L ccL =
    isLimCone D L ccL → isLimCone (funcComp F D) (F .F-ob L) (mapCone D ccL)

  -- TODO: prove that right adjoints preserve limits


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

open import Categories.Category
open import Categories.Object.Zero

-- Cokernels of morphisms.
-- https://ncatlab.org/nlab/show/cokernel
module Categories.Object.Cokernel {o ℓ e} {𝒞 : Category o ℓ e} (𝟎 : Zero 𝒞) where

open import Level

open import Categories.Morphism 𝒞
open import Categories.Morphism.Reasoning 𝒞
  hiding (glue)

open Category 𝒞
open Zero 𝟎

open HomReasoning

private
  variable
    A B X : Obj
    f h i j k : A ⇒ B

record IsCokernel {A B K} (f : A ⇒ B) (k : B ⇒ K) : Set (o ⊔ ℓ ⊔ e) where
  field
    commute   : k ∘ f ≈ zero⇒
    universal : ∀ {X} {h : B ⇒ X} → h ∘ f ≈ zero⇒ → K ⇒ X
    factors   : ∀ {eq : h ∘ f ≈ zero⇒} → h ≈ universal eq ∘ k
    unique    : ∀ {eq : h ∘ f ≈ zero⇒} → h ≈ i ∘ k → i ≈ universal eq

  universal-resp-≈ : ∀ {eq : h ∘ f ≈ zero⇒} {eq′ : i ∘ f ≈ zero⇒} →
    h ≈ i → universal eq ≈ universal eq′
  universal-resp-≈ h≈i = unique (⟺ h≈i ○ factors)

  universal-∘ : h ∘ k ∘ f ≈ zero⇒
  universal-∘ {h = h} = begin
    h ∘ k ∘ f ≈⟨ refl⟩∘⟨ commute ⟩
    h ∘ zero⇒ ≈⟨ zero-∘ˡ h ⟩
    zero⇒     ∎

record Cokernel {A B} (f : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
  field
    {cokernel} : Obj
    cokernel⇒  : B ⇒ cokernel
    isCokernel : IsCokernel f cokernel⇒

  open IsCokernel isCokernel public

IsCokernel⇒Cokernel : IsCokernel f k → Cokernel f
IsCokernel⇒Cokernel {k = k} isCokernel = record
  { cokernel⇒ = k
  ; isCokernel = isCokernel
  }

ext: agda

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
 {-# OPTIONS --type-in-type #-}

module DescTT where

--********************************************
-- Prelude
--********************************************

-- Some preliminary stuffs, to avoid relying on the stdlib

--****************
-- Sigma and friends
--****************

data Sigma (A : Set) (B : A -> Set) : Set where
  _,_ : (x : A) (y : B x) -> Sigma A B

_*_ : (A : Set)(B : Set) -> Set
A * B = Sigma A \_ -> B

fst : {A : Set}{B : A -> Set} -> Sigma A B -> A
fst (a , _) = a

snd : {A : Set}{B : A -> Set} (p : Sigma A B) -> B (fst p)
snd (a , b) = b

data Zero : Set where
data Unit  : Set where
  Void : Unit

--****************
-- Sum and friends
--****************

data _+_ (A : Set)(B : Set) : Set where
  l : A -> A + B
  r : B -> A + B

--****************
-- Equality
--****************

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

cong : {A B : Set}(f : A -> B){x y : A} -> x == y -> f x == f y
cong f refl = refl

cong2 : {A B C : Set}(f : A -> B -> C){x y : A}{z t : B} ->
        x == y -> z == t -> f x z == f y t
cong2 f refl refl = refl

postulate
  reflFun : {A : Set}{B : A -> Set}(f : (a : A) -> B a)(g : (a : A) -> B a)-> ((a : A) -> f a == g a) -> f == g

--********************************************
-- Desc code
--********************************************

data Desc : Set where
  id : Desc
  const : Set -> Desc
  prod : Desc -> Desc -> Desc
  sigma : (S : Set) -> (S -> Desc) -> Desc
  pi : (S : Set) -> (S -> Desc) -> Desc

--********************************************
-- Desc interpretation
--********************************************

[|_|]_ : Desc -> Set -> Set
[| id |] Z        = Z
[| const X |] Z   = X
[| prod D D' |] Z = [| D |] Z * [| D' |] Z
[| sigma S T |] Z = Sigma S (\s -> [| T s |] Z)
[| pi S T |] Z    = (s : S) -> [| T s |] Z

--********************************************
-- Fixpoint construction
--********************************************

data Mu (D : Desc) : Set where
  con : [| D |] (Mu D) -> Mu D

--********************************************
-- Predicate: All
--********************************************

All : (D : Desc)(X : Set)(P : X -> Set) -> [| D |] X -> Set
All id          X P x        = P x
All (const Z)   X P x        = Unit
All (prod D D') X P (d , d') = (All D X P d) * (All D' X P d')
All (sigma S T) X P (a , b)  = All (T a) X P b
All (pi S T)    X P f        = (s : S) -> All (T s) X P (f s)

all : (D : Desc)(X : Set)(P : X -> Set)(R : (x : X) -> P x)(x : [| D |] X) -> All D X P x
all id X P R x = R x
all (const Z) X P R z = Void
all (prod D D') X P R (d , d') = all D X P R d , all D' X P R d'
all (sigma S T) X P R (a , b) = all (T a) X P R b
all (pi S T) X P R f = \ s -> all (T s) X P R (f s)

--********************************************
-- Map
--********************************************

map : (D : Desc)(X Y : Set)(f : X -> Y)(v : [| D |] X) -> [| D |] Y
map id X Y sig x = sig x
map (const Z) X Y sig z = z
map (prod D D') X Y sig (d , d') = map D X Y sig d , map D' X Y sig d'
map (sigma S T) X Y sig (a , b) = (a , map (T a) X Y sig b)
map (pi S T) X Y sig f = \x -> map (T x) X Y sig (f x)

proof-map-id : (D : Desc)(X : Set)(v : [| D |] X) -> map D X X (\x -> x) v == v
proof-map-id id X v = refl
proof-map-id (const Z) X v = refl
proof-map-id (prod D D') X (v , v') = cong2 (\x y -> (x , y)) (proof-map-id D X v) (proof-map-id D' X v')
proof-map-id (sigma S T) X (a , b) = cong (\x -> (a , x)) (proof-map-id (T a) X b)
proof-map-id (pi S T) X f = reflFun (\a -> map (T a) X X (\x -> x) (f a)) f (\a -> proof-map-id (T a) X (f a))

proof-map-compos : (D : Desc)(X Y Z : Set)
                   (f : X -> Y)(g : Y -> Z)
                   (v : [| D |] X) ->
                   map D X Z (\x -> g (f x)) v == map D Y Z g (map D X Y f v)
proof-map-compos id X Y Z f g v = refl
proof-map-compos (const K) X Y Z f g v = refl
proof-map-compos (prod D D') X Y Z f g (v , v') = cong2 (\x y -> (x , y))
                                                        (proof-map-compos D X Y Z f g v)
                                                        (proof-map-compos D' X Y Z f g v')
proof-map-compos (sigma S T) X Y Z f g (a , b) = cong (\x -> (a , x)) (proof-map-compos (T a) X Y Z f g b)
proof-map-compos (pi S T) X Y Z f g fc = reflFun (\a -> map (T a) X Z (\x -> g (f x)) (fc a))
                                                 (\a -> map (T a) Y Z g (map (T a) X Y f (fc a)))
                                                 (\a -> proof-map-compos (T a) X Y Z f g (fc a))

--********************************************
-- Elimination principle: induction
--********************************************

{-
induction : (D : Desc)
            (P : Mu D -> Set) ->
            ( (x : [| D |] (Mu D)) ->
              All D (Mu D) P x -> P (con x)) ->
            (v : Mu D) ->
            P v
induction D P ms (con xs) = ms xs (all D (Mu D) P (\x -> induction D P ms x) xs)
-}

module Elim (D : Desc)
            (P : Mu D -> Set)
            (ms : (x : [| D |] (Mu D)) ->
                  All D (Mu D) P x -> P (con x))
       where

    mutual
        induction : (x : Mu D) -> P x
        induction (con xs) =  ms xs (hyps D xs)

        hyps : (D' : Desc)
               (xs : [| D' |] (Mu D)) ->
               All D' (Mu D) P xs
        hyps id x = induction x
        hyps (const Z) z = Void
        hyps (prod D D') (d , d') = hyps D d , hyps D' d'
        hyps (sigma S T) (a , b) = hyps (T a) b
        hyps (pi S T) f = \s -> hyps (T s) (f s)

induction : (D : Desc)
            (P : Mu D -> Set) ->
            ( (x : [| D |] (Mu D)) ->
              All D (Mu D) P x -> P (con x)) ->
            (v : Mu D) ->
            P v
induction D P ms x = Elim.induction D P ms x

--********************************************
-- Examples
--********************************************

--****************
-- Nat
--****************

data NatConst : Set where
  Ze : NatConst
  Suc : NatConst

natCases : NatConst -> Desc
natCases Ze = const Unit
natCases Suc = id

NatD : Desc
NatD = sigma NatConst natCases

Nat : Set
Nat = Mu NatD

ze : Nat
ze = con (Ze , Void)

suc : Nat -> Nat
suc n = con (Suc , n)

--****************
-- List
--****************

data ListConst : Set where
  Nil : ListConst
  Cons : ListConst

listCases : Set -> ListConst -> Desc
listCases X Nil = const Unit
listCases X Cons = sigma X (\_ -> id)

ListD : Set -> Desc
ListD X = sigma ListConst (listCases X)

List : Set -> Set
List X = Mu (ListD X)

nil : {X : Set} -> List X
nil = con ( Nil , Void )

cons : {X : Set} -> X -> List X -> List X
cons x t = con ( Cons , ( x , t ))

--****************
-- Tree
--****************

data TreeConst : Set where
  Leaf : TreeConst
  Node : TreeConst

treeCases : Set -> TreeConst -> Desc
treeCases X Leaf = const Unit
treeCases X Node = sigma X (\_ -> prod id id)

TreeD : Set -> Desc
TreeD X = sigma TreeConst (treeCases X)

Tree : Set -> Set
Tree X = Mu (TreeD X)

leaf : {X : Set} -> Tree X
leaf = con (Leaf , Void)

node : {X : Set} -> X -> Tree X -> Tree X -> Tree X
node x le ri = con (Node , (x , (le , ri)))

--********************************************
-- Finite sets
--********************************************

EnumU : Set
EnumU = Nat

nilE : EnumU
nilE = ze

consE : EnumU -> EnumU
consE e = suc e

{-
data EnumU : Set where
  nilE : EnumU
  consE : EnumU -> EnumU
-}

data EnumT : (e : EnumU) -> Set where
  EZe : {e : EnumU} -> EnumT (consE e)
  ESu : {e : EnumU} -> EnumT e -> EnumT (consE e)

casesSpi : (xs : [| NatD |] Nat) ->
           All NatD Nat (\e -> (P' : EnumT e -> Set) -> Set) xs ->
           (P' : EnumT (con xs) -> Set) -> Set
casesSpi (Ze , Void) hs P' = Unit
casesSpi (Suc , n) hs P' = P' EZe * hs (\e -> P' (ESu e))

spi : (e : EnumU)(P : EnumT e -> Set) -> Set
spi e P = induction NatD (\e -> (P : EnumT e -> Set) -> Set) casesSpi e  P

{-
spi : (e : EnumU)(P : EnumT e -> Set) -> Set
spi nilE P = Unit
spi (consE e) P = P EZe * spi e (\e -> P (ESu e))
-}

casesSwitch : (xs : [| NatD |] Nat) ->
              All NatD Nat (\e -> (P' : EnumT e -> Set)(b' : spi e P')(x' : EnumT e) -> P' x') xs ->
              (P' : EnumT (con xs) -> Set)(b' : spi (con xs) P')(x' : EnumT (con xs)) -> P' x'
casesSwitch (Ze , Void) hs P' b' ()
casesSwitch (Suc , n) hs P' b' EZe = fst b'
casesSwitch (Suc , n) hs P' b' (ESu e') = hs (\e -> P' (ESu e)) (snd b') e'

switch : (e : EnumU)(P : EnumT e -> Set)(b : spi e P)(x : EnumT e) -> P x
switch e P b x = induction NatD (\e -> (P : EnumT e -> Set)(b : spi e P)(x : EnumT e) -> P x) casesSwitch e P b x

{-
switch : (e : EnumU)(P : EnumT e -> Set)(b : spi e P)(x : EnumT e) -> P x
switch nilE P b ()
switch (consE e) P b EZe = fst b
switch (consE e) P b (ESu n) = switch e (\e -> P (ESu e)) (snd b) n
-}

--********************************************
-- Tagged description
--********************************************

TagDesc : Set
TagDesc = Sigma EnumU (\e -> spi e (\_ -> Desc))

toDesc : TagDesc -> Desc
toDesc (B , F) = sigma (EnumT B) (\e -> switch B (\_ -> Desc) F e)

--********************************************
-- Catamorphism
--********************************************

cata : (D : Desc)
       (T : Set) ->
       ([| D |] T -> T) ->
       (Mu D) -> T
cata D T phi x = induction D (\_ -> T) (\x ms -> phi (replace D T x ms)) x
  where replace : (D' : Desc)(T : Set)(xs : [| D' |] (Mu D))(ms : All D' (Mu D) (\_ -> T) xs) -> [| D' |] T
        replace id T x y = y
        replace (const Z) T z z' = z
        replace (prod D D') T (x , x') (y , y') = replace D T x y , replace D' T x' y'
        replace (sigma A B) T (a , b) t = a , replace (B a) T b t
        replace (pi A B) T f t = \s -> replace (B s) T (f s) (t s)

--********************************************
-- Free monad construction
--********************************************

_**_ : TagDesc -> (X : Set) -> TagDesc
(e , D) ** X = consE e , (const X , D)

--********************************************
-- Substitution
--********************************************

apply : (D : TagDesc)(X Y : Set) ->
        (X -> Mu (toDesc (D ** Y))) ->
        [| toDesc (D ** X) |] (Mu (toDesc (D ** Y))) ->
        Mu (toDesc (D ** Y))
apply (E , B) X Y sig (EZe , x) = sig x
apply (E , B) X Y sig (ESu n , t) = con (ESu n , t)

subst : (D : TagDesc)(X Y : Set) ->
        Mu (toDesc (D ** X)) ->
        (X -> Mu (toDesc (D ** Y))) ->
        Mu (toDesc (D ** Y))
subst D X Y x sig = cata (toDesc (D ** X)) (Mu (toDesc (D ** Y))) (apply D X Y sig) x

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram


text:
------------------------------------------------------------------------------
-- Testing the translation of definitions
------------------------------------------------------------------------------

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

module Definition12 where

infixl 9 _·_
infix  7 _≡_

postulate
  D       : Set
  _≡_     : D → D → Set
  true if : D
  _·_     : D → D → D

postulate if-true : ∀ d₁ {d₂} → if · true · d₁ · d₂ ≡ d₁
{-# ATP axiom if-true #-}

if_then_else_ : D → D → D → D
if b then d₁ else d₂ = if · b · d₁ · d₂
{-# ATP definition if_then_else_ #-}

-- We test the translation of a definition with holes.
postulate foo : ∀ d₁ d₂ → (if true then d₁ else d₂) ≡ d₁
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

open import Cubical.Core.Everything
open import Cubical.Foundations.Logic
open import Cubical.Foundations.Everything

private
  variable
    A : Type₀

infixr 20 _∷_
infix 30 _∈_

data LFSet (A : Type₀) : Type₀ where
  []    : LFSet A
  _∷_   : (x : A) → (xs : LFSet A) → LFSet A
  dup   : ∀ x xs   → x ∷ x ∷ xs ≡ x ∷ xs
  comm  : ∀ x y xs → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
  trunc : isSet (LFSet A)

-- Membership.
--
-- Doing some proofs with equational reasoning adds an extra "_∙ refl"
-- at the end.
-- We might want to avoid it, or come up with a more clever equational reasoning.
_∈_ : A → LFSet A → hProp _
z ∈ []                  = ⊥
z ∈ (y ∷ xs)            = (z ≡ₚ y) ⊔ (z ∈ xs)
z ∈ dup x xs i          = proof i
  where
    -- proof : z ∈ (x ∷ x ∷ xs) ≡ z ∈ (x ∷ xs)
    proof = z ≡ₚ x  ⊔ (z ≡ₚ x ⊔ z ∈ xs) ≡⟨ ⊔-assoc (z ≡ₚ x) (z ≡ₚ x) (z ∈ xs) ⟩
            (z ≡ₚ x ⊔ z ≡ₚ x) ⊔ z ∈ xs  ≡⟨ cong (_⊔ (z ∈ xs)) (⊔-idem (z ≡ₚ x)) ⟩
            z ≡ₚ x            ⊔ z ∈ xs  ∎
z ∈ comm x y xs i       = proof i
  where
    -- proof : z ∈ (x ∷ y ∷ xs) ≡ z ∈ (y ∷ x ∷ xs)
    proof = z ≡ₚ x  ⊔ (z ≡ₚ y ⊔ z ∈ xs) ≡⟨ ⊔-assoc (z ≡ₚ x) (z ≡ₚ y) (z ∈ xs) ⟩
            (z ≡ₚ x ⊔ z ≡ₚ y) ⊔ z ∈ xs  ≡⟨ cong (_⊔ (z ∈ xs)) (⊔-comm (z ≡ₚ x) (z ≡ₚ y)) ⟩
            (z ≡ₚ y ⊔ z ≡ₚ x) ⊔ z ∈ xs  ≡⟨ sym (⊔-assoc (z ≡ₚ y) (z ≡ₚ x) (z ∈ xs)) ⟩
            z ≡ₚ y  ⊔ (z ≡ₚ x ⊔ z ∈ xs) ∎

x ∈ trunc xs ys p q i j = isSetHProp (x ∈ xs) (x ∈ ys) (cong (x ∈_) p) (cong (x ∈_) q) i j

module LFSetElim {ℓ}
  (B : LFSet A → Type ℓ)
  ([]* : B [])
  (_∷*_ : (x : A) {xs : LFSet A} → B xs → B (x ∷ xs))
  (comm* : (x y : A) {xs : LFSet A} (b : B xs)
    → PathP (λ i → B (comm x y xs i)) (x ∷* (y ∷* b)) (y ∷* (x ∷* b)))
  (dup* : (x : A) {xs : LFSet A} (b : B xs)
    → PathP (λ i → B (dup x xs i)) (x ∷* (x ∷* b)) (x ∷* b))
  (trunc* : (xs : LFSet A) → isSet (B xs)) where

  f : ∀ x → B x
  f [] = []*
  f (x ∷ xs) = x ∷* f xs
  f (dup x xs i) = dup* x (f xs) i
  f (comm x y xs i) = comm* x y (f xs) i
  f (trunc x y p q i j) =
    isOfHLevel→isOfHLevelDep 2 trunc*
      (f x) (f y)
      (λ i → f (p i)) (λ i → f (q i))
      (trunc x y p q) i j

module LFSetRec {ℓ} {B : Type ℓ}
  ([]* : B)
  (_∷*_ : (x : A) → B → B)
  (comm* : (x y : A) (xs : B) → (x ∷* (y ∷* xs)) ≡ (y ∷* (x ∷* xs)))
  (dup* : (x : A) (b : B) → (x ∷* (x ∷* b)) ≡ (x ∷* b))
  (trunc* : isSet B) where

  f : LFSet A → B
  f = LFSetElim.f _
    []* (λ x xs → x ∷* xs)
    (λ x y b → comm* x y b) (λ x b → dup* x b)
    λ _ → trunc*

module LFPropElim {ℓ}
  (B : LFSet A → Type ℓ)
  ([]* : B []) (_∷*_ : (x : A) {xs : LFSet A} → B xs → B (x ∷ xs))
  (trunc* : (xs : LFSet A) → isProp (B xs)) where

  f : ∀ x → B x
  f = LFSetElim.f _
    []* _∷*_
    (λ _ _ _ → isOfHLevel→isOfHLevelDep 1 trunc* _ _ _)
    (λ _ _ → isOfHLevel→isOfHLevelDep 1 trunc* _ _ _)
    λ xs → isProp→isSet (trunc* xs)

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.ImplShared.Util.Dijkstra.RWS
open import LibraBFT.ImplShared.Util.Dijkstra.Syntax
open import LibraBFT.Prelude
open import Optics.All

-- This module contains definitions allowing RWS programs to be written using
-- Agda's do-notation, as well as convenient short names for operations
-- (including lens operations).
module LibraBFT.ImplShared.Util.Dijkstra.RWS.Syntax where

private
  variable
    Ev Wr St : Set
    A B C    : Set

-- From this instance declaration, we get _<$>_, pure, and _<*>_ also.
instance
  RWS-Monad : Monad (RWS Ev Wr St)
  Monad.return RWS-Monad = RWS-return
  Monad._>>=_  RWS-Monad = RWS-bind

-- These instance declarations give us variant conditional operations that we
-- can define to play nice with `RWS-weakestPre`

instance
  RWS-MonadIfD : MonadIfD{ℓ₃ = ℓ0} (RWS Ev Wr St)
  MonadIfD.monad RWS-MonadIfD = RWS-Monad
  MonadIfD.ifD‖  RWS-MonadIfD = RWS-if

  RWS-MonadMaybeD : MonadMaybeD (RWS Ev Wr St)
  MonadMaybeD.monad   RWS-MonadMaybeD = RWS-Monad
  MonadMaybeD.maybeSD RWS-MonadMaybeD = RWS-maybe

  RWS-MonadEitherD : MonadEitherD (RWS Ev Wr St)
  MonadEitherD.monad    RWS-MonadEitherD = RWS-Monad
  MonadEitherD.eitherSD RWS-MonadEitherD = RWS-either

gets : (St → A) → RWS Ev Wr St A
gets = RWS-gets

get : RWS Ev Wr St St
get = gets id

put : St → RWS Ev Wr St Unit
put = RWS-put

modify : (St → St) → RWS Ev Wr St Unit
modify f = do
  st ← get
  put (f st)

ask : RWS Ev Wr St Ev
ask = RWS-ask

tell : List Wr → RWS Ev Wr St Unit
tell = RWS-tell

tell1 : Wr → RWS Ev Wr St Unit
tell1 x = tell (x ∷ [])

act = tell1

void : RWS Ev Wr St A → RWS Ev Wr St Unit
void m = do
  _ ← m
  pure unit

-- -- Composition with error monad
ok : A → RWS Ev Wr St (B ⊎ A)
ok = pure ∘ Right

bail : B → RWS Ev Wr St (B ⊎ A)
bail = pure ∘ Left

infixl 4 _∙?∙_
_∙?∙_ : RWS Ev Wr St (Either C A) → (A → RWS Ev Wr St (Either C B)) → RWS Ev Wr St (Either C B)
_∙?∙_ = RWS-ebind

maybeSM : RWS Ev Wr St (Maybe A) → RWS Ev Wr St B → (A → RWS Ev Wr St B) → RWS Ev Wr St B
maybeSM mma mb f = do
  x ← mma
  caseMD x of λ where
    nothing  → mb
    (just j) → f j

maybeSMP-RWS : RWS Ev Wr St (Maybe A) → B → (A → RWS Ev Wr St B)
              → RWS Ev Wr St B
maybeSMP-RWS ma b f = do
  x ← ma
  caseMD x of λ where
    nothing  → pure b
    (just j) → f j

infixl 4 _∙^∙_
_∙^∙_ : RWS Ev Wr St (Either B A) → (B → B) → RWS Ev Wr St (Either B A)
m ∙^∙ f = do
  x ← m
  either (bail ∘ f) ok x

RWS-weakestPre-∙^∙Post : (ev : Ev) (e : C → C) → RWS-Post Wr St (C ⊎ A) → RWS-Post Wr St (C ⊎ A)
RWS-weakestPre-∙^∙Post ev e Post =
  RWS-weakestPre-bindPost ev (either (bail ∘ e) ok) Post

-- Lens functionality
--
-- If we make RWS work for different level State types, we will break use and
-- modify because Lens does not support different levels, we define use and
-- modify' here for RoundManager. We are ok as long as we can keep
-- RoundManager in Set. If we ever need to make RoundManager at some higher
-- Level, we will have to consider making Lens level-agnostic. Preliminary
-- exploration by @cwjnkins showed this to be somewhat painful in particular
-- around composition, so we are not pursuing it for now.
use : Lens St A → RWS Ev Wr St A
use f = gets (_^∙ f)

modifyL : Lens St A → (A → A) → RWS Ev Wr St Unit
modifyL l f = modify (over l f)
syntax modifyL l f = l %= f

setL : Lens St A → A → RWS Ev Wr St Unit
setL l x = l %= const x
syntax setL l x = l ∙= x

setL? : Lens St (Maybe A) → A → RWS Ev Wr St Unit
setL? l x = l ∙= just x
syntax setL? l x = l ?= x

max_stars_repo_name: oracle/bft-consensus-agda

max_issues_repo_name: oracle/bft-consensus-agda

max_forks_repo_name: oracle/bft-consensus-agda


text:
{-# OPTIONS --without-K #-}
module combination where

open import Type
open import Data.Nat.NP
open import Data.Nat.DivMod
open import Data.Fin using (Fin; Fin′; zero; suc) renaming (toℕ to Fin▹ℕ)
open import Data.Zero
open import Data.One
open import Data.Two
open import Data.Sum
open import Data.Product
open import Data.Vec
open import Function.NP
open import Function.Related.TypeIsomorphisms.NP
import Function.Inverse.NP as Inv
open Inv using (_↔_; sym; inverses; module Inverse) renaming (_$₁_ to to; _$₂_ to from; id to idI; _∘_ to _∘I_)
open import Relation.Binary.Product.Pointwise
open import Relation.Binary.Sum
import Relation.Binary.PropositionalEquality as ≡

open import factorial

_/_ : ℕ → ℕ → ℕ
x / y = _div_ x y {{!!}}

module v0 where

  C : ℕ → ℕ → ℕ
  C n       zero    = 1
  C zero    (suc k) = 0
  C (suc n) (suc k) = C n k + C n (suc k)

  D : ℕ → ℕ → ★
  D n       zero    = 𝟙
  D zero    (suc k) = 𝟘
  D (suc n) (suc k) = D n k ⊎ D n (suc k)

  FinC≅D : ∀ n k → Fin (C n k) ↔ D n k
  FinC≅D n       zero    = Fin1↔𝟙
  FinC≅D zero    (suc k) = Fin0↔𝟘
  FinC≅D (suc n) (suc k) =  FinC≅D n k ⊎-cong FinC≅D n (suc k)
                         ∘I sym (Fin-⊎-+ (C n k) (C n (suc k)))

module v! where

  C : ℕ → ℕ → ℕ
  C n k = n ! / (k ! * (n ∸ k)!)

module v1 where

  C : ℕ → ℕ → ℕ
  C n 0 = 1
  C n (suc k) = (C n k * (n ∸ k)) / suc k

module v2 where

  C : ℕ → ℕ → ℕ
  C n       zero    = 1
  C zero    (suc k) = 0
  C (suc n) (suc k) = (C n k * suc n) / suc k

{- Σ_{0≤k<n} (C n k) ≡ 2ⁿ -}

Σ𝟙F↔F : ∀ (F : 𝟙 → ★) → Σ 𝟙 F ↔ F _
Σ𝟙F↔F F = inverses proj₂ ,_ (λ _ → ≡.refl) (λ _ → ≡.refl)

Bits = Vec 𝟚
Bits1↔𝟚 : Bits 1 ↔ 𝟚
Bits1↔𝟚 = {!!}

open v0
foo : ∀ n → Σ (Fin (suc n)) (D (suc n) ∘ Fin▹ℕ) ↔ Bits (suc n)
foo zero = ((sym Bits1↔𝟚 ∘I {!!}) ∘I Σ𝟙F↔F _) ∘I first-iso Fin1↔𝟙
foo (suc n) = {!!}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
module eq-reasoning {A : Set} where

  open import eq

  infix  1 begin_
  infixr 2 _≡⟨⟩_ _≡⟨_⟩_
  infix  3 _∎

  begin_ : ∀ {x y : A}
    → x ≡ y
      -----
    → x ≡ y
  begin x≡y  =  x≡y

  _≡⟨⟩_ : ∀ (x : A) {y : A}
    → x ≡ y
      -----
    → x ≡ y
  x ≡⟨⟩ x≡y  =  x≡y

  _≡⟨_⟩_ : ∀ (x : A) {y z : A}
    → x ≡ y
    → y ≡ z
      -----
    → x ≡ z
  x ≡⟨ x≡y ⟩ y≡z  =  trans x≡y y≡z

  _∎ : ∀ (x : A)
      -----
    → x ≡ x
  x ∎  =  refl

max_stars_repo_name: JimFixGroupResearch/imper-ial

max_issues_repo_name: JimFixGroupResearch/imper-ial

max_forks_repo_name: JimFixGroupResearch/imper-ial


text:
{-# OPTIONS --without-K #-}
module Util.HoTT.Univalence.Statement where

open import Util.HoTT.Equiv
open import Util.Prelude

Univalence : ∀ α → Set (lsuc α)
Univalence α = {A B : Set α} → IsEquiv (≡→≃ {A = A} {B = B})

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
module Luau.Heap where

open import Agda.Builtin.Equality using (_≡_)
open import FFI.Data.Maybe using (Maybe; just)
open import FFI.Data.Vector using (Vector; length; snoc; empty)
open import Luau.Addr using (Addr)
open import Luau.Var using (Var)
open import Luau.Syntax using (Block; Expr; nil; addr; function⟨_⟩_end)

data HeapValue : Set where
  function_⟨_⟩_end : Var → Var → Block → HeapValue

Heap = Vector HeapValue

data _≡_⊕_↦_ : Heap → Heap → Addr → HeapValue → Set where

  defn : ∀ {H val} →

    -----------------------------------
    (snoc H val) ≡ H ⊕ (length H) ↦ val

lookup : Heap → Addr → Maybe HeapValue
lookup = FFI.Data.Vector.lookup

emp : Heap
emp = empty

data AllocResult (H : Heap) (V : HeapValue) : Set where
  ok : ∀ a H′ → (H′ ≡ H ⊕ a ↦ V) → AllocResult H V

alloc : ∀ H V → AllocResult H V
alloc H V = ok (length H) (snoc H V) defn

next : Heap → Addr
next = length

allocated : Heap → HeapValue → Heap
allocated = snoc

-- next-emp : (length empty ≡ 0)
next-emp = FFI.Data.Vector.length-empty

-- lookup-next : ∀ V H → (lookup (allocated H V) (next H) ≡ just V)
lookup-next = FFI.Data.Vector.lookup-snoc

-- lookup-next-emp : ∀ V → (lookup (allocated emp V) 0 ≡ just V)
lookup-next-emp = FFI.Data.Vector.lookup-snoc-empty

max_stars_repo_name: FreakingBarbarians/luau

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


text:
open import Oscar.Prelude
open import Oscar.Data.𝟘

module Oscar.Data.ProperlyExtensionNothing where

module _
  {𝔵} {𝔛 : Ø 𝔵}
  {𝔬} {𝔒 : 𝔛 → Ø 𝔬}
  {ℓ}
  {ℓ̇} {_↦_ : ∀ {x} → 𝔒 x → 𝔒 x → Ø ℓ̇}
  where

  record ProperlyExtensionNothing (P : ExtensionṖroperty ℓ 𝔒 _↦_) : Ø 𝔵 ∙̂ 𝔬 ∙̂ ℓ where
    constructor ∁
    field
      π₀ : ∀ {n} {f : 𝔒 n} → π₀ (π₀ P) f → 𝟘

open ProperlyExtensionNothing public


text:
------------------------------------------------------------------------------
-- Totality properties respect to OrdTree
------------------------------------------------------------------------------

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

module FOTC.Program.SortList.Properties.Totality.OrdTreeI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Data.Bool
open import FOTC.Data.Bool.PropertiesI
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesI
open import FOTC.Data.Nat.List.Type
open import FOTC.Data.Nat.Type
open import FOTC.Program.SortList.SortList
open import FOTC.Program.SortList.Properties.Totality.BoolI
open import FOTC.Program.SortList.Properties.Totality.TreeI

------------------------------------------------------------------------------
-- Subtrees

-- If (node t₁ i t₂) is ordered then t₁ is ordered.
leftSubTree-OrdTree : ∀ {t₁ i t₂} → Tree t₁ → N i → Tree t₂ →
                      OrdTree (node t₁ i t₂) → OrdTree t₁
leftSubTree-OrdTree {t₁} {i} {t₂} Tt₁ Ni Tt₂ TOnode =
  ordTree t₁
    ≡⟨ &&-list₂-t₁ (ordTree-Bool Tt₁)
                   (&&-Bool (ordTree-Bool Tt₂)
                            (&&-Bool (le-TreeItem-Bool Tt₁ Ni)
                                     (le-ItemTree-Bool Ni Tt₂)))
                   (trans (sym (ordTree-node t₁ i t₂)) TOnode)
    ⟩
  true ∎

-- If (node t₁ i t₂) is ordered then t₂ is ordered.
rightSubTree-OrdTree : ∀ {t₁ i t₂} → Tree t₁ → N i → Tree t₂ →
                       OrdTree (node t₁ i t₂) → OrdTree t₂
rightSubTree-OrdTree {t₁} {i} {t₂} Tt₁ Ni Tt₂ TOnode =
  ordTree t₂
    ≡⟨ &&-list₂-t₁
       (ordTree-Bool Tt₂)
         (&&-Bool (le-TreeItem-Bool Tt₁ Ni)
                  (le-ItemTree-Bool Ni Tt₂))
         (&&-list₂-t₂ (ordTree-Bool Tt₁)
                      (&&-Bool (ordTree-Bool Tt₂)
                               (&&-Bool (le-TreeItem-Bool Tt₁ Ni)
                                        (le-ItemTree-Bool Ni Tt₂)))
                      (trans (sym (ordTree-node t₁ i t₂)) TOnode))
    ⟩
  true ∎

------------------------------------------------------------------------------
-- Helper functions

toTree-OrdTree-helper₁ : ∀ {i₁ i₂ t} → N i₁ → N i₂ → i₁ > i₂ →
                         Tree t →
                         ≤-TreeItem t i₁ →
                         ≤-TreeItem (toTree · i₂ · t) i₁
toTree-OrdTree-helper₁ {i₁} {i₂} .{nil} Ni₁ Ni₂ i₁>i₂ tnil _ =
  le-TreeItem (toTree · i₂ · nil) i₁
    ≡⟨ subst (λ t → le-TreeItem (toTree · i₂ · nil) i₁ ≡ le-TreeItem t i₁)
             (toTree-nil i₂)
             refl
    ⟩
  le-TreeItem (tip i₂) i₁
    ≡⟨ le-TreeItem-tip i₂ i₁ ⟩
  le i₂ i₁
    ≡⟨ x<y→x≤y Ni₂ Ni₁ i₁>i₂ ⟩
  true ∎

toTree-OrdTree-helper₁ {i₁} {i₂} Ni₁ Ni₂ i₁>i₂ (ttip {j} Nj) t≤i₁ =
  case prf₁ prf₂ (x>y∨x≤y Nj Ni₂)
  where
  prf₁ : j > i₂ → ≤-TreeItem (toTree · i₂ · tip j) i₁
  prf₁ j>i₂ =
    le-TreeItem (toTree · i₂ · tip j) i₁
      ≡⟨ subst (λ t → le-TreeItem (toTree · i₂ · tip j) i₁ ≡
                      le-TreeItem t i₁)
               (toTree-tip i₂ j)
               refl
      ⟩
    le-TreeItem (if (le j i₂)
                   then (node (tip j) i₂ (tip i₂))
                   else (node (tip i₂) j (tip j))) i₁
      ≡⟨ subst (λ t → le-TreeItem
                      (if (le j i₂)
                         then (node (tip j) i₂ (tip i₂))
                         else (node (tip i₂) j (tip j))) i₁ ≡
                      le-TreeItem (if t
                                     then (node (tip j) i₂ (tip i₂))
                                     else (node (tip i₂) j (tip j))) i₁)
               (x>y→x≰y Nj Ni₂ j>i₂)
               refl
      ⟩
    le-TreeItem (if false
                   then (node (tip j) i₂ (tip i₂))
                   else (node (tip i₂) j (tip j))) i₁
      ≡⟨ subst (λ t → le-TreeItem (if false
                                     then (node (tip j) i₂ (tip i₂))
                                     else (node (tip i₂) j (tip j))) i₁ ≡
                      le-TreeItem t i₁)
               (if-false (node (tip i₂) j (tip j)))
               refl
      ⟩
    le-TreeItem (node (tip i₂) j (tip j)) i₁
      ≡⟨ le-TreeItem-node (tip i₂) j (tip j) i₁ ⟩
    le-TreeItem (tip i₂) i₁ && le-TreeItem (tip j) i₁
      ≡⟨ subst (λ t → le-TreeItem (tip i₂) i₁ && le-TreeItem (tip j) i₁ ≡
                      t && le-TreeItem (tip j) i₁)
               (le-TreeItem-tip i₂ i₁)
               refl
      ⟩
    le i₂ i₁ && le-TreeItem (tip j) i₁
       ≡⟨ subst (λ t → le i₂ i₁ && le-TreeItem (tip j) i₁ ≡
                       t && le-TreeItem (tip j) i₁)
                (x<y→x≤y Ni₂ Ni₁ i₁>i₂)
                refl
       ⟩
    true && le-TreeItem (tip j) i₁
      ≡⟨ subst (λ t → true && le-TreeItem (tip j) i₁ ≡ true && t)
               (le-TreeItem-tip j i₁)
               refl
      ⟩
    true && le j i₁
      ≡⟨ subst (λ t → true && le j i₁ ≡ true && t)
               -- j ≤ i₁ because by hypothesis we have (tip j) ≤ i₁.
               (trans (sym (le-TreeItem-tip j i₁)) t≤i₁)
               refl
      ⟩
    true && true
      ≡⟨ t&&x≡x true ⟩
    true ∎

  prf₂ : j ≤ i₂ → ≤-TreeItem (toTree · i₂ · tip j) i₁
  prf₂ j≤i₂ =
    le-TreeItem (toTree · i₂ · tip j) i₁
      ≡⟨ subst (λ t → le-TreeItem (toTree · i₂ · tip j) i₁ ≡
                      le-TreeItem t i₁)
               (toTree-tip i₂ j)
               refl
      ⟩
    le-TreeItem (if (le j i₂)
                   then (node (tip j) i₂ (tip i₂))
                   else (node (tip i₂) j (tip j))) i₁
      ≡⟨ subst (λ t → le-TreeItem
                      (if (le j i₂)
                         then (node (tip j) i₂ (tip i₂))
                         else (node (tip i₂) j (tip j))) i₁ ≡
                      le-TreeItem (if t
                                     then (node (tip j) i₂ (tip i₂))
                                     else (node (tip i₂) j (tip j))) i₁)
               j≤i₂
               refl
      ⟩
    le-TreeItem (if true
                   then (node (tip j) i₂ (tip i₂))
                   else (node (tip i₂) j (tip j))) i₁
      ≡⟨ subst (λ t → le-TreeItem (if true
                                     then (node (tip j) i₂ (tip i₂))
                                     else (node (tip i₂) j (tip j))) i₁ ≡
                      le-TreeItem t i₁)
               (if-true (node (tip j) i₂ (tip i₂)))
               refl
         ⟩
    le-TreeItem (node (tip j) i₂ (tip i₂)) i₁
      ≡⟨ le-TreeItem-node (tip j) i₂ (tip i₂) i₁ ⟩
    le-TreeItem (tip j) i₁ && le-TreeItem (tip i₂) i₁
      ≡⟨ subst (λ t → le-TreeItem (tip j) i₁ && le-TreeItem (tip i₂) i₁ ≡
                      t && le-TreeItem (tip i₂) i₁)
               (le-TreeItem-tip j i₁)
               refl
      ⟩
    le j i₁ && le-TreeItem (tip i₂) i₁
      ≡⟨ subst (λ t → le j i₁ && le-TreeItem (tip i₂) i₁ ≡
                      t && le-TreeItem (tip i₂) i₁)
               -- j ≤ i₁ because by hypothesis we have (tip j) ≤ i₁.
               (trans (sym (le-TreeItem-tip j i₁)) t≤i₁)
               refl
      ⟩
    true && le-TreeItem (tip i₂) i₁
      ≡⟨ subst (λ t → true && le-TreeItem (tip i₂) i₁ ≡ true && t)
               (le-TreeItem-tip i₂ i₁)
               refl
      ⟩
    true && le i₂ i₁
      ≡⟨ subst (λ t → true && le i₂ i₁ ≡ true && t)
               (x<y→x≤y Ni₂ Ni₁ i₁>i₂)
               refl
      ⟩
    true && true
      ≡⟨ t&&x≡x true ⟩
    true ∎

toTree-OrdTree-helper₁ {i₁} {i₂} Ni₁ Ni₂ i₁>i₂
                       (tnode {t₁} {j} {t₂} Tt₁ Nj Tt₂) t≤i₁ =
  case prf₁ prf₂ (x>y∨x≤y Nj Ni₂)
  where
  prf₁ : j > i₂ → ≤-TreeItem (toTree · i₂ · node t₁ j t₂) i₁
  prf₁ j>i₂ =
    le-TreeItem (toTree · i₂ · node t₁ j t₂) i₁
      ≡⟨ subst (λ t → le-TreeItem (toTree · i₂ · node t₁ j t₂) i₁ ≡
                      le-TreeItem t i₁)
               (toTree-node i₂ t₁ j t₂)
               refl
      ⟩
    le-TreeItem (if (le j i₂)
                   then (node t₁ j (toTree · i₂ · t₂))
                   else (node (toTree · i₂ · t₁) j t₂)) i₁
      ≡⟨ subst (λ t → le-TreeItem
                        (if (le j i₂)
                           then (node t₁ j (toTree · i₂ · t₂))
                           else (node (toTree · i₂ · t₁) j t₂)) i₁ ≡
                      le-TreeItem
                        (if t
                           then (node t₁ j (toTree · i₂ · t₂))
                           else (node (toTree · i₂ · t₁) j t₂)) i₁)
               (x>y→x≰y Nj Ni₂ j>i₂)
               refl
      ⟩
    le-TreeItem (if false
                   then (node t₁ j (toTree · i₂ · t₂))
                   else (node (toTree · i₂ · t₁) j t₂)) i₁
      ≡⟨ subst (λ t → le-TreeItem (if false
                                     then (node t₁ j (toTree · i₂ · t₂))
                                     else (node (toTree · i₂ · t₁) j t₂)) i₁ ≡
                      le-TreeItem t i₁)
               (if-false (node (toTree · i₂ · t₁) j t₂))
               refl
      ⟩
    le-TreeItem (node (toTree · i₂ · t₁) j t₂) i₁
      ≡⟨ le-TreeItem-node (toTree · i₂ · t₁) j t₂ i₁ ⟩
    le-TreeItem (toTree · i₂ · t₁) i₁ && le-TreeItem t₂ i₁
      ≡⟨ subst (λ t → le-TreeItem (toTree · i₂ · t₁) i₁ &&
                      le-TreeItem t₂ i₁                 ≡
                      t                                &&
                      le-TreeItem t₂ i₁)
               -- Inductive hypothesis.
               (toTree-OrdTree-helper₁ Ni₁ Ni₂ i₁>i₂ Tt₁
                 (&&-list₂-t₁ (le-TreeItem-Bool Tt₁ Ni₁)
                              (le-TreeItem-Bool Tt₂ Ni₁)
                              (trans (sym (le-TreeItem-node t₁ j t₂ i₁)) t≤i₁)))
               refl
      ⟩
    true && le-TreeItem t₂ i₁
      ≡⟨ subst (λ t → true && le-TreeItem t₂ i₁ ≡ true && t)
               -- t₂ ≤ i₁ because by hypothesis we have (node t₁ j t₂) ≤ i₁.
               (&&-list₂-t₂ (le-TreeItem-Bool Tt₁ Ni₁)
                            (le-TreeItem-Bool Tt₂ Ni₁)
                            (trans (sym (le-TreeItem-node t₁ j t₂ i₁)) t≤i₁))
               refl
      ⟩
    true && true
      ≡⟨ t&&x≡x true ⟩
    true ∎

  prf₂ : j ≤ i₂ → ≤-TreeItem (toTree · i₂ · node t₁ j t₂) i₁
  prf₂ j≤i₂ =
    le-TreeItem (toTree · i₂ · node t₁ j t₂) i₁
      ≡⟨ subst (λ t → le-TreeItem (toTree · i₂ · node t₁ j t₂) i₁ ≡
                      le-TreeItem t i₁)
               (toTree-node i₂ t₁ j t₂)
               refl
      ⟩
    le-TreeItem (if (le j i₂)
                   then (node t₁ j (toTree · i₂ · t₂))
                   else (node (toTree · i₂ · t₁) j t₂)) i₁
      ≡⟨ subst (λ t → le-TreeItem
                        (if (le j i₂)
                           then (node t₁ j (toTree · i₂ · t₂))
                           else (node (toTree · i₂ · t₁) j t₂)) i₁ ≡
                      le-TreeItem
                        (if t
                           then (node t₁ j (toTree · i₂ · t₂))
                           else (node (toTree · i₂ · t₁) j t₂)) i₁)
               (j≤i₂)
               refl
      ⟩
    le-TreeItem (if true
                   then (node t₁ j (toTree · i₂ · t₂))
                   else (node (toTree · i₂ · t₁) j t₂)) i₁
      ≡⟨ subst (λ t → le-TreeItem (if true
                                     then (node t₁ j (toTree · i₂ · t₂))
                                     else (node (toTree · i₂ · t₁) j t₂)) i₁ ≡
                      le-TreeItem t i₁)
               (if-true (node t₁ j (toTree · i₂ · t₂)))
               refl
      ⟩
    le-TreeItem (node t₁ j (toTree · i₂ · t₂)) i₁
      ≡⟨ le-TreeItem-node t₁ j (toTree · i₂ · t₂) i₁ ⟩
    le-TreeItem t₁ i₁ && le-TreeItem (toTree · i₂ · t₂) i₁
      ≡⟨ subst (λ t → le-TreeItem t₁ i₁ && le-TreeItem (toTree · i₂ · t₂) i₁ ≡
                      t &&  le-TreeItem (toTree · i₂ · t₂) i₁)
               -- t₁ ≤ i₁ because by hypothesis we have (node t₁ j t₂) ≤ i₁.
               (&&-list₂-t₁ (le-TreeItem-Bool Tt₁ Ni₁)
                            (le-TreeItem-Bool Tt₂ Ni₁)
                            (trans (sym (le-TreeItem-node t₁ j t₂ i₁)) t≤i₁))
               refl
      ⟩
    true && le-TreeItem (toTree · i₂ · t₂) i₁
      ≡⟨ subst (λ t → true && le-TreeItem (toTree · i₂ · t₂) i₁ ≡
                      true && t)
               -- Inductive hypothesis.
               (toTree-OrdTree-helper₁ Ni₁ Ni₂ i₁>i₂ Tt₂
                 (&&-list₂-t₂ (le-TreeItem-Bool Tt₁ Ni₁)
                              (le-TreeItem-Bool Tt₂ Ni₁)
                              (trans (sym (le-TreeItem-node t₁ j t₂ i₁)) t≤i₁)))
               refl
      ⟩
    true && true
      ≡⟨ t&&x≡x true ⟩
    true ∎

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

toTree-OrdTree-helper₂ : ∀ {i₁ i₂ t} → N i₁ → N i₂ → i₁ ≤ i₂ →
                         Tree t →
                         ≤-ItemTree i₁ t →
                         ≤-ItemTree i₁ (toTree · i₂ · t)
toTree-OrdTree-helper₂ {i₁} {i₂} .{nil} _ _ i₁≤i₂ tnil _ =
  le-ItemTree i₁ (toTree · i₂ · nil)
    ≡⟨ subst (λ t → le-ItemTree i₁ (toTree · i₂ · nil) ≡ le-ItemTree i₁ t)
             (toTree-nil i₂)
             refl
    ⟩
  le-ItemTree i₁ (tip i₂)
    ≡⟨ le-ItemTree-tip i₁ i₂ ⟩
  le i₁ i₂
    ≡⟨ i₁≤i₂ ⟩
  true ∎

toTree-OrdTree-helper₂ {i₁} {i₂} Ni₁ Ni₂ i₁≤i₂ (ttip {j} Nj) i₁≤t =
  case prf₁ prf₂ (x>y∨x≤y Nj Ni₂)
  where
  prf₁ : j > i₂ → ≤-ItemTree i₁ (toTree · i₂ · tip j)
  prf₁ j>i₂ =
    le-ItemTree i₁ (toTree · i₂ · tip j)
      ≡⟨ subst (λ t → le-ItemTree i₁ (toTree · i₂ · tip j) ≡
                      le-ItemTree i₁ t)
               (toTree-tip i₂ j)
               refl
      ⟩
    le-ItemTree i₁ (if (le j i₂)
                      then (node (tip j) i₂ (tip i₂))
                      else (node (tip i₂) j (tip j)))
      ≡⟨ subst (λ t → le-ItemTree i₁ (if (le j i₂)
                                        then (node (tip j) i₂ (tip i₂))
                                        else (node (tip i₂) j (tip j))) ≡
                      le-ItemTree i₁ (if t
                                        then (node (tip j) i₂ (tip i₂))
                                        else (node (tip i₂) j (tip j))))
             (x>y→x≰y Nj Ni₂ j>i₂)
             refl
       ⟩
    le-ItemTree i₁ (if false
                      then (node (tip j) i₂ (tip i₂))
                      else (node (tip i₂) j (tip j)))
    ≡⟨ subst (λ t → le-ItemTree i₁ (if false
                                      then (node (tip j) i₂ (tip i₂))
                                      else (node (tip i₂) j (tip j))) ≡
                    le-ItemTree i₁ t)
                (if-false (node (tip i₂) j (tip j)))
                refl
       ⟩
    le-ItemTree i₁ (node (tip i₂) j (tip j))
      ≡⟨ le-ItemTree-node i₁ (tip i₂) j (tip j) ⟩
    le-ItemTree i₁ (tip i₂) && le-ItemTree i₁ (tip j)
      ≡⟨ subst (λ t → le-ItemTree i₁ (tip i₂) && le-ItemTree i₁ (tip j) ≡
                      t && le-ItemTree i₁ (tip j))
               (le-ItemTree-tip i₁ i₂)
               refl
      ⟩
    le i₁ i₂ && le-ItemTree i₁ (tip j)
       ≡⟨ subst (λ t → le i₁ i₂ && le-ItemTree i₁ (tip j) ≡
                       t && le-ItemTree i₁ (tip j))
                i₁≤i₂
                refl
        ⟩
    true && le-ItemTree i₁ (tip j)
      ≡⟨ subst (λ t → true && le-ItemTree i₁ (tip j) ≡ true && t)
               (le-ItemTree-tip i₁ j)
               refl
      ⟩
    true && le i₁ j
      ≡⟨ subst (λ t → true && le i₁ j ≡ true && t)
               -- i₁ ≤ j because by hypothesis we have i₁ ≤ (tip j).
               (trans (sym (le-ItemTree-tip i₁ j)) i₁≤t)
               refl
      ⟩
    true && true
      ≡⟨ t&&x≡x true ⟩
    true ∎

  prf₂ : j ≤ i₂ → ≤-ItemTree i₁ (toTree · i₂ · tip j)
  prf₂ j≤i₂ =
    le-ItemTree i₁ (toTree · i₂ · tip j)
      ≡⟨ subst (λ t → le-ItemTree i₁ (toTree · i₂ · tip j) ≡
                      le-ItemTree i₁ t)
               (toTree-tip i₂ j)
               refl
      ⟩
    le-ItemTree i₁ (if (le j i₂)
                      then (node (tip j) i₂ (tip i₂))
                      else (node (tip i₂) j (tip j)))
      ≡⟨ subst (λ t → le-ItemTree i₁ (if (le j i₂)
                                        then (node (tip j) i₂ (tip i₂))
                                        else (node (tip i₂) j (tip j))) ≡
                      le-ItemTree i₁ (if t
                                        then (node (tip j) i₂ (tip i₂))
                                        else (node (tip i₂) j (tip j))))
               j≤i₂
               refl
        ⟩
    le-ItemTree i₁ (if true
                      then (node (tip j) i₂ (tip i₂))
                      else (node (tip i₂) j (tip j)))
      ≡⟨ subst (λ t → le-ItemTree i₁ (if true
                                        then (node (tip j) i₂ (tip i₂))
                                        else (node (tip i₂) j (tip j))) ≡
                      le-ItemTree i₁ t)
               (if-true (node (tip j) i₂ (tip i₂)))
               refl
      ⟩
    le-ItemTree i₁ (node (tip j) i₂ (tip i₂))
      ≡⟨ le-ItemTree-node i₁ (tip j) i₂ (tip i₂) ⟩
    le-ItemTree i₁ (tip j) && le-ItemTree i₁ (tip i₂)
      ≡⟨ subst (λ t → le-ItemTree i₁ (tip j) && le-ItemTree i₁ (tip i₂) ≡
                      t && le-ItemTree i₁ (tip i₂))
               (le-ItemTree-tip i₁ j)
               refl
      ⟩
    le i₁ j && le-ItemTree i₁ (tip i₂)
       ≡⟨ subst (λ t → le i₁ j && le-ItemTree i₁ (tip i₂) ≡
                       t && le-ItemTree i₁ (tip i₂))
          -- i₁ ≤ j because by hypothesis we have i₁ ≤ (tip j).
                (trans (sym (le-ItemTree-tip i₁ j)) i₁≤t)
                refl
       ⟩
    true && le-ItemTree i₁ (tip i₂)
      ≡⟨ subst (λ t → true && le-ItemTree i₁ (tip i₂) ≡ true && t)
               (le-ItemTree-tip i₁ i₂)
               refl
      ⟩
      true && le i₁ i₂
      ≡⟨ subst (λ t → true && le i₁ i₂ ≡ true && t)
               i₁≤i₂
               refl
      ⟩
    true && true
      ≡⟨ t&&x≡x true ⟩
    true ∎

toTree-OrdTree-helper₂ {i₁} {i₂} Ni₁ Ni₂ i₁≤i₂
                       (tnode {t₁} {j} {t₂} Tt₁ Nj Tt₂) i₁≤t =
  case prf₁ prf₂ (x>y∨x≤y Nj Ni₂)
  where
  prf₁ : j > i₂ → ≤-ItemTree i₁ (toTree · i₂ · node t₁ j t₂)
  prf₁ j>i₂ =
    le-ItemTree i₁ (toTree · i₂ · node t₁ j t₂)
      ≡⟨ subst (λ t → le-ItemTree i₁ (toTree · i₂ · node t₁ j t₂) ≡
                      le-ItemTree i₁ t)
               (toTree-node i₂ t₁ j t₂)
               refl
      ⟩
    le-ItemTree i₁ (if (le j i₂)
                      then (node t₁ j (toTree · i₂ · t₂))
                      else (node (toTree · i₂ · t₁) j t₂))
    ≡⟨ subst (λ t → le-ItemTree i₁ (if (le j i₂)
                                      then (node t₁ j (toTree · i₂ · t₂))
                                      else (node (toTree · i₂ · t₁) j t₂)) ≡
                    le-ItemTree i₁ (if t
                                      then (node t₁ j (toTree · i₂ · t₂))
                                      else (node (toTree · i₂ · t₁) j t₂)))
                (x>y→x≰y Nj Ni₂ j>i₂)
                refl
       ⟩
    le-ItemTree i₁ (if false
                      then (node t₁ j (toTree · i₂ · t₂))
                      else (node (toTree · i₂ · t₁) j t₂))
      ≡⟨ subst (λ t → le-ItemTree i₁ (if false
                                        then (node t₁ j (toTree · i₂ · t₂))
                                        else (node (toTree · i₂ · t₁) j t₂)) ≡
                      le-ItemTree i₁ t)
               (if-false (node (toTree · i₂ · t₁) j t₂))
               refl
      ⟩
    le-ItemTree i₁ (node (toTree · i₂ · t₁) j t₂)
      ≡⟨ le-ItemTree-node i₁ (toTree · i₂ · t₁) j t₂ ⟩
      le-ItemTree i₁ (toTree · i₂ · t₁) && le-ItemTree i₁ t₂
      ≡⟨ subst (λ t → le-ItemTree i₁ (toTree · i₂ · t₁) && le-ItemTree i₁ t₂ ≡
                      t && le-ItemTree i₁ t₂)
               -- Inductive hypothesis.
               (toTree-OrdTree-helper₂ Ni₁ Ni₂ i₁≤i₂ Tt₁
                 (&&-list₂-t₁ (le-ItemTree-Bool Ni₁ Tt₁)
                              (le-ItemTree-Bool Ni₁ Tt₂)
                              (trans (sym (le-ItemTree-node i₁ t₁ j t₂)) i₁≤t)))
               refl
      ⟩
    true && le-ItemTree i₁ t₂
      ≡⟨ subst (λ t → true && le-ItemTree i₁ t₂ ≡ true && t)
               -- i₁ ≤ t₂ because by hypothesis we have i₁ ≤ (node t₁ j t₂).
               (&&-list₂-t₂ (le-ItemTree-Bool Ni₁ Tt₁)
                            (le-ItemTree-Bool Ni₁ Tt₂)
                            (trans (sym (le-ItemTree-node i₁ t₁ j t₂)) i₁≤t))
               refl
      ⟩
    true && true
      ≡⟨ t&&x≡x true ⟩
    true ∎

  prf₂ : j ≤ i₂ → ≤-ItemTree i₁ (toTree · i₂ · node t₁ j t₂)
  prf₂ j≤i₂ =
    le-ItemTree i₁ (toTree · i₂ · node t₁ j t₂)
      ≡⟨ subst (λ t → le-ItemTree i₁ (toTree · i₂ · node t₁ j t₂) ≡
                      le-ItemTree i₁ t)
               (toTree-node i₂ t₁ j t₂)
               refl
      ⟩
    le-ItemTree i₁ (if (le j i₂)
                      then (node t₁ j (toTree · i₂ · t₂))
                      else (node (toTree · i₂ · t₁) j t₂))
    ≡⟨ subst (λ t → le-ItemTree i₁ (if (le j i₂)
                                      then (node t₁ j (toTree · i₂ · t₂))
                                      else (node (toTree · i₂ · t₁) j t₂)) ≡
                    le-ItemTree i₁ (if t
                                      then (node t₁ j (toTree · i₂ · t₂))
                                      else (node (toTree · i₂ · t₁) j t₂)))
                j≤i₂
                refl
       ⟩
    le-ItemTree i₁ (if true
                      then (node t₁ j (toTree · i₂ · t₂))
                      else (node (toTree · i₂ · t₁) j t₂))
      ≡⟨ subst (λ t → le-ItemTree i₁ (if true
                                        then (node t₁ j (toTree · i₂ · t₂))
                                        else (node (toTree · i₂ · t₁) j t₂)) ≡
                      le-ItemTree i₁ t)
               (if-true (node t₁ j (toTree · i₂ · t₂)))
               refl
      ⟩
    le-ItemTree i₁ (node t₁ j (toTree · i₂ · t₂))
      ≡⟨ le-ItemTree-node i₁ t₁ j (toTree · i₂ · t₂) ⟩
    le-ItemTree i₁ t₁ && le-ItemTree i₁ (toTree · i₂ · t₂)
      ≡⟨ subst (λ t → le-ItemTree i₁ t₁ && le-ItemTree i₁ (toTree · i₂ · t₂) ≡
                      t && le-ItemTree i₁ (toTree · i₂ · t₂))
               -- i₁ ≤ t₁ because by hypothesis we have i₁ ≤ (node t₁ j t₂).
               (&&-list₂-t₁ (le-ItemTree-Bool Ni₁ Tt₁)
                            (le-ItemTree-Bool Ni₁ Tt₂)
                            (trans (sym (le-ItemTree-node i₁ t₁ j t₂)) i₁≤t))
               refl
      ⟩
    true && le-ItemTree i₁ (toTree · i₂ · t₂)
      ≡⟨ subst (λ t → true && le-ItemTree i₁ (toTree · i₂ · t₂) ≡ true && t)
               -- Inductive hypothesis.
               (toTree-OrdTree-helper₂ Ni₁ Ni₂ i₁≤i₂ Tt₂
                 (&&-list₂-t₂ (le-ItemTree-Bool Ni₁ Tt₁)
                              (le-ItemTree-Bool Ni₁ Tt₂)
                              (trans (sym (le-ItemTree-node i₁ t₁ j t₂)) i₁≤t)))
               refl
      ⟩
    true && true
      ≡⟨ t&&x≡x true ⟩
    true ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module UniverseCollapse
    (down : Set₁ -> Set)
    (up : Set → Set₁)
    (iso : ∀ {A} → down (up A) → A)
    (osi : ∀ {A} → up (down A) → A) where

anything : (A : Set) → A
anything = {!!}

max_stars_repo_name: danr/agder

max_issues_repo_name: danr/agder

max_forks_repo_name: danr/agder


text:
module ctxt where

open import lib
open import cedille-types
open import ctxt-types public
open import subst
open import general-util
open import syntax-util

new-sym-info-trie : trie sym-info
new-sym-info-trie = trie-insert empty-trie compileFail-qual ((term-decl compileFailType) , "missing" , "missing")

new-qualif : qualif
new-qualif = trie-insert empty-trie compileFail (compileFail-qual , ArgsNil)

qualif-nonempty : qualif → 𝔹
qualif-nonempty q = trie-nonempty (trie-remove q compileFail)

new-ctxt : (filename modname : string) → ctxt
new-ctxt fn mn = mk-ctxt (fn , mn , ParamsNil , new-qualif) (empty-trie , empty-trie , empty-trie , empty-trie , 0 , []) new-sym-info-trie empty-trie empty-trie

empty-ctxt : ctxt
empty-ctxt = new-ctxt "" ""

ctxt-get-info : var → ctxt → maybe sym-info
ctxt-get-info v (mk-ctxt _ _ i _ _) = trie-lookup i v

ctxt-set-qualif : ctxt → qualif → ctxt
ctxt-set-qualif (mk-ctxt (f , m , p , q') syms i sym-occurrences d) q
  = mk-ctxt (f , m , p , q) syms i sym-occurrences d

ctxt-get-qualif : ctxt → qualif
ctxt-get-qualif (mk-ctxt (_ , _ , _ , q) _ _ _ _) = q

ctxt-get-qi : ctxt → var → maybe qualif-info
ctxt-get-qi Γ = trie-lookup (ctxt-get-qualif Γ)

ctxt-qualif-args-length : ctxt → maybeErased → var → maybe ℕ
ctxt-qualif-args-length Γ me v =
  ctxt-get-qi Γ v ≫=maybe λ qv →
  just (me-args-length me (snd qv))

qi-var-if : maybe qualif-info → var → var
qi-var-if (just (v , _)) _ = v
qi-var-if nothing v = v

ctxt-restore-info : ctxt → var → maybe qualif-info → maybe sym-info → ctxt
ctxt-restore-info (mk-ctxt (fn , mn , ps , q) syms i symb-occs d) v qi si =
  mk-ctxt (fn , mn , ps , f qi v q) syms (f si (qi-var-if qi v) (trie-remove i (qi-var-if (trie-lookup q v) v))) symb-occs d
  where
    f : ∀{A : Set} → maybe A → string → trie A → trie A
    f (just a) s t = trie-insert t s a
    f nothing s t = trie-remove t s

ctxt-restore-info* : ctxt → 𝕃 (string × maybe qualif-info × maybe sym-info) → ctxt
ctxt-restore-info* Γ [] = Γ
ctxt-restore-info* Γ ((v , qi , m) :: ms) = ctxt-restore-info* (ctxt-restore-info Γ v qi m) ms

def-params : defScope → params → defParams
def-params tt ps = nothing
def-params ff ps = just ps

-- TODO add renamectxt to avoid capture bugs?
inst-type : ctxt → params → args → type → type
inst-type Γ ps as T with mk-inst ps as
...| σ , ps' = abs-expand-type (substs-params Γ σ ps') (substs Γ σ T)

inst-kind : ctxt → params → args → kind → kind
inst-kind Γ ps as k with mk-inst ps as
...| σ , ps' = abs-expand-kind (substs-params Γ σ ps') (substs Γ σ k)

qualif-x : ∀ {ℓ} {X : Set ℓ} → (ctxt → qualif → X) → ctxt → X
qualif-x f Γ = f Γ (ctxt-get-qualif Γ)

qualif-term = qualif-x $ substs {TERM}
qualif-type = qualif-x $ substs {TYPE}
qualif-kind = qualif-x $ substs {KIND}
qualif-liftingType = qualif-x $ substs {LIFTINGTYPE}
qualif-tk = qualif-x $ substs {TK}
qualif-params = qualif-x substs-params
qualif-args = qualif-x substs-args

erased-margs : ctxt → stringset
erased-margs = stringset-insert* empty-stringset ∘ (erased-params ∘ ctxt-get-current-params)

ctxt-term-decl : posinfo → var → type → ctxt → ctxt
ctxt-term-decl p v t Γ@(mk-ctxt (fn , mn , ps , q) syms i symb-occs d) =
  mk-ctxt (fn , mn , ps , (qualif-insert-params q v' v ParamsNil))
  syms
  (trie-insert i v' ((term-decl (qualif-type Γ t)) , fn , p))
  symb-occs
  d
  where v' = p % v

ctxt-type-decl : posinfo → var → kind → ctxt → ctxt
ctxt-type-decl p v k Γ@(mk-ctxt (fn , mn , ps , q) syms i symb-occs d) =
  mk-ctxt (fn , mn , ps , (qualif-insert-params q v' v ParamsNil))
  syms
  (trie-insert i v' (type-decl (qualif-kind Γ k) , fn , p))
  symb-occs
  d
  where v' = p % v

ctxt-tk-decl : posinfo → var → tk → ctxt → ctxt
ctxt-tk-decl p x (Tkt t) Γ = ctxt-term-decl p x t Γ
ctxt-tk-decl p x (Tkk k) Γ = ctxt-type-decl p x k Γ

-- TODO not sure how this and renaming interacts with module scope
ctxt-var-decl-if : var → ctxt → ctxt
ctxt-var-decl-if v Γ with Γ
... | mk-ctxt (fn , mn , ps , q) syms i symb-occs d with trie-lookup i v
... | just (rename-def _ , _) = Γ
... | just (var-decl , _) = Γ
... | _ = mk-ctxt (fn , mn , ps , (trie-insert q v (v , ArgsNil))) syms
  (trie-insert i v (var-decl , "missing" , "missing"))
  symb-occs
  d

ctxt-rename-rep : ctxt → var → var
ctxt-rename-rep (mk-ctxt m syms i _ _) v with trie-lookup i v
...                                           | just (rename-def v' , _) = v'
...                                           | _ = v

-- we assume that only the left variable might have been renamed
ctxt-eq-rep : ctxt → var → var → 𝔹
ctxt-eq-rep Γ x y = (ctxt-rename-rep Γ x) =string y

{- add a renaming mapping the first variable to the second, unless they are equal.
   Notice that adding a renaming for v will overwrite any other declarations for v. -}

ctxt-rename : var → var → ctxt → ctxt
ctxt-rename v v' Γ @ (mk-ctxt (fn , mn , ps , q) syms i symb-occs d) =
  (mk-ctxt (fn , mn , ps , qualif-insert-params q v' v ps) syms
  (trie-insert i v (rename-def v' , "missing" , "missing"))
  symb-occs
  d)

----------------------------------------------------------------------
-- lookup functions
----------------------------------------------------------------------

-- lookup mod params from filename
lookup-mod-params : ctxt → var → maybe params
lookup-mod-params (mk-ctxt _ (syms , _ , mn-ps , id) _ _ _) fn =
  trie-lookup syms fn ≫=maybe λ { (mn , _) →
  trie-lookup mn-ps mn }

-- look for a defined kind for the given var, which is assumed to be a type,
-- then instantiate its parameters
qual-lookup : ctxt → var → maybe (args × sym-info)
qual-lookup Γ@(mk-ctxt (_ , _ , _ , q) _ i _ _) v =
  trie-lookup q v ≫=maybe λ qv →
  trie-lookup i (fst qv) ≫=maybe λ si →
  just (snd qv , si)

env-lookup : ctxt → var → maybe sym-info
env-lookup Γ@(mk-ctxt (_ , _ , _ , _) _ i _ _) v =
  trie-lookup i v

-- look for a declared kind for the given var, which is assumed to be a type,
-- otherwise look for a qualified defined kind
ctxt-lookup-type-var : ctxt → var → maybe kind
ctxt-lookup-type-var Γ v with qual-lookup Γ v
... | just (as , type-decl k , _) = just k
... | just (as , type-def (just ps) _ T k , _) = just (inst-kind Γ ps as k)
... | just (as , type-def nothing _ T k , _) = just k
... | just (as , datatype-def _ k     , _) = just k
... | _ = nothing

-- remove ?
-- add-param-type : params → type → type
-- add-param-type (ParamsCons (Decl pi pix e x tk _) ps) ty  = Abs pi e pix x tk (add-param-type ps ty)
-- add-param-type ParamsNil                              ty  = ty

ctxt-lookup-term-var : ctxt → var → maybe type
ctxt-lookup-term-var Γ v with qual-lookup Γ v
... | just (as , term-decl T , _) = just T
... | just (as , term-def (just ps) _ t T , _) = just $ inst-type Γ ps as T
... | just (as , term-def nothing _ t T , _) = just T
... | just (as , const-def T            , _) = just T
... | _ = nothing

ctxt-lookup-tk-var : ctxt → var → maybe tk
ctxt-lookup-tk-var Γ v with qual-lookup Γ v
... | just (as , term-decl T , _) = just $ Tkt T
... | just (as , type-decl k , _) = just $ Tkk k
... | just (as , term-def (just ps) _ t T , _) = just $ Tkt $ inst-type Γ ps as T
... | just (as , type-def (just ps) _ T k , _) = just $ Tkk $ inst-kind Γ ps as k
... | just (as , term-def nothing _ t T , _) = just $ Tkt T
... | just (as , type-def nothing _ T k , _) = just $ Tkk k
... | just (as , datatype-def _ k     , _) = just $ Tkk k
... | _ = nothing

ctxt-lookup-term-var-def : ctxt → var → maybe term
ctxt-lookup-term-var-def Γ v with env-lookup Γ v
... | just (term-def nothing OpacTrans t _ , _) = just t
... | just (term-udef nothing OpacTrans t , _) = just t
... | just (term-def (just ps) OpacTrans t _ , _) = just $ lam-expand-term ps t
... | just (term-udef (just ps) OpacTrans t , _) = just $ lam-expand-term ps t
... | _ = nothing

ctxt-lookup-type-var-def : ctxt → var → maybe type
ctxt-lookup-type-var-def Γ v with env-lookup Γ v
... | just (type-def nothing OpacTrans T _ , _) = just T
... | just (type-def (just ps) OpacTrans T _ , _) = just $ lam-expand-type ps T
... | _ = nothing

ctxt-lookup-kind-var-def : ctxt → var → maybe (params × kind)
ctxt-lookup-kind-var-def Γ x with env-lookup Γ x
... | just (kind-def ps k , _) = just (ps , k)
... | _ = nothing

ctxt-lookup-kind-var-def-args : ctxt → var → maybe (params × args)
ctxt-lookup-kind-var-def-args Γ@(mk-ctxt (_ , _ , _ , q) _ i _ _) v with trie-lookup q v
... | just (v' , as) = ctxt-lookup-kind-var-def Γ v' ≫=maybe λ { (ps , k) → just (ps , as) }
... | _ = nothing

ctxt-lookup-occurrences : ctxt → var → 𝕃 (var × posinfo × string)
ctxt-lookup-occurrences (mk-ctxt _ _ _ symb-occs _) symbol with trie-lookup symb-occs symbol
... | just l = l
... | nothing = []

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

ctxt-var-location : ctxt → var → location
ctxt-var-location (mk-ctxt _ _ i _ _) x with trie-lookup i x
... | just (_ , l) = l
... | nothing = "missing" , "missing"

ctxt-clarify-def : ctxt → var → maybe (sym-info × ctxt)
ctxt-clarify-def Γ@(mk-ctxt mod@(_ , _ , _ , q) syms i sym-occurrences d) x
  = trie-lookup i x ≫=maybe λ { (ci , l) →
    clarified x ci l }
  where
    ctxt' : var → ctxt-info → location → ctxt
    ctxt' v ci l = mk-ctxt mod syms (trie-insert i v (ci , l)) sym-occurrences d

    clarified : var → ctxt-info → location → maybe (sym-info × ctxt)
    clarified v ci@(term-def ps _ t T) l = just ((ci , l) , (ctxt' v (term-def ps OpacTrans t T) l))
    clarified v ci@(term-udef ps _ t) l = just ((ci , l) , (ctxt' v (term-udef ps OpacTrans t) l))
    clarified v ci@(type-def ps _ T k) l = just ((ci , l) , (ctxt' v (type-def ps OpacTrans T k) l))
    clarified _ _ _ = nothing

ctxt-set-sym-info : ctxt → var → sym-info → ctxt
ctxt-set-sym-info (mk-ctxt mod syms i sym-occurrences d) x si =
  mk-ctxt mod syms (trie-insert i x si) sym-occurrences d

ctxt-restore-clarified-def : ctxt → var → sym-info → ctxt
ctxt-restore-clarified-def = ctxt-set-sym-info

ctxt-set-current-file : ctxt → string → string → ctxt
ctxt-set-current-file (mk-ctxt _ syms i symb-occs d) fn mn = mk-ctxt (fn , mn , ParamsNil , new-qualif) syms i symb-occs d

ctxt-set-current-mod : ctxt → mod-info → ctxt
ctxt-set-current-mod (mk-ctxt _ syms i symb-occs d) m = mk-ctxt m syms i symb-occs d

ctxt-add-current-params : ctxt → ctxt
ctxt-add-current-params Γ@(mk-ctxt m@(fn , mn , ps , _) (syms , mn-fn , mn-ps , ids) i symb-occs d) =
  mk-ctxt m (trie-insert syms fn (mn , []) , mn-fn , trie-insert mn-ps mn ps , ids) i symb-occs d

ctxt-clear-symbol : ctxt → string → ctxt
ctxt-clear-symbol Γ @ (mk-ctxt (fn , mn , pms , q) (syms , mn-fn) i symb-occs d) x =
  mk-ctxt (fn , mn , pms , (trie-remove q x)) (trie-map (λ ss → fst ss , remove _=string_ x (snd ss)) syms , mn-fn) (trie-remove i (qualif-var Γ x)) symb-occs d

ctxt-clear-symbols : ctxt → 𝕃 string → ctxt
ctxt-clear-symbols Γ [] = Γ
ctxt-clear-symbols Γ (v :: vs) = ctxt-clear-symbols (ctxt-clear-symbol Γ v) vs

ctxt-clear-symbols-of-file : ctxt → (filename : string) → ctxt
ctxt-clear-symbols-of-file (mk-ctxt f (syms , mn-fn , mn-ps) i symb-occs d) fn =
  mk-ctxt f (trie-insert syms fn (fst p , []) , trie-insert mn-fn (fst p) fn , mn-ps)
    (hremove i (fst p) (snd p))
    symb-occs
    d
  where
  p = trie-lookup𝕃2 syms fn
  hremove : ∀ {A : Set} → trie A → var → 𝕃 string → trie A
  hremove i mn [] = i
  hremove i mn (x :: xs) = hremove (trie-remove i (mn # x)) mn xs

ctxt-add-current-id : ctxt → ctxt
ctxt-add-current-id (mk-ctxt mod (syms , mn-fn , mn-ps , fn-ids , id , id-fns) is os d) =
  mk-ctxt mod (syms , mn-fn , mn-ps , trie-insert fn-ids (fst mod) (suc id) , suc id , (fst mod) :: id-fns) is os d

ctxt-initiate-file : ctxt → (filename modname : string) → ctxt
ctxt-initiate-file Γ fn mn = ctxt-add-current-id (ctxt-set-current-file (ctxt-clear-symbols-of-file Γ fn) fn mn)

unqual : ctxt → var → string
unqual (mk-ctxt (_ , _ , _ , q) _ _ _  _) v =
  if qualif-nonempty q
  then unqual-local (unqual-all q v)
  else v

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
{-# OPTIONS --copatterns #-}
-- Andreas, 2013-11-05  Coverage checker needs clauses to reduce type!
-- {-# OPTIONS -v tc.cover:20 #-}

module Issue937a where

open import Common.Prelude
open import Common.Equality
open import Common.Product

T : (b : Bool) → Set
T true = Nat
T false = Bool → Nat

test : Σ Bool T
proj₁ test = false
proj₂ test true  = zero
proj₂ test false = suc zero -- Error: unreachable clause

module _ {_ : Set} where

  bla : Σ Bool T
  proj₁ bla = false
  proj₂ bla true  = zero
  proj₂ bla false = suc zero -- Error: unreachable clause

-- should coverage check

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Sized.StatefulCell where

open import Data.Product
open import Data.String.Base

open import SizedIO.Object
open import SizedIO.IOObject
open import SizedIO.ConsoleObject

open import SizedIO.Console hiding (main)

open import NativeIO

open import Size

--open import StateSizedIO.Base

data CellState#  : Set where
  empty full  : CellState#

data CellMethodEmpty A : Set where
    put : A → CellMethodEmpty A

data CellMethodFull A : Set where
    get : CellMethodFull A
    put : A → CellMethodFull A

CellMethod# : ∀{A} → CellState# → Set
CellMethod#{A} empty = CellMethodEmpty A
CellMethod#{A} full = CellMethodFull A

CellResultFull : ∀{A} → CellMethodFull A → Set
CellResultFull {A} get = A
CellResultFull (put _) = Unit

CellResultEmpty : ∀{A} → CellMethodEmpty A → Set
CellResultEmpty (put _) = Unit

CellResult# : ∀{A} → (s : CellState#) → CellMethod#{A} s → Set
CellResult#{A} empty = CellResultEmpty{A}
CellResult#{A} full = CellResultFull{A}

n# : ∀{A} → (s : CellState#) → (c : CellMethod#{A} s) → (CellResult# s c) → CellState#
n# empty (put x) unit = full
n# full get z = full
n# full (put x) unit = full

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

module Cubical.Data.SumFin.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_)
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Unit
open import Cubical.Data.Bool
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
import Cubical.Data.Fin as Fin
import Cubical.Data.Fin.LehmerCode as LehmerCode
open import Cubical.Data.SumFin.Base as SumFin
open import Cubical.Data.Sum
open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation as Prop

open import Cubical.Relation.Nullary

private
  variable
    ℓ : Level
    k : ℕ

SumFin→Fin : Fin k → Fin.Fin k
SumFin→Fin = SumFin.elim (λ {k} _ → Fin.Fin k) Fin.fzero Fin.fsuc

Fin→SumFin : Fin.Fin k → Fin k
Fin→SumFin = Fin.elim (λ {k} _ → Fin k) fzero fsuc

Fin→SumFin-fsuc : (fk : Fin.Fin k) → Fin→SumFin (Fin.fsuc fk) ≡ fsuc (Fin→SumFin fk)
Fin→SumFin-fsuc = Fin.elim-fsuc (λ {k} _ → Fin k) fzero fsuc

SumFin→Fin→SumFin : (fk : Fin k) → Fin→SumFin (SumFin→Fin fk) ≡ fk
SumFin→Fin→SumFin = SumFin.elim (λ fk → Fin→SumFin (SumFin→Fin fk) ≡ fk)
                                refl λ {k} {fk} eq →
  Fin→SumFin (Fin.fsuc (SumFin→Fin fk)) ≡⟨ Fin→SumFin-fsuc (SumFin→Fin fk) ⟩
  fsuc (Fin→SumFin (SumFin→Fin fk))     ≡⟨ cong fsuc eq ⟩
  fsuc fk                               ∎

Fin→SumFin→Fin : (fk : Fin.Fin k) → SumFin→Fin (Fin→SumFin fk) ≡ fk
Fin→SumFin→Fin = Fin.elim (λ fk → SumFin→Fin (Fin→SumFin fk) ≡ fk)
                          refl λ {k} {fk} eq →
  SumFin→Fin (Fin→SumFin (Fin.fsuc fk)) ≡⟨ cong SumFin→Fin (Fin→SumFin-fsuc fk) ⟩
  Fin.fsuc (SumFin→Fin (Fin→SumFin fk)) ≡⟨ cong Fin.fsuc eq ⟩
  Fin.fsuc fk                           ∎

SumFin≃Fin : ∀ k → Fin k ≃ Fin.Fin k
SumFin≃Fin _ =
  isoToEquiv (iso SumFin→Fin Fin→SumFin Fin→SumFin→Fin SumFin→Fin→SumFin)

SumFin≡Fin : ∀ k → Fin k ≡ Fin.Fin k
SumFin≡Fin k = ua (SumFin≃Fin k)

enum : (n : ℕ)(p : n < k) → Fin k
enum n p = Fin→SumFin (n , p)

enumElim : (P : Fin k → Type ℓ) → ((n : ℕ)(p : n < k) → P (enum _ p)) → (i : Fin k) → P i
enumElim P f i = subst P (SumFin→Fin→SumFin i) (f (SumFin→Fin i .fst) (SumFin→Fin i .snd))

-- Closure properties of SumFin under type constructors

SumFin⊎≃ : (m n : ℕ) → (Fin m ⊎ Fin n) ≃ (Fin (m + n))
SumFin⊎≃ 0 n = ⊎-swap-≃ ⋆ ⊎-⊥-≃
SumFin⊎≃ (suc m) n = ⊎-assoc-≃ ⋆ ⊎-equiv (idEquiv ⊤) (SumFin⊎≃ m n)

SumFinΣ≃ : (n : ℕ)(f : Fin n → ℕ) → (Σ (Fin n) (λ x → Fin (f x))) ≃ (Fin (totalSum f))
SumFinΣ≃ 0 f = ΣEmpty _
SumFinΣ≃ (suc n) f =
    Σ⊎≃
  ⋆ ⊎-equiv (ΣUnit (λ tt → Fin (f (inl tt)))) (SumFinΣ≃ n (λ x → f (inr x)))
  ⋆ SumFin⊎≃ (f (inl tt)) (totalSum (λ x → f (inr x)))

SumFin×≃ : (m n : ℕ) → (Fin m × Fin n) ≃ (Fin (m · n))
SumFin×≃ m n = SumFinΣ≃ m (λ _ → n) ⋆ pathToEquiv (λ i → Fin (totalSumConst {m = m} n i))

SumFinΠ≃ : (n : ℕ)(f : Fin n → ℕ) → ((x : Fin n) → Fin (f x)) ≃ (Fin (totalProd f))
SumFinΠ≃ 0 _ = isContr→≃Unit (isContrΠ⊥) ⋆ invEquiv (⊎-⊥-≃)
SumFinΠ≃ (suc n) f =
    Π⊎≃
  ⋆ Σ-cong-equiv (ΠUnit (λ tt → Fin (f (inl tt)))) (λ _ → SumFinΠ≃ n (λ x → f (inr x)))
  ⋆ SumFin×≃ (f (inl tt)) (totalProd (λ x → f (inr x)))

isNotZero : ℕ → ℕ
isNotZero 0 = 0
isNotZero (suc n) = 1

SumFin∥∥≃ : (n : ℕ) → ∥ Fin n ∥ ≃ Fin (isNotZero n)
SumFin∥∥≃ 0 = propTruncIdempotent≃ (isProp⊥)
SumFin∥∥≃ (suc n) =
    isContr→≃Unit (inhProp→isContr ∣ inl tt ∣ isPropPropTrunc)
  ⋆ isContr→≃Unit (isContrUnit) ⋆ invEquiv (⊎-⊥-≃)

ℕ→Bool : ℕ → Bool
ℕ→Bool 0 = false
ℕ→Bool (suc n) = true

SumFin∥∥DecProp : (n : ℕ) → ∥ Fin n ∥ ≃ Bool→Type (ℕ→Bool n)
SumFin∥∥DecProp 0 = uninhabEquiv (Prop.rec isProp⊥ ⊥.rec) ⊥.rec
SumFin∥∥DecProp (suc n) = isContr→≃Unit (inhProp→isContr ∣ inl tt ∣ isPropPropTrunc)

-- negation of SumFin

SumFin¬ : (n : ℕ) → (¬ Fin n) ≃ Bool→Type (isZero n)
SumFin¬ 0 = isContr→≃Unit isContr⊥→A
SumFin¬ (suc n) = uninhabEquiv (λ f → f fzero) ⊥.rec

-- SumFin 1 is equivalent to unit

Fin1≃Unit : Fin 1 ≃ Unit
Fin1≃Unit = ⊎-⊥-≃

isContrSumFin1 : isContr (Fin 1)
isContrSumFin1 = isOfHLevelRespectEquiv 0 (invEquiv Fin1≃Unit) isContrUnit

-- SumFin 2 is equivalent to Bool

SumFin2≃Bool : Fin 2 ≃ Bool
SumFin2≃Bool = ⊎-equiv (idEquiv _) ⊎-⊥-≃ ⋆ isoToEquiv Iso-⊤⊎⊤-Bool

-- decidable predicate over SumFin

SumFinℙ≃ : (n : ℕ) → (Fin n → Bool) ≃ Fin (2 ^ n)
SumFinℙ≃ 0 = isContr→≃Unit (isContrΠ⊥) ⋆ invEquiv (⊎-⊥-≃)
SumFinℙ≃ (suc n) =
    Π⊎≃
  ⋆ Σ-cong-equiv (UnitToType≃ Bool ⋆ invEquiv SumFin2≃Bool) (λ _ → SumFinℙ≃ n)
  ⋆ SumFin×≃ 2 (2 ^ n)

-- decidable subsets of SumFin

Bool→ℕ : Bool → ℕ
Bool→ℕ true = 1
Bool→ℕ false = 0

trueCount : {n : ℕ}(f : Fin n → Bool) → ℕ
trueCount {n = 0} _ = 0
trueCount {n = suc n} f = Bool→ℕ (f (inl tt)) + (trueCount (f ∘ inr))

SumFinDec⊎≃ : (n : ℕ)(t : Bool) → (Bool→Type t ⊎ Fin n) ≃ (Fin (Bool→ℕ t + n))
SumFinDec⊎≃ _ true = idEquiv _
SumFinDec⊎≃ _ false = ⊎-swap-≃ ⋆ ⊎-⊥-≃

SumFinSub≃ : (n : ℕ)(f : Fin n → Bool) → Σ _ (Bool→Type ∘ f) ≃ Fin (trueCount f)
SumFinSub≃ 0 _ = ΣEmpty _
SumFinSub≃ (suc n) f =
    Σ⊎≃
  ⋆ ⊎-equiv (ΣUnit (Bool→Type ∘ f ∘ inl)) (SumFinSub≃ n (f ∘ inr))
  ⋆ SumFinDec⊎≃ _ (f (inl tt))

-- decidable quantifier

trueForSome : (n : ℕ)(f : Fin n → Bool) → Bool
trueForSome 0 _ = false
trueForSome (suc n) f = f (inl tt) or trueForSome n (f ∘ inr)

trueForAll : (n : ℕ)(f : Fin n → Bool) → Bool
trueForAll 0 _ = true
trueForAll (suc n) f = f (inl tt) and trueForAll n (f ∘ inr)

SumFin∃→ : (n : ℕ)(f : Fin n → Bool) → Σ _ (Bool→Type ∘ f) → Bool→Type (trueForSome n f)
SumFin∃→ 0 _ = ΣEmpty _ .fst
SumFin∃→ (suc n) f =
    Bool→Type⊎' _ _
  ∘ map-⊎ (ΣUnit (Bool→Type ∘ f ∘ inl) .fst) (SumFin∃→ n (f ∘ inr))
  ∘ Σ⊎≃ .fst

SumFin∃← : (n : ℕ)(f : Fin n → Bool) → Bool→Type (trueForSome n f) → Σ _ (Bool→Type ∘ f)
SumFin∃← 0 _ = ⊥.rec
SumFin∃← (suc n) f =
    invEq Σ⊎≃
  ∘ map-⊎ (invEq (ΣUnit (Bool→Type ∘ f ∘ inl))) (SumFin∃← n (f ∘ inr))
  ∘ Bool→Type⊎ _ _

SumFin∃≃ : (n : ℕ)(f : Fin n → Bool) → ∥ Σ (Fin n) (Bool→Type ∘ f) ∥ ≃ Bool→Type (trueForSome n f)
SumFin∃≃ n f =
  propBiimpl→Equiv isPropPropTrunc isPropBool→Type
    (Prop.rec isPropBool→Type (SumFin∃→ n f))
    (∣_∣ ∘ SumFin∃← n f)

SumFin∀≃ : (n : ℕ)(f : Fin n → Bool) → ((x : Fin n) → Bool→Type (f x)) ≃ Bool→Type (trueForAll n f)
SumFin∀≃ 0 _ = isContr→≃Unit (isContrΠ⊥)
SumFin∀≃ (suc n) f =
    Π⊎≃
  ⋆ Σ-cong-equiv (ΠUnit (Bool→Type ∘ f ∘ inl)) (λ _ → SumFin∀≃ n (f ∘ inr))
  ⋆ Bool→Type×≃ _ _

-- internal equality

SumFin≡ : (n : ℕ) → (a b : Fin n) → Bool
SumFin≡ 0 _ _ = true
SumFin≡ (suc n) (inl tt) (inl tt) = true
SumFin≡ (suc n) (inl tt) (inr y) = false
SumFin≡ (suc n) (inr x) (inl tt) = false
SumFin≡ (suc n) (inr x) (inr y) = SumFin≡ n x y

isSetSumFin : (n : ℕ)→ isSet (Fin n)
isSetSumFin 0 = isProp→isSet isProp⊥
isSetSumFin (suc n) = isSet⊎ (isProp→isSet isPropUnit) (isSetSumFin n)

SumFin≡≃ : (n : ℕ) → (a b : Fin n) → (a ≡ b) ≃ Bool→Type (SumFin≡ n a b)
SumFin≡≃ 0 _ _ = isContr→≃Unit (isProp→isContrPath isProp⊥ _ _)
SumFin≡≃ (suc n) (inl tt) (inl tt) = isContr→≃Unit (inhProp→isContr refl (isSetSumFin _ _ _))
SumFin≡≃ (suc n) (inl tt) (inr y) = invEquiv (⊎Path.Cover≃Path _ _) ⋆ uninhabEquiv ⊥.rec* ⊥.rec
SumFin≡≃ (suc n) (inr x) (inl tt) = invEquiv (⊎Path.Cover≃Path _ _) ⋆ uninhabEquiv ⊥.rec* ⊥.rec
SumFin≡≃ (suc n) (inr x) (inr y) = invEquiv (_ , isEmbedding-inr x y) ⋆ SumFin≡≃ n x y

-- propositional truncation of Fin

-- decidability of Fin

DecFin : (n : ℕ) → Dec (Fin n)
DecFin 0 = no (idfun _)
DecFin (suc n) = yes fzero

-- propositional truncation of Fin

Dec∥Fin∥ : (n : ℕ) → Dec ∥ Fin n ∥
Dec∥Fin∥ n = Dec∥∥ (DecFin n)

-- some properties about cardinality

fzero≠fone : {n : ℕ} → ¬ (fzero ≡ fsuc fzero)
fzero≠fone {n = n} = SumFin≡≃ (suc (suc n)) fzero (fsuc fzero) .fst

Fin>0→isInhab : (n : ℕ) → 0 < n → Fin n
Fin>0→isInhab 0 p = ⊥.rec (¬-<-zero p)
Fin>0→isInhab (suc n) p = fzero

Fin>1→hasNonEqualTerm : (n : ℕ) → 1 < n → Σ[ i ∈ Fin n ] Σ[ j ∈ Fin n ] ¬ i ≡ j
Fin>1→hasNonEqualTerm 0 p = ⊥.rec (snotz (≤0→≡0 p))
Fin>1→hasNonEqualTerm 1 p = ⊥.rec (snotz (≤0→≡0 (pred-≤-pred p)))
Fin>1→hasNonEqualTerm (suc (suc n)) _ = fzero , fsuc fzero , fzero≠fone

isEmpty→Fin≡0 : (n : ℕ) → ¬ Fin n → 0 ≡ n
isEmpty→Fin≡0 0 _ = refl
isEmpty→Fin≡0 (suc n) p = ⊥.rec (p fzero)

isInhab→Fin>0 : (n : ℕ) → Fin n → 0 < n
isInhab→Fin>0 0 i = ⊥.rec i
isInhab→Fin>0 (suc n) _ = suc-≤-suc zero-≤

hasNonEqualTerm→Fin>1 : (n : ℕ) → (i j : Fin n) → ¬ i ≡ j → 1 < n
hasNonEqualTerm→Fin>1 0 i _ _ = ⊥.rec i
hasNonEqualTerm→Fin>1 1 i j p = ⊥.rec (p (isContr→isProp isContrSumFin1 i j))
hasNonEqualTerm→Fin>1 (suc (suc n)) _ _ _ = suc-≤-suc (suc-≤-suc zero-≤)

Fin≤1→isProp : (n : ℕ) → n ≤ 1 → isProp (Fin n)
Fin≤1→isProp 0 _ = isProp⊥
Fin≤1→isProp 1 _ = isContr→isProp isContrSumFin1
Fin≤1→isProp (suc (suc n)) p = ⊥.rec (¬-<-zero (pred-≤-pred p))

isProp→Fin≤1 : (n : ℕ) → isProp (Fin n) → n ≤ 1
isProp→Fin≤1 0 _ = ≤-solver 0 1
isProp→Fin≤1 1 _ = ≤-solver 1 1
isProp→Fin≤1 (suc (suc n)) p = ⊥.rec (fzero≠fone (p fzero (fsuc fzero)))

-- automorphisms of SumFin

SumFin≃≃ : (n : ℕ) → (Fin n ≃ Fin n) ≃ Fin (LehmerCode.factorial n)
SumFin≃≃ _ =
    equivComp (SumFin≃Fin _) (SumFin≃Fin _)
  ⋆ LehmerCode.lehmerEquiv
  ⋆ LehmerCode.lehmerFinEquiv
  ⋆ invEquiv (SumFin≃Fin _)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Functions.Definition
open import Lists.Definition
open import Lists.Fold.Fold
open import Lists.Length

module Lists.Map.Map where

map : {a b : _} {A : Set a} {B : Set b} (f : A → B) → List A → List B
map f [] = []
map f (x :: list) = (f x) :: (map f list)

map' : {a b : _} {A : Set a} {B : Set b} (f : A → B) → List A → List B
map' f = fold (λ a → (f a) ::_ ) []

map=map' : {a b : _} {A : Set a} {B : Set b} (f : A → B) → (l : List A) → (map f l ≡ map' f l)
map=map' f [] = refl
map=map' f (x :: l) with map=map' f l
... | bl = applyEquality (f x ::_) bl

mapId : {a : _} {A : Set a} (l : List A) → map id l ≡ l
mapId [] = refl
mapId (x :: l) rewrite mapId l = refl

mapMap : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → (l : List A) → {f : A → B} {g : B → C} → map g (map f l) ≡ map (g ∘ f) l
mapMap [] = refl
mapMap (x :: l) {f = f} {g} rewrite mapMap l {f} {g} = refl

mapExtension : {a b : _} {A : Set a} {B : Set b} (l : List A) (f g : A → B) → ({x : A} → (f x ≡ g x)) → map f l ≡ map g l
mapExtension [] f g pr = refl
mapExtension (x :: l) f g pr rewrite mapExtension l f g pr | pr {x} = refl

mapConcat : {a b : _} {A : Set a} {B : Set b} (l1 l2 : List A) (f : A → B) → map f (l1 ++ l2) ≡ (map f l1) ++ (map f l2)
mapConcat [] l2 f = refl
mapConcat (x :: l1) l2 f rewrite mapConcat l1 l2 f = refl

lengthMap : {a b : _} {A : Set a} {B : Set b} → (l : List A) → {f : A → B} → length l ≡ length (map f l)
lengthMap [] {f} = refl
lengthMap (x :: l) {f} rewrite lengthMap l {f} = refl


text:
module Structure.Container.SetLike where
{-
open import Data.Boolean
open import Data.Boolean.Stmt
open import Functional
open import Lang.Instance
import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid renaming (_≡_ to _≡ₛ_ ; _≢_ to _≢ₛ_)
open import Structure.Function.Domain
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Relator hiding (module Names)
open import Type.Properties.Inhabited
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ ℓ₇ ℓ₈ ℓ₉ ℓ₁₀ ℓₗ ℓₗ₁ ℓₗ₂ ℓₗ₃ : Lvl.Level
private variable A B C C₁ C₂ Cₒ Cᵢ E E₁ E₂ : Type{ℓ}
private variable _∈_ _∈ₒ_ _∈ᵢ_ : E → C

module _ {C : Type{ℓ₁}} {E : Type{ℓ₂}} (_∈_ : E → C → Stmt{ℓ₃}) where -- TODO: Maybe generalize C so that it becomes "indexed": `(C : (i : I) → Type{ℓ₁(i)})`? Is it neccessary? Which set-like structures does not fit with the definitions below?
  record SetLike {ℓ₄} : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃ Lvl.⊔ Lvl.𝐒(ℓ₄)} where
    field
      _≡_ : C → C → Stmt{ℓ₄}

    field
      [≡]-membership : ∀{a b} → (a ≡ b) ↔ (∀{x} → (x ∈ a) ↔ (x ∈ b))

    _∋_ : C → E → Stmt
    _∋_ = swap(_∈_)

    _∉_ : E → C → Stmt
    _∉_ = (¬_) ∘₂ (_∈_)

    _≢_ : C → C → Stmt
    _≢_ = (¬_) ∘₂ (_≡_)

  -- A type such that its inhabitants is the elements of the set `S`.
  SetElement : C → Stmt
  SetElement(S) = ∃(_∈ S)

  record SubsetRelation {ℓ₄} : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃ Lvl.⊔ Lvl.𝐒(ℓ₄)} where
    field _⊆_ : C → C → Stmt{ℓ₄}
    Membership = ∀{a b} → (a ⊆ b) ↔ (∀{x} → (x ∈ a) → (x ∈ b))
    field [⊆]-membership : Membership

    _⊇_ : C → C → Stmt
    _⊇_ = swap(_⊆_)

    _⊈_ : C → C → Stmt
    _⊈_ = (¬_) ∘₂ (_⊆_)

    _⊉_ : C → C → Stmt
    _⊉_ = (¬_) ∘₂ (_⊇_)
  open SubsetRelation ⦃ ... ⦄ hiding (Membership ; membership) public
  module Subset ⦃ inst ⦄ = SubsetRelation(inst)

  module FunctionProperties where
    module Names where
      _closed-under₁_ : C → (E → E) → Stmt -- TODO: Maybe possible to generalize over n
      S closed-under₁ f = (∀{x} → (x ∈ S) → (f(x) ∈ S))

      _closed-under₂_ : C → (E → E → E) → Stmt
      S closed-under₂ (_▫_) = (∀{x y} → (x ∈ S) → (y ∈ S) → ((x ▫ y) ∈ S))

    open import Lang.Instance
    module _ (S : C) (f : E → E) where
      record _closed-under₁_ : Stmt{Lvl.of(S Names.closed-under₁ f)} where
        constructor intro
        field proof : S Names.closed-under₁ f
      _closureUnder₁_ = inst-fn _closed-under₁_.proof

    module _ (S : C) (_▫_ : E → E → E) where
      record _closed-under₂_ : Stmt{Lvl.of(S Names.closed-under₂ (_▫_))} where
        constructor intro
        field proof : S Names.closed-under₂ (_▫_)
      _closureUnder₂_ = inst-fn _closed-under₂_.proof

module _ (_∈_ : _) ⦃ setLike : SetLike{ℓ₁}{ℓ₂}{ℓ₃}{C}{E} (_∈_) {ℓ₄} ⦄ where
  open SetLike(setLike)

  module Names where

  record EmptySet : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    field ∅ : C
    Membership = ∀{x} → (x ∉ ∅)
    field membership : Membership
  open EmptySet ⦃ ... ⦄ hiding (Membership ; membership) public
  module Empty ⦃ inst ⦄ = EmptySet(inst)
  {-# DISPLAY EmptySet.∅ = ∅ #-}

  record UniversalSet : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    field 𝐔 : C
    Membership = ∀{x} → (x ∈ 𝐔)
    field membership : Membership
  open UniversalSet ⦃ ... ⦄ hiding (Membership ; membership) public
  module Universal ⦃ inst ⦄ = UniversalSet(inst)

  record UnionOperator : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    field _∪_ : C → C → C
    Membership = ∀{a b}{x} → (x ∈ (a ∪ b)) ↔ ((x ∈ a) ∨ (x ∈ b))
    field membership : Membership
  open UnionOperator ⦃ ... ⦄ hiding (Membership ; membership) public
  module Union ⦃ inst ⦄ = UnionOperator(inst)

  record IntersectionOperator : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    field _∩_ : C → C → C
    Membership = ∀{a b}{x} → (x ∈ (a ∩ b)) ↔ ((x ∈ a) ∧ (x ∈ b))
    field membership : Membership
  open IntersectionOperator ⦃ ... ⦄ hiding (Membership ; membership) public
  module Intersection ⦃ inst ⦄ = IntersectionOperator(inst)
  {-# DISPLAY IntersectionOperator._∩_ = _∩_ #-}

  record WithoutOperator : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    field _∖_ : C → C → C
    Membership = ∀{a b}{x} → (x ∈ (a ∖ b)) ↔ ((x ∈ a) ∧ (x ∉ b))
    field membership : Membership
  open WithoutOperator ⦃ ... ⦄ hiding (Membership ; membership) public
  module Without ⦃ inst ⦄ = WithoutOperator(inst)

  record ComplementOperator : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    field ∁ : C → C
    Membership = ∀{a}{x} → (x ∈ (∁ a)) ↔ (x ∉ a)
    field membership : Membership
  open ComplementOperator ⦃ ... ⦄ hiding (Membership ; membership) public
  module Complement ⦃ inst ⦄ = ComplementOperator(inst)

  module _ {I : Type{ℓ}} ⦃ equiv-I : Equiv{ℓₗ₁}(I) ⦄ ⦃ equiv-E : Equiv{ℓₗ₂}(E) ⦄ where
    record ImageOperator : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃ Lvl.⊔ ℓ Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂} where
      field ⊶ : (f : I → E) → ⦃ func : Function(f) ⦄ → C
      Membership = ∀{f} ⦃ func : Function(f) ⦄ → ∀{y} → (y ∈ (⊶ f)) ↔ ∃(x ↦ f(x) ≡ₛ y)
      field membership : Membership
    open ImageOperator ⦃ ... ⦄ hiding (Membership ; membership) public
    module Image ⦃ inst ⦄ = ImageOperator(inst)

  module _ ⦃ _ : Equiv{ℓₗ}(E) ⦄ where
    record SingletonSet : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃ Lvl.⊔ ℓₗ} where
      field singleton : E → C
      Membership = ∀{y}{x} → (x ∈ singleton(y)) ↔ (x ≡ₛ y)
      field membership : Membership
    open SingletonSet ⦃ ... ⦄ hiding (Membership ; membership) public
    module Singleton ⦃ inst ⦄ = SingletonSet(inst)

    record PairSet : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃ Lvl.⊔ ℓₗ} where
      field pair : E → E → C
      Membership = ∀{y₁ y₂}{x} → (x ∈ pair y₁ y₂) ↔ (x ≡ₛ y₁)∨(x ≡ₛ y₂)
      field membership : Membership
    open PairSet ⦃ ... ⦄ hiding (Membership ; membership) public
    module Pair ⦃ inst ⦄ = PairSet(inst)

    record AddFunction : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃ Lvl.⊔ ℓₗ} where
      field add : E → C → C
      Membership = ∀{y}{a}{x} → (x ∈ add y a) ↔ ((x ∈ a) ∨ (x ≡ₛ y))
      field membership : Membership
    open AddFunction ⦃ ... ⦄ hiding (Membership ; membership) public
    module Add ⦃ inst ⦄ = AddFunction(inst)

    record RemoveFunction : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃ Lvl.⊔ ℓₗ} where
      field remove : E → C → C
      Membership = ∀{y}{a}{x} → (x ∈ remove y a) ↔ ((x ∈ a) ∧ (x ≢ₛ y))
      field membership : Membership
    open RemoveFunction ⦃ ... ⦄ hiding (Membership ; membership) public
    module Remove ⦃ inst ⦄ = RemoveFunction(inst)

    module _ {ℓ} where
      record FilterFunction : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃ Lvl.⊔ Lvl.𝐒(ℓ) Lvl.⊔ ℓₗ} where
        field filter : (P : E → Stmt{ℓ}) ⦃ unaryRelator : UnaryRelator(P) ⦄ → (C → C)
        Membership = ∀{A}{P} ⦃ unaryRelator : UnaryRelator(P) ⦄ {x} → (x ∈ filter P(A)) ↔ ((x ∈ A) ∧ P(x))
        field membership : Membership
      open FilterFunction ⦃ ... ⦄ hiding (Membership ; membership) public
      module Filter ⦃ inst ⦄ = FilterFunction(inst)

  record BooleanFilterFunction : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    field boolFilter : (E → Bool) → (C → C)
    Membership = ∀{A}{P}{x} → (x ∈ boolFilter P(A)) ↔ ((x ∈ A) ∧ IsTrue(P(x)))
    field membership : Membership
  open BooleanFilterFunction ⦃ ... ⦄ hiding (Membership ; membership) public
  module BooleanFilter ⦃ inst ⦄ = BooleanFilterFunction(inst)

module _ (_∈_ : _) ⦃ setLike : SetLike{ℓ₁}{ℓ₂}{ℓ₃}{C}{E} (_∈_) {ℓ₄} ⦄ ⦃ equiv-E : Equiv{ℓₗ₁}(E) ⦄ {O : Type{ℓ₆}} ⦃ equiv-O : Equiv{ℓₗ₂}(O) ⦄ where
  record UnapplyFunction : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃ Lvl.⊔ ℓ₆ Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂} where
    field unapply : (f : E → O) ⦃ func : Function(f) ⦄ → O → C
    Membership = ∀{f} ⦃ func : Function(f) ⦄ {y}{x} → (x ∈ unapply f(y)) ↔ (f(x) ≡ₛ y)
    field membership : Membership
  open UnapplyFunction ⦃ ... ⦄ hiding (Membership ; membership) public
  module Unapply ⦃ inst ⦄ = UnapplyFunction(inst)

module _
  ⦃ equiv-E₁ : Equiv{ℓₗ₁}(E₁) ⦄
  (_∈₁_ : _) ⦃ setLike₁ : SetLike{ℓ₁}{ℓ₂}{ℓ₃}{C₁}{E₁} (_∈₁_) {ℓ₄} ⦄
  ⦃ equiv-E₂ : Equiv{ℓₗ₂}(E₂) ⦄
  (_∈₂_ : _) ⦃ setLike₂ : SetLike{ℓ₆}{ℓ₇}{ℓ₈}{C₂}{E₂} (_∈₂_) {ℓ₉} ⦄
  where

  open SetLike ⦃ … ⦄
  record MapFunction : Type{ℓₗ₁ Lvl.⊔ ℓₗ₂ Lvl.⊔ ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃ Lvl.⊔ ℓ₆ Lvl.⊔ ℓ₇ Lvl.⊔ ℓ₈} where
    field map : (f : E₁ → E₂) ⦃ func : Function(f) ⦄ → (C₁ → C₂)
    Membership = ∀{f} ⦃ func : Function(f) ⦄ {A}{y} → (y ∈₂ map f(A)) ↔ ∃(x ↦ (x ∈₁ A) ∧ (f(x) ≡ₛ y))
    field membership : Membership
  open MapFunction ⦃ ... ⦄ hiding (Membership ; membership) public
  module Map ⦃ inst ⦄ = MapFunction(inst)

  record UnmapFunction : Type{ℓₗ₁ Lvl.⊔ ℓₗ₂ Lvl.⊔ ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃ Lvl.⊔ ℓ₆ Lvl.⊔ ℓ₇ Lvl.⊔ ℓ₈} where
    field unmap : (f : E₁ → E₂) ⦃ func : Function(f) ⦄ → (C₂ → C₁)
    Membership = ∀{f} ⦃ func : Function(f) ⦄ {A}{x} → (x ∈₁ unmap f(A)) ↔ (f(x) ∈₂ A)
    field membership : Membership
  open UnmapFunction ⦃ ... ⦄ hiding (Membership ; membership) public
  module Unmap ⦃ inst ⦄ = UnmapFunction(inst)

module _ (_∈ₒ_ : _) ⦃ outer-setLike : SetLike{ℓ₁}{ℓ₂}{ℓ₃}{Cₒ}{Cᵢ} (_∈ₒ_) {ℓ₄} ⦄ (_∈ᵢ_ : _) ⦃ inner-setLike : SetLike{ℓ₂}{ℓ₆}{ℓ₇}{Cᵢ}{E} (_∈ᵢ_) {ℓ₈} ⦄ where
  open SetLike ⦃ … ⦄

  record PowerFunction ⦃ subset : SubsetRelation(_∈ᵢ_){ℓ₄ = ℓ₉} ⦄ : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃ Lvl.⊔ ℓ₈} where
    field ℘ : Cᵢ → Cₒ
    Membership = ∀{A x} → (x ∈ₒ ℘(A)) ↔ (x ⊆ A)
    field membership : Membership
  open PowerFunction ⦃ ... ⦄ hiding (Membership ; membership) public
  module Power ⦃ inst ⦄ = PowerFunction(inst)

  record BigUnionOperator : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃ Lvl.⊔ ℓ₆ Lvl.⊔ ℓ₇} where
    field ⋃ : Cₒ → Cᵢ
    Membership = ∀{A}{x} → (x ∈ᵢ (⋃ A)) ↔ ∃(a ↦ (a ∈ₒ A) ∧ (x ∈ᵢ a))
    field membership : Membership
  open BigUnionOperator ⦃ ... ⦄ hiding (Membership ; membership) public
  module BigUnion ⦃ inst ⦄ = BigUnionOperator(inst)

  record BigIntersectionOperator : Type{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃ Lvl.⊔ ℓ₆ Lvl.⊔ ℓ₇} where
    field ⋂ : Cₒ → Cᵢ
    Membership = ∀{A} → ∃(_∈ₒ A) → ∀{x} → (x ∈ᵢ (⋂ A)) ↔ (∀{a} → (a ∈ₒ A) → (x ∈ᵢ a))
    field membership : Membership
  open BigIntersectionOperator ⦃ ... ⦄ hiding (Membership ; membership) public
  module BigIntersection ⦃ inst ⦄ = BigIntersectionOperator(inst)

module _ {I : Type{ℓ}} ⦃ equiv-I : Equiv{ℓₗ₁}(I) ⦄ ⦃ equiv-E : Equiv{ℓₗ₂}(E) ⦄ (_∈_ : _) ⦃ setLike : SetLike{ℓ₁}{ℓ₂}{ℓ₃}{C}{E} (_∈_) {ℓ₄}{ℓ₅} ⦄ where
  record IndexedBigUnionOperator : Type{ℓ Lvl.⊔ ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    field ⋃ᵢ : (I → C) → C
    Membership = ∀{Ai}{x} → (x ∈ (⋃ᵢ Ai)) ↔ ∃(i ↦ (x ∈ Ai(i)))
    field membership : Membership
  open IndexedBigUnionOperator ⦃ ... ⦄ hiding (Membership ; membership) public
  module IndexedBigUnion ⦃ inst ⦄ = IndexedBigUnionOperator(inst)

  record IndexedBigIntersectionOperator : Type{ℓ Lvl.⊔ ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    field ⋂ᵢ : (I → C) → C
    Membership = ∀{Ai} → ◊(I) → ∀{x} → (x ∈ (⋂ᵢ Ai)) ↔ (∀{i} → (x ∈ Ai(i)))
    field membership : Membership
  open IndexedBigIntersectionOperator ⦃ ... ⦄ hiding (Membership ; membership) public
  module IndexedBigIntersection ⦃ inst ⦄ = IndexedBigIntersectionOperator(inst)

{-
open SetLike ⦃ … ⦄
  using (
    _∈_ ; _⊆_ ; _≡_ ;
    _∋_ ; _⊇_ ;
    _∉_ ; _⊈_ ; _⊉_ ; _≢_ ;
    ∅ ; _∪_ ; _∩_ ; _∖_ ;
    singleton ; add ; remove
  )
-}
-}

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 --cubical-compatible --show-implicit #-}
-- {-# OPTIONS -v tc.data.sort:20 -v tc.lhs.split.well-formed:100 #-}

module WithoutK5 where

-- Equality defined with one index.

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

weak-K : {A : Set} {a b : A} (p q : a ≡ b) (α β : p ≡ q) → α ≡ β
weak-K refl .refl refl refl = refl


text:
-- Andreas, 2016-02-21 issue 1862 reported by nad
-- {-# OPTIONS -v tc.decl:10 -v tc.def.where:10 -v tc.meta:10 -v tc.size.solve:100 #-}

open import Common.Size

data Nat (i : Size) : Set where
  zero : Nat i
  suc  : (j : Size< i) (n : Nat j) → Nat i

id : ∀ i → Nat i → Nat i
id _ zero      = zero
id _ (suc j n) = s
  where
    mutual
      s = suc _ r  -- should not be instantiated to ∞x
      r = id _ n


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

open import lib.Basics
open import lib.types.Span
open import lib.types.Pointed
open import lib.types.Pushout
open import lib.types.PushoutFlattening
open import lib.types.Unit
open import lib.types.Paths
open import lib.types.Lift
open import lib.cubical.Square

-- Suspension is defined as a particular case of pushout

module lib.types.Suspension where

module _ {i} (A : Type i) where

  suspension-span : Span
  suspension-span = span Unit Unit A (λ _ → tt) (λ _ → tt)

  Suspension : Type i
  Suspension = Pushout suspension-span

  -- [north'] and [south'] explictly ask for [A]

  north' : Suspension
  north' = left tt

  south' : Suspension
  south' = right tt

module _ {i} {A : Type i} where

  north : Suspension A
  north = north' A

  south : Suspension A
  south = south' A

  merid : A → north == south
  merid x = glue x

  module SuspensionElim {j} {P : Suspension A → Type j} (n : P north)
    (s : P south) (p : (x : A) → n == s [ P ↓ merid x ]) where
    open module P = PushoutElim (λ _ → n) (λ _ → s) p
      public using (f) renaming (glue-β to merid-β)

  open SuspensionElim public using () renaming (f to Suspension-elim)

  module SuspensionRec {j} {C : Type j} (n s : C) (p : A → n == s) where
    open module P = PushoutRec {d = suspension-span A} (λ _ → n) (λ _ → s) p
      public using (f) renaming (glue-β to merid-β)

  open SuspensionRec public using () renaming (f to Suspension-rec)

  module SuspensionRecType {j} (n s : Type j) (p : A → n ≃ s)
    = PushoutRecType {d = suspension-span A} (λ _ → n) (λ _ → s) p

suspension-⊙span : ∀ {i} → Ptd i → ⊙Span
suspension-⊙span X =
  ⊙span ⊙Unit ⊙Unit X (⊙cst {X = X}) (⊙cst {X = X})

⊙Susp : ∀ {i} → Ptd i → Ptd i
⊙Susp (A , _) = ⊙[ Suspension A , north ]

σloop : ∀ {i} (X : Ptd i) → fst X → north' (fst X) == north' (fst X)
σloop (_ , x₀) x = merid x ∙ ! (merid x₀)

σloop-pt : ∀ {i} {X : Ptd i} → σloop X (snd X) == idp
σloop-pt {X = (_ , x₀)} = !-inv-r (merid x₀)

module FlipSusp {i} {A : Type i} = SuspensionRec
  (south' A) north (! ∘ merid)

flip-susp : ∀ {i} {A : Type i} → Suspension A → Suspension A
flip-susp = FlipSusp.f

⊙flip-susp : ∀ {i} (X : Ptd i) → fst (⊙Susp X ⊙→ ⊙Susp X)
⊙flip-susp X = (flip-susp , ! (merid (snd X)))

module _ {i j} where

  module SuspFmap {A : Type i} {B : Type j} (f : A → B) =
    SuspensionRec north south (merid ∘ f)

  susp-fmap : {A : Type i} {B : Type j} (f : A → B)
    → (Suspension A → Suspension B)
  susp-fmap = SuspFmap.f

  ⊙susp-fmap : {X : Ptd i} {Y : Ptd j} (f : fst (X ⊙→ Y))
    → fst (⊙Susp X ⊙→ ⊙Susp Y)
  ⊙susp-fmap (f , fpt) = (susp-fmap f , idp)

module _ {i} where

  susp-fmap-idf : (A : Type i) → ∀ a → susp-fmap (idf A) a == a
  susp-fmap-idf A = Suspension-elim idp idp $ λ a →
    ↓-='-in (ap-idf (merid a) ∙ ! (SuspFmap.merid-β (idf A) a))

  ⊙susp-fmap-idf : (X : Ptd i)
    → ⊙susp-fmap (⊙idf X) == ⊙idf (⊙Susp X)
  ⊙susp-fmap-idf X = ⊙λ= (susp-fmap-idf (fst X)) idp

module _ {i j} where

  susp-fmap-cst : {A : Type i} {B : Type j} (b : B)
    (a : Suspension A) → susp-fmap (cst b) a == north
  susp-fmap-cst b = Suspension-elim idp (! (merid b)) $ (λ a →
    ↓-app=cst-from-square $ SuspFmap.merid-β (cst b) a ∙v⊡ tr-square _)

  ⊙susp-fmap-cst : {X : Ptd i} {Y : Ptd j}
    → ⊙susp-fmap (⊙cst {X = X} {Y = Y}) == ⊙cst
  ⊙susp-fmap-cst = ⊙λ= (susp-fmap-cst _) idp

module _ {i j k} where

  susp-fmap-∘ : {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A → B)
    (σ : Suspension A) → susp-fmap (g ∘ f) σ == susp-fmap g (susp-fmap f σ)
  susp-fmap-∘ g f = Suspension-elim
    idp
    idp
    (λ a → ↓-='-in $
      ap-∘ (susp-fmap g) (susp-fmap f) (merid a)
      ∙ ap (ap (susp-fmap g)) (SuspFmap.merid-β f a)
      ∙ SuspFmap.merid-β g (f a)
      ∙ ! (SuspFmap.merid-β (g ∘ f) a))

  ⊙susp-fmap-∘ : {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
    (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y))
    → ⊙susp-fmap (g ⊙∘ f) == ⊙susp-fmap g ⊙∘ ⊙susp-fmap f
  ⊙susp-fmap-∘ g f = ⊙λ= (susp-fmap-∘ (fst g) (fst f)) idp

{- Extract the 'glue component' of a pushout -}
module _ {i j k} {s : Span {i} {j} {k}} where

  module ExtGlue = PushoutRec {d = s} {D = Suspension (Span.C s)}
    (λ _ → north) (λ _ → south) merid

  ext-glue = ExtGlue.f

  module _ {x₀ : Span.A s} where

    ⊙ext-glue :
      fst ((Pushout s , left x₀) ⊙→ (Suspension (Span.C s) , north))
    ⊙ext-glue = (ext-glue , idp)

module _ {i j} {A : Type i} {B : Type j} where

  equiv-Suspension : A ≃ B → Suspension A ≃ Suspension B
  equiv-Suspension eq = equiv to from to-from from-to where
    module To = SuspensionRec north south (λ a → merid (–> eq a))
    module From = SuspensionRec north south (λ b → merid (<– eq b))

    to : Suspension A → Suspension B
    to = To.f

    from : Suspension B → Suspension A
    from = From.f

    to-from : ∀ b → to (from b) == b
    to-from = Suspension-elim idp idp to-from-merid where
      to-from-merid : ∀ b → idp == idp [ (λ b → to (from b) == b) ↓ merid b ]
      to-from-merid b = ↓-app=idf-in $
        idp ∙' merid b
          =⟨ ∙'-unit-l (merid b) ⟩
        merid b
          =⟨ ! $ <–-inv-r eq b |in-ctx merid ⟩
        merid (–> eq (<– eq b))
          =⟨ ! $ To.merid-β (<– eq b) ⟩
        ap to (merid (<– eq b))
          =⟨ ! $ From.merid-β b |in-ctx ap To.f ⟩
        ap to (ap from (merid b))
          =⟨ ! $ ap-∘ to from (merid b) ⟩
        ap (to ∘ from) (merid b)
          =⟨ ! $ ∙-unit-r (ap (to ∘ from) (merid b)) ⟩
        ap (to ∘ from) (merid b) ∙ idp
          ∎

    from-to : ∀ a → from (to a) == a
    from-to = Suspension-elim idp idp from-to-merid where
      from-to-merid : ∀ a → idp == idp [ (λ a → from (to a) == a) ↓ merid a ]
      from-to-merid a = ↓-app=idf-in $
        idp ∙' merid a
          =⟨ ∙'-unit-l (merid a) ⟩
        merid a
          =⟨ ! $ <–-inv-l eq a |in-ctx merid ⟩
        merid (<– eq (–> eq a))
          =⟨ ! $ From.merid-β (–> eq a) ⟩
        ap from (merid (–> eq a))
          =⟨ ! $ To.merid-β a |in-ctx ap From.f ⟩
        ap from (ap to (merid a))
          =⟨ ! $ ap-∘ from to (merid a) ⟩
        ap (from ∘ to) (merid a)
          =⟨ ! $ ∙-unit-r (ap (from ∘ to) (merid a)) ⟩
        ap (from ∘ to) (merid a) ∙ idp
          ∎

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  ⊙equiv-⊙Susp : X ⊙≃ Y → ⊙Susp X ⊙≃ ⊙Susp Y
  ⊙equiv-⊙Susp ⊙eq = ⊙≃-in (equiv-Suspension (fst (⊙≃-out ⊙eq))) idp

{- Interaction with [Lift] -}
module _ {i j} (X : Type i) where

  Suspension-Lift-equiv-Lift-Suspension : Suspension (Lift {j = j} X) ≃ Lift {j = j} (Suspension X)
  Suspension-Lift-equiv-Lift-Suspension = lift-equiv ∘e equiv-Suspension lower-equiv

  Suspension-Lift : Suspension (Lift {j = j} X) == Lift {j = j} (Suspension X)
  Suspension-Lift = ua Suspension-Lift-equiv-Lift-Suspension

module _ {i j} (X : Ptd i) where

  ⊙Susp-⊙Lift-⊙equiv-⊙Lift-⊙Susp : ⊙Susp (⊙Lift {j = j} X) ⊙≃ ⊙Lift {j = j} (⊙Susp X)
  ⊙Susp-⊙Lift-⊙equiv-⊙Lift-⊙Susp = ⊙lift-equiv {j = j} ⊙∘e ⊙equiv-⊙Susp {X = ⊙Lift {j = j} X} {Y = X} ⊙lower-equiv

  ⊙Susp-⊙Lift : ⊙Susp (⊙Lift {j = j} X) == ⊙Lift {j = j} (⊙Susp X)
  ⊙Susp-⊙Lift = ⊙ua ⊙Susp-⊙Lift-⊙equiv-⊙Lift-⊙Susp

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda