text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Group.MorphismProperties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Function using (_∘_; id)
open import Cubical.Foundations.GroupoidLaws hiding (_⁻¹)
open import Cubical.Functions.Embedding
open import Cubical.Data.Sigma
open import Cubical.Data.Prod using (isPropProd)

open import Cubical.Algebra
open import Cubical.Algebra.Properties
open import Cubical.Algebra.Group.Morphism

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Record

open import Cubical.Algebra.Monoid.Properties using (isPropIsMonoid)

open import Cubical.Relation.Binary.Reasoning.Equality

open Iso

private
  variable
    ℓ ℓ′ ℓ′′ : Level
    F : Group ℓ
    G : Group ℓ′
    H : Group ℓ′′

isPropIsGroupHom : ∀ (G : Group ℓ) (H : Group ℓ′) f → isProp (IsGroupHom G H f)
isPropIsGroupHom G H f (isgrouphom aHom) (isgrouphom bHom) =
  cong isgrouphom
    (isPropHomomorphic₂ (Group.is-set H) f (Group._•_ G) (Group._•_ H) aHom bHom)

isSetGroupHom : isSet (G ⟶ᴴ H)
isSetGroupHom {G = G} {H = H} = isOfHLevelRespectEquiv 2 equiv
                                  (isSetΣ (isSetΠ λ _ → is-set H)
                                          (λ f → isProp→isSet (isPropIsGroupHom G H f)))
  where
    open Group
    equiv : (Σ[ g ∈ (⟨ G ⟩ → ⟨ H ⟩) ] IsGroupHom G H g) ≃ GroupHom G H
    equiv = isoToEquiv (iso (λ (g , m) → grouphom g m)
                            (λ (grouphom g m) → g , m)
                            (λ _ → refl) λ _ → refl)

isGroupHomComp : {f : ⟨ F ⟩ → ⟨ G ⟩} {g : ⟨ G ⟩ → ⟨ H ⟩}
                  → IsGroupHom F G f → IsGroupHom G H g → IsGroupHom F H (g ∘ f)
isGroupHomComp {g = g} (isgrouphom fHom) (isgrouphom gHom) =
  isgrouphom (λ _ _ → cong g (fHom _ _) ∙ gHom _ _)

private
  isGroupHomComp′ : (f : F ⟶ᴴ G) (g : G ⟶ᴴ H)
                    → IsGroupHom F H (GroupHom.fun g ∘ GroupHom.fun f)
  isGroupHomComp′ (grouphom f (isgrouphom fHom)) (grouphom g (isgrouphom gHom)) =
    isgrouphom (λ _ _ → cong g (fHom _ _) ∙ gHom _ _)

compGroupHom : (F ⟶ᴴ G) → (G ⟶ᴴ H) → (F ⟶ᴴ H)
compGroupHom f g = grouphom _ (isGroupHomComp′ f g)

compGroupEquiv : F ≃ᴴ G → G ≃ᴴ H → F ≃ᴴ H
compGroupEquiv f g = groupequiv (compEquiv f.eq g.eq) (isGroupHomComp′ f.hom g.hom)
  where
    module f = GroupEquiv f
    module g = GroupEquiv g

isGroupHomId : (G : Group ℓ) → IsGroupHom G G id
isGroupHomId G = record
  { preservesOp = λ _ _ → refl
  }

idGroupHom : (G : Group ℓ) → (G ⟶ᴴ G)
idGroupHom G = record
  { fun   = id
  ; isHom = isGroupHomId G
  }

idGroupEquiv : (G : Group ℓ) → G ≃ᴴ G
idGroupEquiv G = record
  { eq    = idEquiv ⟨ G ⟩
  ; isHom = isGroupHomId G
  }

-- Isomorphism inversion
isGroupHomInv : (eqv : G ≃ᴴ H) → IsGroupHom H G (invEq (GroupEquiv.eq eqv))
isGroupHomInv {G = G} {H = H} (groupequiv eq (isgrouphom hom)) = isgrouphom (λ x y → isInj-f (
    f (f⁻¹ (x H.• y))       ≡⟨ retEq eq _ ⟩
    x H.• y                 ≡˘⟨ cong₂ H._•_ (retEq eq x) (retEq eq y) ⟩
    f (f⁻¹ x) H.• f (f⁻¹ y) ≡˘⟨ hom (f⁻¹ x) (f⁻¹ y) ⟩
    f (f⁻¹ x G.• f⁻¹ y)     ∎))
    where
      module G = Group G
      module H = Group H
      f = equivFun eq
      f⁻¹ = invEq eq
      isInj-f : {x y : ⟨ G ⟩} → f x ≡ f y → x ≡ y
      isInj-f {x} {y} = invEq (_ , isEquiv→isEmbedding (eq .snd) x y)

invGroupHom : G ≃ᴴ H → (H ⟶ᴴ G)
invGroupHom eq = record { isHom = isGroupHomInv eq }

invGroupEquiv : G ≃ᴴ H → H ≃ᴴ G
invGroupEquiv eq = record
  { eq    = invEquiv (GroupEquiv.eq eq)
  ; isHom = isGroupHomInv eq
  }

groupHomEq : {f g : G ⟶ᴴ H} → (GroupHom.fun f ≡ GroupHom.fun g) → f ≡ g
groupHomEq {G = G} {H = H} {grouphom f fm} {grouphom g gm} p i =
  grouphom (p i) (p-hom i)
  where
    p-hom : PathP (λ i → IsGroupHom G H (p i)) fm gm
    p-hom = toPathP (isPropIsGroupHom G H _ _ _)

groupEquivEq : {f g : G ≃ᴴ H} → (GroupEquiv.eq f ≡ GroupEquiv.eq g) → f ≡ g
groupEquivEq {G = G} {H = H} {groupequiv f fm} {groupequiv g gm} p i =
  groupequiv (p i) (p-hom i)
  where
    p-hom : PathP (λ i → IsGroupHom G H (p i .fst)) fm gm
    p-hom = toPathP (isPropIsGroupHom G H _ _ _)

module GroupΣTheory {ℓ} where

  RawGroupStructure : Type ℓ → Type ℓ
  RawGroupStructure X = (X → X → X) × X × (X → X)

  RawGroupEquivStr = AutoEquivStr RawGroupStructure

  rawGroupUnivalentStr : UnivalentStr _ RawGroupEquivStr
  rawGroupUnivalentStr = autoUnivalentStr RawGroupStructure

  GroupAxioms : (G : Type ℓ) → RawGroupStructure G → Type ℓ
  GroupAxioms G (_•_ , ε , _⁻¹) = IsMonoid G _•_ ε × Inverse ε _⁻¹ _•_

  GroupStructure : Type ℓ → Type ℓ
  GroupStructure = AxiomsStructure RawGroupStructure GroupAxioms

  GroupΣ : Type (ℓ-suc ℓ)
  GroupΣ = TypeWithStr ℓ GroupStructure

  isPropGroupAxioms : (G : Type ℓ) (s : RawGroupStructure G) → isProp (GroupAxioms G s)
  isPropGroupAxioms G (_•_ , ε , _⁻¹) = isPropΣ isPropIsMonoid
                                    λ isMonG → isPropInverse (IsMonoid.is-set isMonG) _•_ _⁻¹ ε

  GroupEquivStr : StrEquiv GroupStructure ℓ
  GroupEquivStr = AxiomsEquivStr RawGroupEquivStr GroupAxioms

  GroupAxiomsIsoIsGroup : {G : Type ℓ} (s : RawGroupStructure G) →
                          Iso (GroupAxioms G s) (IsGroup G (s .fst) (s .snd .fst) (s .snd .snd))
  fun (GroupAxiomsIsoIsGroup s) (x , y)       = isgroup x y
  inv (GroupAxiomsIsoIsGroup s) (isgroup x y) = (x , y)
  rightInv (GroupAxiomsIsoIsGroup s) _        = refl
  leftInv (GroupAxiomsIsoIsGroup s) _         = refl

  GroupAxioms≡IsGroup : {G : Type ℓ} (s : RawGroupStructure G) →
                        GroupAxioms G s ≡ IsGroup G (s .fst) (s .snd .fst) (s .snd .snd)
  GroupAxioms≡IsGroup s = isoToPath (GroupAxiomsIsoIsGroup s)

  Group→GroupΣ : Group ℓ → GroupΣ
  Group→GroupΣ (mkgroup G _•_ ε _⁻¹ isGroup) =
    G , (_•_ , ε , _⁻¹) , GroupAxiomsIsoIsGroup (_•_ , ε , _⁻¹) .inv isGroup

  GroupΣ→Group : GroupΣ → Group ℓ
  GroupΣ→Group (G , (_•_ , ε , _⁻¹) , isGroupG) =
    mkgroup G _•_ ε _⁻¹ (GroupAxiomsIsoIsGroup (_•_ , ε , _⁻¹) .fun isGroupG)

  GroupIsoGroupΣ : Iso (Group ℓ) GroupΣ
  GroupIsoGroupΣ =
    iso Group→GroupΣ GroupΣ→Group (λ _ → refl) (λ _ → refl)

  groupUnivalentStr : UnivalentStr GroupStructure GroupEquivStr
  groupUnivalentStr = axiomsUnivalentStr _ isPropGroupAxioms rawGroupUnivalentStr

  GroupΣPath : (G H : GroupΣ) → (G ≃[ GroupEquivStr ] H) ≃ (G ≡ H)
  GroupΣPath = SIP groupUnivalentStr

  GroupEquivΣ : (G H : Group ℓ) → Type ℓ
  GroupEquivΣ G H = Group→GroupΣ G ≃[ GroupEquivStr ] Group→GroupΣ H

  GroupIsoΣPath : {G H : Group ℓ} → Iso (GroupEquiv G H) (GroupEquivΣ G H)
  fun GroupIsoΣPath (groupequiv eq hom) = eq , IsGroupHom.preservesOp hom , IsGroupHom.preservesId hom , IsGroupHom.preservesInv hom
  inv GroupIsoΣPath (eq , hom , _)      = groupequiv eq (isgrouphom hom)
  rightInv (GroupIsoΣPath {H = H}) _    = ΣPathTransport→PathΣ _ _ (refl ,
                                          ΣPathTransport→PathΣ _ _ (transportRefl _ ,
                                          ΣPathTransport→PathΣ _ _
                                          (Group.is-set H _ _ _ _ ,
                                          isPropΠ (λ _ → Group.is-set H _ _) _ _ )
                                          ))
  leftInv (GroupIsoΣPath {H = H}) _     = refl

  GroupPath : (G H : Group ℓ) → (GroupEquiv G H) ≃ (G ≡ H)
  GroupPath G H =
    GroupEquiv G H                   ≃⟨ isoToEquiv GroupIsoΣPath ⟩
    GroupEquivΣ G H                  ≃⟨ GroupΣPath _ _ ⟩
    Group→GroupΣ G ≡ Group→GroupΣ H  ≃⟨ isoToEquiv (invIso (congIso GroupIsoGroupΣ)) ⟩
    G ≡ H                            ■

  RawGroupΣ : Type (ℓ-suc ℓ)
  RawGroupΣ = TypeWithStr ℓ RawGroupStructure

  Group→RawGroupΣ : Group ℓ → RawGroupΣ
  Group→RawGroupΣ (mkgroup A _•_ ε _⁻¹ _) = A , _•_ , ε , _⁻¹

  InducedGroup : (G : Group ℓ) (H : RawGroupΣ) (e : G .Group.Carrier ≃ H .fst)
                 → RawGroupEquivStr (Group→RawGroupΣ G) H e → Group ℓ
  InducedGroup G H e r =
    GroupΣ→Group (inducedStructure rawGroupUnivalentStr (Group→GroupΣ G) H (e , r))

  InducedGroupPath : (G : Group ℓ) (H : RawGroupΣ) (e : G .Group.Carrier ≃ H .fst)
                      (E : RawGroupEquivStr (Group→RawGroupΣ G) H e) →
                      G ≡ InducedGroup G H e E
  InducedGroupPath G H e E =
    GroupPath G (InducedGroup G H e E) .fst (groupequiv e (isgrouphom (E .fst)))

-- We now extract the important results from the above module

open GroupΣTheory public using (InducedGroup; InducedGroupPath)

isPropIsGroup : {G : Type ℓ} {_•_ : Op₂ G} {ε : G} {_⁻¹ : Op₁ G} → isProp (IsGroup G _•_ ε _⁻¹)
isPropIsGroup =
  subst isProp (GroupΣTheory.GroupAxioms≡IsGroup (_ , _ , _))
        (GroupΣTheory.isPropGroupAxioms _ (_ , _ , _))

GroupPath : (G ≃ᴴ H) ≃ (G ≡ H)
GroupPath = GroupΣTheory.GroupPath _ _

open Group

uaGroup : G ≃ᴴ H → G ≡ H
uaGroup = equivFun GroupPath

carac-uaGroup : {G H : Group ℓ} (f : G ≃ᴴ H) → cong Carrier (uaGroup f) ≡ ua (GroupEquiv.eq f)
carac-uaGroup (groupequiv f m) =
  (refl ∙∙ ua f ∙∙ refl) ≡˘⟨ rUnit (ua f) ⟩
  ua f                   ∎

Group≡ : (G H : Group ℓ) → (
  Σ[ p ∈ ⟨ G ⟩ ≡ ⟨ H ⟩ ]
  Σ[ q ∈ PathP (λ i → p i → p i → p i) (_•_ G) (_•_ H) ]
  Σ[ r ∈ PathP (λ i → p i) (ε G) (ε H) ]
  Σ[ s ∈ PathP (λ i → p i → p i) (_⁻¹ G) (_⁻¹ H) ]
  PathP (λ i → IsGroup (p i) (q i) (r i) (s i)) (isGroup G) (isGroup H))
  ≃ (G ≡ H)
Group≡ G H = isoToEquiv (iso
  (λ (p , q , r , s , t) i → mkgroup (p i) (q i) (r i) (s i) (t i))
  (λ p → cong Carrier p , cong _•_ p , cong ε p , cong _⁻¹ p , cong isGroup p)
  (λ _ → refl) (λ _ → refl))

caracGroup≡ : {G H : Group ℓ} (p q : G ≡ H) → cong Carrier p ≡ cong Carrier q → p ≡ q
caracGroup≡ {G = G} {H} p q t = cong (fst (Group≡ G H)) (Σ≡Prop (λ _ → isPropΣ
    (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set H) _ _) λ _ → isPropΣ
    (isOfHLevelPathP' 1 (is-set H) _ _) λ _ → isPropΣ
    (isOfHLevelPathP' 1 (isSetΠ λ _ → is-set H) _ _) λ _ →
    isOfHLevelPathP 1 isPropIsGroup _ _)
  t)

uaGroupId : (G : Group ℓ) → uaGroup (idGroupEquiv G) ≡ refl
uaGroupId G = caracGroup≡ _ _ (carac-uaGroup (idGroupEquiv G) ∙ uaIdEquiv)

uaCompGroupEquiv : {F G H : Group ℓ} (f : GroupEquiv F G) (g : GroupEquiv G H) → uaGroup (compGroupEquiv f g) ≡ uaGroup f ∙ uaGroup g
uaCompGroupEquiv f g = caracGroup≡ _ _ (
  cong Carrier (uaGroup (compGroupEquiv f g))
    ≡⟨ carac-uaGroup (compGroupEquiv f g) ⟩
  ua (eq (compGroupEquiv f g))
    ≡⟨ uaCompEquiv _ _ ⟩
  ua (eq f) ∙ ua (eq g)
    ≡˘⟨ cong (_∙ ua (eq g)) (carac-uaGroup f) ⟩
  cong Carrier (uaGroup f) ∙ ua (eq g)
    ≡˘⟨ cong (cong Carrier (uaGroup f) ∙_) (carac-uaGroup g) ⟩
  cong Carrier (uaGroup f) ∙ cong Carrier (uaGroup g)
    ≡˘⟨ cong-∙ Carrier (uaGroup f) (uaGroup g) ⟩
  cong Carrier (uaGroup f ∙ uaGroup g) ∎)
  where open GroupEquiv


text:
module Bad where

data Bool : Set where
  false : Bool
  true  : Bool

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

F : Bool -> Set
F false = Bool
F true  = Nat

cast : {x : Bool} -> F x -> F x
cast a = a

not : Bool -> Bool
not true  = false
not false = true

oops : Bool
oops = not (cast zero)

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module _ where

open import Agda.Builtin.Reflection
open import Agda.Builtin.Bool
open import Agda.Builtin.Unit
open import Agda.Builtin.String
open import Common.Prelude

_<_ = primQNameLess

True : Bool → Set
True true  = ⊤
True false = ⊥

zzz aaa : ⊤
zzz = _
aaa = _

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

check : (x y : Name) → True (x < y) → String
check x y prf with x < y
check x y prf | true = "A-ok"
check x y prf | false = ⊥-elim prf

main : IO Unit
main = putStrLn (check (quote zzz) (quote aaa) _)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The reflexive, symmetric and transitive closure of a binary
-- relation (aka the equivalence closure).
------------------------------------------------------------------------

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

module Relation.Binary.Construct.Closure.Equivalence where

open import Function using (flip; id; _∘_)
open import Level using (_⊔_)
open import Relation.Binary
open import Relation.Binary.Construct.Closure.ReflexiveTransitive as Star
  using (Star; ε; _◅◅_; reverse)
open import Relation.Binary.Construct.Closure.Symmetric as SC using (SymClosure)

------------------------------------------------------------------------
-- Definition

EqClosure : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Rel A (a ⊔ ℓ)
EqClosure _∼_ = Star (SymClosure _∼_)

------------------------------------------------------------------------
-- Equivalence closures are equivalences.

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

  reflexive : Reflexive (EqClosure _∼_)
  reflexive = ε

  transitive : Transitive (EqClosure _∼_)
  transitive = _◅◅_

  symmetric : Symmetric (EqClosure _∼_)
  symmetric = reverse (SC.symmetric _∼_)

  isEquivalence : IsEquivalence (EqClosure _∼_)
  isEquivalence = record
    { refl  = reflexive
    ; sym   = symmetric
    ; trans = transitive
    }

  setoid : Setoid a (a ⊔ ℓ)
  setoid = record
    { _≈_           = EqClosure _∼_
    ; isEquivalence = isEquivalence
    }

------------------------------------------------------------------------
-- Operations

module _ {a ℓ₁ ℓ₂} {A : Set a} where

  -- A generalised variant of map which allows the index type to change.

  gmap : ∀ {b} {B : Set b} {P : Rel A ℓ₁} {Q : Rel B ℓ₂} →
         (f : A → B) → P =[ f ]⇒ Q → EqClosure P =[ f ]⇒ EqClosure Q
  gmap {Q = Q} f = Star.gmap f ∘ SC.gmap {Q = Q} f

  map : ∀ {P : Rel A ℓ₁} {Q : Rel A ℓ₂} →
        P ⇒ Q → EqClosure P ⇒ EqClosure Q
  map = gmap id


text:
module Prelude.Int.Properties where

open import Prelude.Unit
open import Prelude.Nat
open import Prelude.Nat.Properties
open import Prelude.Number
open import Prelude.Equality
open import Prelude.Int.Core
open import Prelude.Smashed
open import Prelude.Ord
open import Prelude.Semiring
open import Prelude.Function

--- Specification functions ---
---   sucInt   a   =  1 + a
---   predInt  a   = -1 + a
---   sucsInt  n a = pos n + a
---   predsInt n a = neg n + a
---   diffNat  a b = a -NZ b

sucInt : Int → Int
sucInt (pos n)          = pos (suc n)
sucInt (negsuc zero)    = pos zero
sucInt (negsuc (suc n)) = negsuc n

predInt : Int → Int
predInt (pos zero)    = negsuc zero
predInt (pos (suc n)) = pos n
predInt (negsuc n)    = negsuc (suc n)

sucsInt : Nat → Int → Int
sucsInt zero    b = b
sucsInt (suc a) b = sucInt (sucsInt a b)

predsInt : Nat → Int → Int
predsInt zero    b = b
predsInt (suc a) b = predInt (predsInt a b)

diffNat : Nat → Nat → Int
diffNat a       zero    = pos a
diffNat zero    (suc b) = negsuc b
diffNat (suc a) (suc b) = diffNat a b

--- Injectivity proofs ---

pos-inj : ∀ {a b} → pos a ≡ pos b → a ≡ b
pos-inj refl = refl

negsuc-inj : ∀ {a b} → negsuc a ≡ negsuc b → a ≡ b
negsuc-inj refl = refl

neg-inj : ∀ {a b} → neg a ≡ neg b → a ≡ b
neg-inj {zero}  {zero}  eq = refl
neg-inj {zero}  {suc b} ()
neg-inj {suc a} {zero}  ()
neg-inj {suc a} {suc b} eq = suc $≡ negsuc-inj eq

negate-inj : {a b : Int} → negate a ≡ negate b → a ≡ b
negate-inj {pos    a}    {pos    b}    eq = pos $≡ neg-inj eq
negate-inj {pos  zero}   {negsuc b}    ()
negate-inj {pos (suc a)} {negsuc b}    ()
negate-inj {negsuc a}    {pos zero}    ()
negate-inj {negsuc a}    {pos (suc _)} ()
negate-inj {negsuc a}    {negsuc b}    eq = negsuc $≡ suc-inj (pos-inj eq)

sucInt-inj : ∀ a b → sucInt a ≡ sucInt b → a ≡ b
sucInt-inj (pos a)          (pos a)          refl = refl
sucInt-inj (pos a)          (negsuc zero)    ()
sucInt-inj (pos a)          (negsuc (suc b)) ()
sucInt-inj (negsuc zero)    (pos b) ()
sucInt-inj (negsuc (suc a)) (pos b) ()
sucInt-inj (negsuc zero)    (negsuc zero)    eq = refl
sucInt-inj (negsuc zero)    (negsuc (suc b)) ()
sucInt-inj (negsuc (suc a)) (negsuc zero)    ()
sucInt-inj (negsuc (suc a)) (negsuc (suc a)) refl = refl

predInt-inj : ∀ a b → predInt a ≡ predInt b → a ≡ b
predInt-inj (pos zero)    (pos zero)    eq = refl
predInt-inj (pos zero)    (pos (suc b)) ()
predInt-inj (pos (suc a)) (pos zero)    ()
predInt-inj (pos (suc a)) (pos (suc a)) refl = refl
predInt-inj (pos zero)    (negsuc b)    ()
predInt-inj (pos (suc a)) (negsuc b)    ()
predInt-inj (negsuc a)    (pos zero)    ()
predInt-inj (negsuc a)    (pos (suc b)) ()
predInt-inj (negsuc a)    (negsuc a)    refl = refl

--- sucInt and predInt are inverses --

sucInt-predInt : ∀ a → sucInt (predInt a) ≡ a
sucInt-predInt (pos zero)    = refl
sucInt-predInt (pos (suc n)) = refl
sucInt-predInt (negsuc n)    = refl

predInt-sucInt : ∀ a → predInt (sucInt a) ≡ a
predInt-sucInt (pos n)          = refl
predInt-sucInt (negsuc zero)    = refl
predInt-sucInt (negsuc (suc n)) = refl

--- Commutativity of _+_ is easy

addInt-commute : (a b : Int) → a + b ≡ b + a
addInt-commute (pos    a) (pos    b) = pos $≡ add-commute a b
addInt-commute (pos    a) (negsuc b) = refl
addInt-commute (negsuc a) (pos    b) = refl
addInt-commute (negsuc a) (negsuc b) = negsuc ∘ suc $≡ add-commute a b

--- Proving _-NZ_ == diffNat

-NZ-suc : ∀ a b → suc a -NZ suc b ≡ a -NZ b
-NZ-suc a b rewrite smashed {x = compare (suc a) (suc b)} {suc-comparison (compare a b)}
            with    compare a b
... | less    (diff! k) = refl
... | equal   eq        = refl
... | greater (diff! k) = refl

-NZ-spec : ∀ a b → a -NZ b ≡ diffNat a b
-NZ-spec zero    zero    = refl
-NZ-spec (suc a) zero    = refl
-NZ-spec zero    (suc b) = refl
-NZ-spec (suc a) (suc b) = -NZ-suc a b ⟨≡⟩ -NZ-spec a b

--- diffNat distributes over suc in both arguments...

diffNat-suc-l : ∀ a b → diffNat (suc a) b ≡ sucInt (diffNat a b)
diffNat-suc-l a       0             = refl
diffNat-suc-l 0       1             = refl
diffNat-suc-l 0       (suc (suc b)) = refl
diffNat-suc-l (suc a) (suc b)       = diffNat-suc-l a b

diffNat-suc-r : ∀ a b → diffNat a (suc b) ≡ predInt (diffNat a b)
diffNat-suc-r zero    zero    = refl
diffNat-suc-r zero    (suc b) = refl
diffNat-suc-r (suc a) zero    = refl
diffNat-suc-r (suc a) (suc b) = diffNat-suc-r a b

--- ...and thus so does _-NZ_

-NZ-suc-l : ∀ a b → suc a -NZ b ≡ sucInt (a -NZ b)
-NZ-suc-l a b = -NZ-spec (suc a) b ⟨≡⟩ diffNat-suc-l a b ⟨≡⟩ʳ sucInt $≡ -NZ-spec a b

-NZ-suc-r : ∀ a b → a -NZ suc b ≡ predInt (a -NZ b)
-NZ-suc-r a b = -NZ-spec a (suc b) ⟨≡⟩ diffNat-suc-r a b ⟨≡⟩ʳ predInt $≡ -NZ-spec a b

--- We need some lemmas about how sucInt and predInt relates to _+_.
--- These are special cases of the computation rules below, so we make them private.

private
  sucInt-spec : ∀ a → 1 + a ≡ sucInt a
  sucInt-spec (pos n)          = refl
  sucInt-spec (negsuc zero)    = refl
  sucInt-spec (negsuc (suc n)) = refl

  predInt-spec : ∀ a → -1 + a ≡ predInt a
  predInt-spec (pos zero)    = refl
  predInt-spec (pos (suc n)) = -NZ-spec (suc n) 1
  predInt-spec (negsuc n)    = refl

  addInt-suc : ∀ a b → pos (suc a) + b ≡ sucInt (pos a + b)
  addInt-suc a (pos    b) = refl
  addInt-suc a (negsuc b) = -NZ-suc-l a (suc b)

  addInt-negsuc : ∀ a b → negsuc (suc a) + b ≡ predInt (negsuc a + b)
  addInt-negsuc a (pos b)    = -NZ-suc-r b (suc a)
  addInt-negsuc a (negsuc b) = refl

--- Now we can prove some "computation" rules for _+_

addInt-zero-l : (a : Int) → 0 + a ≡ a
addInt-zero-l (pos a)    = refl
addInt-zero-l (negsuc a) = -NZ-spec 0 (suc a)

addInt-zero-r : (a : Int) → a + 0 ≡ a
addInt-zero-r (pos a)    = pos $≡ add-zero-r a
addInt-zero-r (negsuc a) = -NZ-spec 0 (suc a)

addInt-sucInt-l : ∀ a b → sucInt a + b ≡ sucInt (a + b)
addInt-sucInt-l (pos a)          b = addInt-suc a b
addInt-sucInt-l (negsuc zero)    b = addInt-zero-l b ⟨≡⟩ʳ sucInt $≡ predInt-spec b ⟨≡⟩ sucInt-predInt b
addInt-sucInt-l (negsuc (suc a)) b = sucInt-predInt (negsuc a + b) ʳ⟨≡⟩ʳ sucInt $≡ addInt-negsuc a b

addInt-predInt-l : ∀ a b → predInt a + b ≡ predInt (a + b)
addInt-predInt-l (pos zero)    b = predInt-spec b ⟨≡⟩ʳ predInt $≡ addInt-zero-l b
addInt-predInt-l (pos (suc a)) b = predInt-sucInt (pos a + b) ʳ⟨≡⟩ʳ predInt $≡ addInt-suc a b
addInt-predInt-l (negsuc a)    b = addInt-negsuc a b

--- Adding a non-negative number is equivalent to sucsInt and adding a negative number
--- to predsInt.

addInt-pos : ∀ a b → pos a + b ≡ sucsInt a b
addInt-pos zero    b = addInt-zero-l b
addInt-pos (suc a) b = addInt-suc a b ⟨≡⟩ sucInt $≡ addInt-pos a b

addInt-neg : ∀ a b → neg a + b ≡ predsInt a b
addInt-neg zero          b = addInt-zero-l b
addInt-neg (suc zero)    b = addInt-predInt-l 0 b ⟨≡⟩ predInt $≡ addInt-zero-l b -- predInt-spec b
addInt-neg (suc (suc a)) b = addInt-predInt-l (negsuc a) b ⟨≡⟩ predInt $≡ addInt-neg (suc a) b

--- sucsInt and predsInt have the appropriate associativity properties

private
  sucsInt-assoc : ∀ a b c → sucsInt a (b + c) ≡ sucsInt a b + c
  sucsInt-assoc zero    b c = refl
  sucsInt-assoc (suc a) b c = sucInt $≡ sucsInt-assoc a b c ⟨≡⟩ʳ
                              addInt-sucInt-l (sucsInt a b) c

  predsInt-assoc : ∀ a b c → predsInt a (b + c) ≡ predsInt a b + c
  predsInt-assoc zero    b c = refl
  predsInt-assoc (suc a) b c = predInt $≡ predsInt-assoc a b c ⟨≡⟩ʳ
                               addInt-predInt-l (predsInt a b) c

--- Finally we can prove associativity of _+_

addInt-assoc : (a b c : Int) → a + (b + c) ≡ (a + b) + c
addInt-assoc (pos    a) b c = addInt-pos a (b + c)       ⟨≡⟩ sucsInt-assoc a b c        ⟨≡⟩ʳ _+ c $≡ addInt-pos a b
addInt-assoc (negsuc a) b c = addInt-neg (suc a) (b + c) ⟨≡⟩ predsInt-assoc (suc a) b c ⟨≡⟩ʳ _+ c $≡ addInt-neg (suc a) b

--- Injectivity of _+_

private
  sucsInt-inj : ∀ a b c → sucsInt a b ≡ sucsInt a c → b ≡ c
  sucsInt-inj zero    b c eq = eq
  sucsInt-inj (suc a) b c eq = sucsInt-inj a b c (sucInt-inj _ _ eq)

  predsInt-inj : ∀ a b c → predsInt a b ≡ predsInt a c → b ≡ c
  predsInt-inj zero    b c eq = eq
  predsInt-inj (suc a) b c eq = predsInt-inj a b c (predInt-inj _ _ eq)

addInt-inj₂ : (a b c : Int) → a + b ≡ a + c → b ≡ c
addInt-inj₂ (pos a)    b c eq = sucsInt-inj  a b c                  (addInt-pos a b       ʳ⟨≡⟩ eq ⟨≡⟩ addInt-pos a c)
addInt-inj₂ (negsuc a) b c eq = predsInt-inj a b c (predInt-inj _ _ (addInt-neg (suc a) b ʳ⟨≡⟩ eq ⟨≡⟩ addInt-neg (suc a) c))

addInt-inj₁ : (a b c : Int) → a + c ≡ b + c → a ≡ b
addInt-inj₁ a b c eq = addInt-inj₂ c a b (addInt-commute c a ⟨≡⟩ eq ⟨≡⟩ addInt-commute b c)

--- Properties of negate ---

negate-idempotent : (a : Int) → negate (negate a) ≡ a
negate-idempotent (pos zero)    = refl
negate-idempotent (pos (suc n)) = refl
negate-idempotent (negsuc n)    = refl

private
  neg-add : ∀ a b → neg (a + b) ≡ neg a + neg b
  neg-add zero    b       = sym (addInt-zero-l (neg b))
  neg-add (suc a) zero    = negsuc $≡ add-zero-r a ⟨≡⟩ʳ -NZ-spec 0 (suc a)
  neg-add (suc a) (suc b) = negsuc $≡ add-suc-r a b

  negate-diffNat : ∀ a b → negate (diffNat a b) ≡ diffNat b a
  negate-diffNat zero    zero    = refl
  negate-diffNat zero    (suc b) = refl
  negate-diffNat (suc a) zero    = refl
  negate-diffNat (suc a) (suc b) = negate-diffNat a b

negate-NZ : ∀ a b → negate (a -NZ b) ≡ b -NZ a
negate-NZ a b = negate $≡ -NZ-spec a b ⟨≡⟩ negate-diffNat a b ⟨≡⟩ʳ -NZ-spec b a

negate-addInt : (a b : Int) → negate (a + b) ≡ negate a + negate b
negate-addInt (pos a)       (pos b)       = neg-add a b
negate-addInt (pos zero)    (negsuc b)    = refl
negate-addInt (pos (suc a)) (negsuc b)    = negate-NZ (suc a) (suc b)
negate-addInt (negsuc a)    (pos zero)    = pos ∘ suc $≡ sym (add-zero-r a)
negate-addInt (negsuc a)    (pos (suc b)) = negate-NZ (suc b) (suc a)
negate-addInt (negsuc a)    (negsuc b)    = pos $≡ sym (add-suc-r (suc a) b)

negate-subInt : (a b : Int) → negate (a - b) ≡ b - a
negate-subInt a b = negate-addInt a (negate b) ⟨≡⟩
                    negate a +_ $≡ negate-idempotent b ⟨≡⟩
                    addInt-commute (negate a) b

--- Properties of subtraction ---

private
  diffNat-equal : ∀ a → diffNat a a ≡ 0
  diffNat-equal zero = refl
  diffNat-equal (suc a) = diffNat-equal a

subInt-equal : (a b : Int) → a ≡ b → a - b ≡ 0
subInt-equal (pos zero)    _ refl = refl
subInt-equal (pos (suc n)) _ refl = -NZ-spec (suc n) (suc n) ⟨≡⟩ diffNat-equal n
subInt-equal (negsuc n)    _ refl = -NZ-spec (suc n) (suc n) ⟨≡⟩ diffNat-equal n

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
module Luau.Type where

open import FFI.Data.Maybe using (Maybe; just; nothing)

data Type : Set where
  nil : Type
  _⇒_ : Type → Type → Type
  none : Type
  any : Type
  number : Type
  _∪_ : Type → Type → Type
  _∩_ : Type → Type → Type

src : Type → Type
src nil = none
src (S ⇒ T) = S
src none = none
src any = any
src number = none
src (S ∪ T) = (src S) ∪ (src T)
src (S ∩ T) = (src S) ∩ (src T)

tgt : Type → Type
tgt nil = none
tgt (S ⇒ T) = T
tgt none = none
tgt any = any
tgt number = none
tgt (S ∪ T) = (tgt S) ∪ (tgt T)
tgt (S ∩ T) = (tgt S) ∩ (tgt T)

optional : Type → Type
optional nil = nil
optional (T ∪ nil) = (T ∪ nil)
optional T = (T ∪ nil)

normalizeOptional : Type → Type
normalizeOptional (S ∪ T) with normalizeOptional S | normalizeOptional T
normalizeOptional (S ∪ T) | (S′ ∪ nil) | (T′ ∪ nil) = (S′ ∪ T′) ∪ nil
normalizeOptional (S ∪ T) | S′         | (T′ ∪ nil) = (S′ ∪ T′) ∪ nil
normalizeOptional (S ∪ T) | (S′ ∪ nil) | T′         = (S′ ∪ T′) ∪ nil
normalizeOptional (S ∪ T) | S′         | nil        = optional S′
normalizeOptional (S ∪ T) | nil        | T′         = optional T′
normalizeOptional (S ∪ T) | S′         | T′         = S′ ∪ T′
normalizeOptional T = T


text:
  module NumeralNaturalProofs where
    open NumeralNatural
    open Structure
    open Structure.Function'.Properties
    open Structure.Relator
    open Structure.Relator.Properties

    [∩]-inductive : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ (Inductive(a) ∧ Inductive(b)) ⟶ Inductive(a ∩ b))))
    [∩]-inductive =
      ([∀].intro (\{a} →
        ([∀].intro (\{b} →
          ([→].intro(indaindb ↦
            ([∧].intro
              -- ∅ is in
              ([↔].elimₗ
                ([∀].elim([∀].elim([∀].elim([∩]-membership){a}){b}){∅})
                ([∧].intro
                  ([∧].elimₗ([∧].elimₗ indaindb))
                  ([∧].elimₗ([∧].elimᵣ indaindb))
                )
              )

              -- 𝐒 is in
              ([∀].intro (\{x} →
                ([→].intro(x∈a∩b ↦
                  ([↔].elimₗ
                    ([∀].elim([∀].elim([∀].elim([∩]-membership){a}){b}){𝐒(x)})
                    ([∧].intro
                      -- 𝐒(x) ∈ a
                      ([→].elim([∀].elim([∧].elimᵣ([∧].elimₗ indaindb)){x})(
                        -- x ∈ a
                        [∧].elimₗ([↔].elimᵣ
                          ([∀].elim([∀].elim([∀].elim([∩]-membership){a}){b}){x})
                          (x∈a∩b)
                        )
                      ))

                      -- 𝐒(x) ∈ b
                      ([→].elim([∀].elim([∧].elimᵣ([∧].elimᵣ indaindb)){x})(
                        -- x ∈ b
                        [∧].elimᵣ([↔].elimᵣ
                          ([∀].elim([∀].elim([∀].elim([∩]-membership){a}){b}){x})
                          (x∈a∩b)
                        )
                      ))
                    )
                  )
                ))
              ))
            )
          ))
        ))
      ))

    -- postulate [⋂]-property : ∀{φ} → Proof(∀ₗ(s ↦ ∀ₗ(x ↦ (x ∈ s) ⟶ φ(x)) ⟶ φ(⋂ s))) TODO: MAybe not true
    [⋂]-inductive : Proof(∀ₗ(s ↦ ∀ₗ(x ↦ (x ∈ s) ⟶ Inductive(x)) ⟶ Inductive(⋂ s)))
    [⋂]-inductive =
      ([∀].intro (\{s} →
        ([→].intro(allxxsindx ↦
          ([∧].intro
            -- ∅ is in
            proof

            -- 𝐒 is in
            proof
          )
        ))
      ))
      where postulate proof : ∀{a} → a

    [ℕ]-inductive : Proof(Inductive(ℕ))
    [ℕ]-inductive =
      ([→].elim
        ([∀].elim
          [⋂]-inductive
          {filter(℘(inductiveSet)) Inductive}
        )
        ([∀].intro(\{x} →
          ([→].intro(x∈filter ↦
            [∧].elimᵣ(([↔].elimᵣ([∀].elim([∀].elim filter-membership{℘(inductiveSet)}){x})) (x∈filter))
          ))
        ))
      )

    module _ where
      open FunctionSet
      open FunctionProofs

      postulate [ℕ]-recursive-function : ∀{z : Domain}{s : Domain → Domain → Domain} → Proof(∃ₛ!(ℕ →ₛₑₜ ℕ)(f ↦ ((𝟎 , z) ∈ f) ∧ (∀ₗ(n ↦ ∀ₗ(fn ↦ ((n , fn) ∈ f) ⟶ ((𝐒(n) , s(n)(fn)) ∈ f))))))

      [ℕ]-recursive-function-witness : Domain → BinaryOperator → Function
      [ℕ]-recursive-function-witness z s = [→ₛₑₜ]-witness([∃ₛ!]-witness ⦃ f ⦄ ) ⦃ [∃ₛ!]-domain ⦃ f ⦄ ⦄ where
        f = [ℕ]-recursive-function{z}{s}

      postulate [ℕ]-recursive-function-of-zero : ∀{z : Domain}{s : Domain → Domain → Domain} → Proof(([ℕ]-recursive-function-witness z s)(𝟎) ≡ z)
      postulate [ℕ]-recursive-function-of-successor : ∀{z : Domain}{s : Domain → Domain → Domain} → Proof(∀ₛ(ℕ) (n ↦ ([ℕ]-recursive-function-witness z s)(𝐒(n)) ≡ s(n)(([ℕ]-recursive-function-witness z s)(n))))

      _+_ : Domain → Domain → Domain
      _+_ a b = [ℕ]-recursive-function-witness z s b where
        z : Domain
        z = a

        s : Domain → Domain → Domain
        s(n)(sn) = 𝐒(sn)

      _⋅_ : Domain → Domain → Domain
      _⋅_ a b = [ℕ]-recursive-function-witness z s b where
        z : Domain
        z = 𝟎

        s : Domain → Domain → Domain
        s(n)(sn) = sn + a

      _^'_ : Domain → Domain → Domain -- TODO: Temporary name collision fix
      _^'_ a b = [ℕ]-recursive-function-witness z s b where
        z : Domain
        z = 𝐒(𝟎)

        s : Domain → Domain → Domain
        s(n)(sn) = sn ⋅ a

      module _ where
        open Structure.Operator.Properties

        postulate [+]-commutativity : Proof(Commutativity(ℕ)(_+_))
        postulate [+]-associativity : Proof(Associativity(ℕ)(_+_))
        postulate [+]-identity : Proof(Identity(ℕ)(_+_)(𝟎))

        postulate [⋅]-commutativity : Proof(Commutativity(ℕ)(_⋅_))
        postulate [⋅]-associativity : Proof(Associativity(ℕ)(_⋅_))
        postulate [⋅]-identity : Proof(Identity(ℕ)(_⋅_)(𝐒(𝟎)))

        postulate [⋅][+]-distributivity : Proof(Distributivity(ℕ)(_⋅_)(_+_))

    postulate [ℕ]-elements : Proof(∀ₛ(ℕ)(n ↦ (n ≡ 𝟎) ∨ ∃ₛ(ℕ)(p ↦ n ≡ 𝐒(p))))

    postulate [<]-irreflexivity : Proof(Irreflexivity(ℕ)(_<_))
    postulate [<]-asymmetry     : Proof(Antisymmetry(ℕ)(_<_))
    postulate [<]-transitivity  : Proof(Transitivity(ℕ)(_<_))

    postulate [≤]-reflexivity  : Proof(Irreflexivity(ℕ)(_≤_))
    postulate [≤]-antisymmetry : Proof(Antisymmetry(ℕ)(_≤_))
    postulate [≤]-transitivity : Proof(Transitivity(ℕ)(_≤_))

    -- instance
    --   [𝐒]-type : Function.Type(𝐒)
    --   [𝐒]-type = Function.Type.intro ℕ ℕ proof where
    --     postulate proof : ∀{a} → a

    -- postulate [𝐒]-injective : Proof(Injective(ℕ)(𝐒))

    -- ∀ₛ(ℕ)(a ↦ ∀ₛ(ℕ)(b ↦ (a < b) ⟶ (𝐒(a) < 𝐒(b))))
    -- ∀ₛ(ℕ)(n ↦ 𝟎 ≢ 𝐒(n))

  -- A model of the integers expressed in set theory (using only sets).
  module NumeralInteger where
    open Structure.Function'.Properties
    open Structure.Relator.Properties
    private
      module Nat where
        open NumeralNatural ⦃ signature ⦄ public
        open NumeralNaturalProofs public

    EqualDistance : Domain → Domain → Formula
    EqualDistance x y = ∃ₗ(x₁ ↦ ∃ₗ(x₂ ↦ (x ≡ (x₁ , x₂)) ∧ ∃ₗ(y₁ ↦ ∃ₗ(y₂ ↦ (y ≡ (y₁ , y₂)) ∧ ((x₁ Nat.+ y₂) ≡ (x₂ Nat.+ y₁))))))

    postulate EqualDistance-equivalence : Proof(Equivalence(Nat.ℕ ⨯ Nat.ℕ)(EqualDistance))

    ℤ : Domain
    ℤ = (Nat.ℕ ⨯ Nat.ℕ) / EqualDistance

    nat : Domain → Domain
    nat(n) = map(N ↦ (N , (N Nat.+ n))) Nat.ℕ

    postulate nat-type : Proof(Type(Nat.ℕ)(ℤ)(nat))

    𝟎 : Domain
    𝟎 = nat(Nat.𝟎)

    postulate _<_ : Domain → Domain → Formula -- TODO

    _≤_ : Domain → Domain → Formula
    a ≤ b = (a < b) ∨ (a ≡ b)

    _>_ : Domain → Domain → Formula
    _>_ = swap _<_

    _≥_ : Domain → Domain → Formula
    _≥_ = swap _≤_

    ℕ : Domain
    ℕ = filter(ℤ) (_≥ 𝟎)

    ℤ₊ : Domain
    ℤ₊ = filter(ℤ) (_> 𝟎)

    ℤ₋ : Domain
    ℤ₋ = filter(ℤ) (_< 𝟎)

    postulate 𝐒 : Domain → Domain -- TODO

    postulate 𝐏 : Domain → Domain -- TODO

    postulate _+_ : Domain → Domain → Domain -- TODO

    postulate −_ : Domain → Domain -- TODO

    _−_ : Domain → Domain → Domain
    a − b = a + (− b)

    postulate _⋅_ : Domain → Domain → Domain -- TODO

  -- A model of the rational numbers expressed in set theory (using only sets).
  module NumeralRational where
    open Structure.Function'.Properties
    open Structure.Relator.Properties
    private module Nat = NumeralNatural
    private module Int = NumeralInteger
    open Structure.Ordering.Strict

    EqualRatio : Domain → Domain → Formula
    EqualRatio x y = ∃ₗ(x₁ ↦ ∃ₗ(x₂ ↦ (x ≡ (x₁ , x₂)) ∧ ∃ₗ(y₁ ↦ ∃ₗ(y₂ ↦ (y ≡ (y₁ , y₂)) ∧ ((x₁ Int.⋅ y₂) ≡ (x₂ Int.⋅ y₁))))))

    postulate EqualRatio-equivalence : Proof(Equivalence(Int.ℤ ⨯ Int.ℤ₊)(EqualRatio))

    ℚ : Domain
    ℚ = (Int.ℤ ⨯ Int.ℤ₊) / EqualRatio

    postulate int : Domain → Domain -- TODO
    -- int(n) = map(N ↦ (N , (N Int.⋅ n))) Int.ℤ

    postulate int-type : Proof(Type(Int.ℤ)(ℚ)(int))

    nat : Domain → Domain
    nat(n) = int(Int.nat(n))

    postulate nat-type : Proof(Type(Nat.ℕ)(ℚ)(nat))

    𝟎 : Domain
    𝟎 = nat(Nat.𝟎)

    -- TODO: These are incorrect because elements in ℚ are sets of tuples
    _≤_ : Domain → Domain → Formula
    _≤_ x y = ∃ₗ(x₁ ↦ ∃ₗ(x₂ ↦ (x ≡ (x₁ , x₂)) ∧ ∃ₗ(y₁ ↦ ∃ₗ(y₂ ↦ (y ≡ (y₁ , y₂)) ∧ ((x₁ Int.⋅ y₂) Int.≤ (x₂ Int.⋅ y₁))))))

    _<_ : Domain → Domain → Formula
    _<_ x y = ∃ₗ(x₁ ↦ ∃ₗ(x₂ ↦ (x ≡ (x₁ , x₂)) ∧ ∃ₗ(y₁ ↦ ∃ₗ(y₂ ↦ (y ≡ (y₁ , y₂)) ∧ ((x₁ Int.⋅ y₂) Int.< (x₂ Int.⋅ y₁))))))

    _>_ : Domain → Domain → Formula
    _>_ = swap _<_

    _≥_ : Domain → Domain → Formula
    _≥_ = swap _≤_

    postulate [<]-dense : Proof(Dense(ℚ)(_<_)) -- TODO

    postulate _+_ : Domain → Domain → Domain -- TODO

    postulate −_ : Domain → Domain -- TODO

    _−_ : Domain → Domain → Domain
    a − b = a + (− b)

    postulate _⋅_ : Domain → Domain → Domain -- TODO

    postulate ⅟_ : Domain → Domain -- TODO

    _/'_ : Domain → Domain → Domain
    a /' b = a ⋅ (⅟ b)

    postulate abs : Domain → Domain

    _𝄩_ : Domain → Domain → Domain
    a 𝄩 b = abs(a − b)

  -- A model of the real numbers expressed in set theory (using only sets).
  module NumeralReal where
    private module Rat = NumeralRational

-- TODO: https://math.stackexchange.com/questions/1076806/proof-that-the-floor-and-ceiling-functions-exist

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Cats.Category.Sets where

open import Data.Product using (Σ ; _×_ ; proj₁ ; proj₂)
open import Level
open import Relation.Binary using (Rel ; IsEquivalence ; _Preserves₂_⟶_⟶_)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

open import Cats.Category.Base
open import Cats.Util.Function
open import Cats.Util.Logic.Constructive

module _ {l} {A B : Set l} where

  infixr 4 _≈_

  _≈_ : (f g : A → B) → Set l
  f ≈ g = ∀ x → f x ≡ g x

  equiv : IsEquivalence _≈_
  equiv = record
      { refl = λ x → ≡.refl
      ; sym = λ eq x → ≡.sym (eq x)
      ; trans = λ eq₁ eq₂ x → ≡.trans (eq₁ x) (eq₂ x)
      }

instance Sets : ∀ l → Category (suc l) l l
Sets l = record
    { Obj = Set l
    ; _⇒_ = λ A B → A → B
    ; _≈_ = _≈_
    ; id = id
    ; _∘_ = _∘_
    ; equiv = equiv
    ; ∘-resp = λ {_} {_} {_} {f} eq₁ eq₂ x
        → ≡.trans (≡.cong f (eq₂ _)) (eq₁ _)
    ; id-r = λ _ → ≡.refl
    ; id-l = λ _ → ≡.refl
    ; assoc = λ _ → ≡.refl
    }

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
module Bughunting2 where

data Nat : Set where zero : Nat -- Comment which gets eaten
                     suc  : Nat -> Nat --Comment which is preserved

plus  :
 Nat ->  Nat -> Nat

plus2 : Nat -> Nat -> Nat
plus2 = plus

plus zero  m = m
plus m n = {!   !}


text:
module Categories.WithFamilies where

open import Level
import Relation.Binary.HeterogeneousEquality as Het
open Het using (_≅_)

open import Categories.Support.PropositionalEquality
open import Categories.Support.Experimental

open import Categories.Category
open import Categories.Functor
open import Categories.NaturalIsomorphism
open import Categories.Object.Terminal

open import Categories.Fam

module UnpackFam {o ℓ e a b} (C : Category o ℓ e)
                 (T : Functor (Category.op C) (Fam a b)) where
  private module C = Category C
  private module T = Functor T

  Context = C.Obj

  Ty : C.Obj → Set a
  Ty Γ = Fam.U (T.F₀ Γ)

  _[_] : ∀ {Γ Δ} → Ty Γ → Δ C.⇒ Γ → Ty Δ
  _[_] A f = Fam.Hom.f (T.F₁ f) A

  Tm : ∀ Γ → Ty Γ → Set b
  Tm Γ = Fam.T (T.F₀ Γ)

  _[_⁺] : ∀ {Γ Δ A} → Tm Γ A → (f : Δ C.⇒ Γ) → Tm Δ (A [ f ])
  _[_⁺] M f = Fam.Hom.φ (T.F₁ f) _ M

record CwF {o ℓ e a b} : Set (suc e ⊔ (suc ℓ ⊔ suc o) ⊔ suc a ⊔ suc b) where
  field
    C : Category o ℓ e
    T : Functor (Category.op C) (Fam a b)
    Empty : Terminal C

  module C = Category C
  module T = Functor T
  open UnpackFam C T
  module Empty = Terminal C Empty

  field
    -- context snoc
    _>_ : ∀ Γ → Ty Γ → C.Obj
    -- projections
    p : ∀ {Γ A} → (Γ > A) C.⇒ Γ
    v : ∀ {Γ A} → Tm (Γ > A) (A [ p ])
    -- constructor
    <_,_>         : ∀ {Γ A} → ∀ {Δ} (γ : Δ C.⇒ Γ) (a : Tm Δ (A [ γ ])) → Δ C.⇒ (Γ > A)
    .p∘<γ,a>≡γ    : ∀ {Γ A} → ∀ {Δ} {γ : Δ C.⇒ Γ} {a : Tm Δ (A [ γ ])} → p C.∘ < γ , a > C.≡ γ
    .v[<γ,a>]≡a   : ∀ {Γ A} → ∀ {Δ} {γ : Δ C.⇒ Γ} {a : Tm Δ (A [ γ ])} → v [ < γ , a > ⁺] ≅ a
    .<γ,a>-unique : ∀ {Γ A} → ∀ {Δ} {γ : Δ C.⇒ Γ} {a : Tm Δ (A [ γ ])} →
                      (δ : Δ C.⇒ (Γ > A)) → .(p C.∘ δ C.≡ γ) → .(v [ δ ⁺] ≅ a) → δ C.≡ < γ , a >

  v[_] : ∀ {Γ A Δ} → (γ : Δ C.⇒ Γ) -> Tm (Δ > A [ γ ]) (A [ γ C.∘ p ])
  v[_] {Γ} {A} {Δ} γ = ≣-subst′ (Tm (Δ > A [ γ ])) (≣-sym (Fam.Eq.f≡g (T.homomorphism {Γ}) {A})) (v {Δ} {A [ γ ]})

  _[id] : ∀ {Γ A} -> Tm Γ A -> Tm Γ (A [ C.id ])
  _[id] {Γ} {A} x = ≣-subst′ (Tm Γ) (≣-sym (Fam.Eq.f≡g (T.identity {Γ}) {A})) x

  open UnpackFam C T public
  open Empty public using () renaming (⊤ to <>)

record Pi {o ℓ e a b} (Cwf : CwF {o} {ℓ} {e} {a} {b}) : Set (o ⊔ ℓ ⊔ a ⊔ b) where
  open CwF Cwf
  field
    Π : ∀ {Γ} -> (A : Ty Γ) (B : Ty (Γ > A)) -> Ty Γ
    lam : ∀ {Γ} {A : Ty Γ} {B : Ty (Γ > A)} -> (b : Tm (Γ > A) B) -> Tm Γ (Π A B)
    _$_ : ∀ {Γ} {A : Ty Γ} {B : Ty (Γ > A)} ->
            (f : Tm Γ (Π A B)) (x : Tm Γ A) -> Tm Γ (B [ < C.id , x [id] > ])

    -- naturality laws
    .Π-nat   : ∀ {Γ} -> (A : Ty Γ) (B : Ty (Γ > A)) -> ∀ {Δ} (γ : Δ C.⇒ Γ)
                     -> Π A B [ γ ] ≣ Π (A [ γ ]) (B [ < (γ C.∘ p) , v[ γ ] > ])
    .lam-nat : ∀ {Γ} {A : Ty Γ} {B : Ty (Γ > A)} -> (b : Tm (Γ > A) B) -> ∀ {Δ} (γ : Δ C.⇒ Γ)
                     -> lam b [ γ ⁺] ≅ lam {A = A [ γ ]} (b [ < γ C.∘ p , v[ γ ] > ⁺])
    .app-nat : ∀ {Γ} {A : Ty Γ} {B : Ty (Γ > A)} -> (f : Tm Γ (Π A B)) (x : Tm Γ A) -> ∀ {Δ} (γ : Δ C.⇒ Γ)
                     -> (f $ x) [ γ ⁺] ≅ ≣-subst′ (Tm Δ) (Π-nat A B γ) (f [ γ ⁺]) $ (x [ γ ⁺])

    -- proofs of the lam/_$_ isomorphism
    .β : ∀ {Γ} {A : Ty Γ} {B : Ty (Γ > A)} -> (b : Tm (Γ > A) B) (x : Tm Γ A)
           -> (lam b $ x) ≣ b [ < C.id , x [id] > ⁺]

    .η : ∀ {Γ} {A : Ty Γ} {B : Ty (Γ > A)} -> (f : Tm Γ (Π A B))
           -> lam (≣-subst′ (Tm (Γ > A)) (Π-nat A B p) (f [ p ⁺]) $ v) ≅ f

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

module Categories.Category.Concrete where

open import Level

open import Categories.Category.Core using (Category)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Functor.Core using (Functor)
open import Categories.Functor.Representable using (Representable)
open import Categories.Functor.Properties using (Faithful)

-- A Concrete Category is a category along with a faithful
-- functor to Setoid.
-- [Normally Set, but that doesn't work so well here]

private
  variable
    o ℓ e : Level

record Concrete (C : Category o ℓ e) (ℓ′ e′ : Level) : Set (o ⊔ ℓ ⊔ e ⊔ suc (ℓ′ ⊔ e′)) where
  field
    concretize : Functor C (Setoids ℓ′ e′)
    conc-faithful : Faithful concretize

-- Because of the use of the Hom functor, some levels collapse
record RepresentablyConcrete (C : Category o ℓ e) : Set (o ⊔ suc (e ⊔ ℓ)) where
  open Concrete
  field
    conc : Concrete C ℓ e
    representable : Representable (concretize conc)

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:
{- Name: Bowornmet (Ben) Hudson

--Complexity : "Playing The Game"--

-}

open import Preliminaries
open import Preorder-withmax

module Complexity-lang where

  data Typ : Set where
    nat : Typ
    _×'_ : Typ → Typ → Typ
    _⇒_ : Typ → Typ → Typ
    unit : Typ

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

  -- represent a context as a list of types
  Ctx = List Typ

  -- de Bruijn indices (for free variables)
  data _∈_ : Typ → Ctx → Set where
    i0 : ∀ {Γ T}
       → T ∈ (T :: Γ)
    iS : ∀ {Γ T T1}
       → T ∈ Γ
       → T ∈ (T1 :: Γ)

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

  -- some syntax
  data _|-_ : Ctx → Typ → Set where
    var : ∀ {Γ T}
        → (x : T ∈ Γ) → Γ |- T
    z : ∀ {Γ}
      → Γ |- nat
    suc : ∀ {Γ}
        → (e : Γ |- nat)
        → Γ |- nat
    rec : ∀ {Γ T}
        → (e : Γ |- nat)
        → (e0 : Γ |- T)
        → (e1 : (nat :: (T :: Γ)) |- T)
        → Γ |- T
    lam : ∀ {Γ T Ρ}
        → (x : (Ρ :: Γ) |- T)
        → Γ |- (Ρ ⇒ T)
    app : ∀ {Γ T1 T2}
        → (e1 : Γ |- (T2 ⇒ T1)) → (e2 : Γ |- T2)
        → Γ |- T1
    unit : ∀ {Γ}
         → Γ |- unit
    prod : ∀ {Γ T1 T2}
         → (e1 : Γ |- T1) → (e2 : Γ |- T2)
         → Γ |- (T1 ×' T2)
    l-proj : ∀ {Γ T1 T2}
           → (e : Γ |- (T1 ×' T2))
           → Γ |- T1
    r-proj : ∀ {Γ T1 T2}
           → (e : Γ |- (T1 ×' T2))
           → Γ |- T2

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

  -- renaming function
  rctx : Ctx → Ctx → Set
  rctx Γ Γ' = ∀ {τ} → τ ∈ Γ' → τ ∈ Γ

  lem1 : ∀ {Γ Γ' τ} → rctx Γ Γ' → rctx (τ :: Γ) (τ :: Γ')
  lem1 d i0 = i0
  lem1 d (iS x) = iS (d x)

  ren : ∀ {Γ Γ' τ} → Γ' |- τ → rctx Γ Γ' → Γ |- τ
  ren (var x) d = var (d x)
  ren z d = z
  ren (suc e) d = suc (ren e d)
  ren (rec e0 e1 e2) d = rec (ren e0 d) (ren e1 d) (ren e2 (lem1 (lem1 d)))
  ren (lam x) d = lam (ren x (lem1 d))
  ren (app e1 e2) d = app (ren e1 d) (ren e2 d)
  ren unit d = unit
  ren (prod e1 e2) d = prod (ren e1 d) (ren e2 d)
  ren (l-proj e) d = l-proj (ren e d)
  ren (r-proj e) d = r-proj (ren e d)

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

  -- substitution
  sctx : Ctx → Ctx → Set
  sctx Γ Γ' = ∀ {τ} → τ ∈ Γ' → Γ |- τ

  -- weakening
  wkn : ∀ {Γ τ1 τ2} → Γ |- τ2 → (τ1 :: Γ) |- τ2
  wkn e = ren e iS

  -- lemmas everywhere
  wkn-s : ∀ {Γ τ1 Γ'} → sctx Γ Γ' → sctx (τ1 :: Γ) Γ'
  wkn-s d = λ f → wkn (d f)

  wkn-r : ∀ {Γ τ1 Γ'} → rctx Γ Γ' → rctx (τ1 :: Γ) Γ'
  wkn-r d = λ x → iS (d x)

  lem2 : ∀ {Γ Γ' τ} → sctx Γ Γ' → sctx (τ :: Γ) (τ :: Γ')
  lem2 d i0 = var i0
  lem2 d (iS i) = wkn (d i)

  lem3 : ∀ {Γ τ} → Γ |- τ → sctx Γ (τ :: Γ)
  lem3 e i0 = e
  lem3 e (iS i) = var i

  lem4 : ∀ {Γ τ1 τ2} → Γ |- τ1 → Γ |- τ2 → sctx Γ (τ1 :: (τ2 :: Γ))
  lem4 e1 e2 i0 = e1
  lem4 e1 e2 (iS i0) = e2
  lem4 e1 e2 (iS (iS i)) = var i

  subst : ∀ {Γ Γ' τ} → sctx Γ Γ' → Γ' |- τ → Γ |- τ
  subst d (var x) = d x
  subst d z = z
  subst d (suc e) = suc (subst d e)
  subst d (rec e0 e1 e2) = rec (subst d e0) (subst d e1) (subst (lem2 (lem2 d)) e2)
  subst d (lam e) = lam (subst (lem2 d) e)
  subst d (app e1 e2) = app (subst d e1) (subst d e2)
  subst d unit = unit
  subst d (prod e1 e2) = prod (subst d e1) (subst d e2)
  subst d (l-proj e) = l-proj (subst d e)
  subst d (r-proj e) = r-proj (subst d e)

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

  -- define 'stepping' as a datatype (fig. 1 of proof)
  data _≤s_ : ∀ {Γ T} → Γ |- T → Γ |- T → Set where
    refl-s : ∀ {Γ T}
           → (e : Γ |- T)
           → e ≤s e
    trans-s : ∀ {Γ T}
            → (e e' e'' : Γ |- T)
            → e ≤s e' → e' ≤s e''
            → e ≤s e''
    cong-s : ∀ {Γ T T'}
           →  (e : (T :: Γ) |- T')
           → (e1 e2 : Γ |- T)
           → e1 ≤s e2
           → subst (lem3 e1) e ≤s subst (lem3 e2) e
    lam-s : ∀ {Γ T T'}
          → (e : (T :: Γ) |- T')
          → (e2 : Γ |- T)
          → subst (lem3 e2) e ≤s app (lam e) e2
    l-proj-s : ∀ {Γ T1 T2}
             → (e1 : Γ |- T1) → (e2 : Γ |- T2)
             → e1 ≤s (l-proj (prod e1 e2))
    r-proj-s : ∀ {Γ T1 T2}
             → (e1 : Γ |- T1) → (e2 : Γ |- T2)
             → e2 ≤s (r-proj (prod e1 e2))
    rec-steps-s : ∀ {Γ T}
                → (e : Γ |- nat)
                → (e0 : Γ |- T)
                → (e1 : (nat :: (T :: Γ)) |- T)
                → subst (lem4 e (rec e e0 e1)) e1 ≤s (rec (suc e) e0 e1)
    rec-steps-z : ∀ {Γ T}
                → (e0 : Γ |- T)
                → (e1 : (nat :: (T :: Γ)) |- T)
                → e0 ≤s (rec z e0 e1)

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

  el : PREORDER → Set
  el = fst

  PREORDER≤ : (PA : PREORDER) → el PA → el PA → Set
  PREORDER≤ PA = Preorder-max-str.≤ (snd PA)

  interp : Typ → PREORDER
  interp nat = Nat , nat-p
  interp (A ×' B) = interp A ×p interp B
  interp (A ⇒ B) = interp A ->p interp B
  interp unit = unit-p

  interpC : Ctx → PREORDER
  interpC [] = unit-p
  interpC (A :: Γ) = interpC Γ ×p interp A

  -- look up a variable in context
  lookup : ∀{Γ τ} → τ ∈ Γ → el (interpC Γ ->p interp τ)
  lookup (i0 {Γ} {τ}) = snd' {interpC (τ :: Γ)} {interpC Γ} {_} id
  lookup (iS {Γ} {τ} {τ1} x) = comp {interpC (τ1 :: Γ)} {_} {_} (fst' {interpC (τ1 :: Γ)} {_} {interp τ1} id) (lookup x)

  interpE : ∀{Γ τ} → Γ |- τ → el (interpC Γ ->p interp τ)
  interpE (var x) = lookup x
  interpE z = monotone (λ x → Z) (λ x y _ → <>)
  interpE (suc e) = {!!} --monotone (λ x → S {!!}) {!!}
  interpE (rec e0 e1 e2) = mnatrec {!!} (interpE e1) (λ x x₁ → {!!}) {!!} --mnatrec {!!} (λ x x₁ → interpE e1) {!!}
  interpE (lam e) = lam' (interpE e)
  interpE (app e1 e2) = app' (interpE e1) (interpE e2)
  interpE unit = monotone (λ _ → <>) (λ x y _ → <>)
  interpE (prod e1 e2) = pair' (interpE e1) (interpE e2)
  interpE (l-proj {Γ} {τ1} {τ2} e) = fst' {_} {_} {interp τ2} (interpE e)
  interpE (r-proj {Γ} {τ1} {τ2} e) = snd' {_} {interp τ1} {_} (interpE e)

  sound : ∀ {Γ τ} (e e' : Γ |- τ) → e ≤s e' → PREORDER≤ (interpC Γ ->p interp τ) (interpE e) (interpE e')
  sound {_} {τ} .e' e' (refl-s .e') k = Preorder-max-str.refl (snd (interp τ)) (Monotone.f (interpE e') k)
  sound {_} {τ} e e' (trans-s .e e'' .e' p p₁) k = Preorder-max-str.trans (snd (interp τ)) (Monotone.f (interpE e) k)
                                                     (Monotone.f (interpE e'') k) (Monotone.f (interpE e') k)
                                                     (sound e e'' p k) (sound e'' e' p₁ k)
  sound .(subst (lem3 e1) e) .(subst (lem3 e2) e) (cong-s e e1 e2 p) k = {!!}
  sound .(subst (lem3 e2) e) .(app (lam e) e2) (lam-s e e2) k = {!!}
  sound {_} {τ} e .(l-proj (prod e e2)) (l-proj-s .e e2) k = Preorder-max-str.refl (snd (interp τ)) (Monotone.f (interpE e) k)
  sound {_} {τ} e .(r-proj (prod e1 e)) (r-proj-s e1 .e) k = Preorder-max-str.refl (snd (interp τ)) (Monotone.f (interpE e) k)
  sound .(subst (lem4 e (rec e e0 e1)) e1) .(rec (suc e) e0 e1) (rec-steps-s e e0 e1) k = {!!}
  sound e .(rec z e e1) (rec-steps-z .e e1) k = {!!}

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
------------------------------------------------------------------------------
-- Well-founded induction on natural numbers
------------------------------------------------------------------------------

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

-- Adapted from
-- http://www.iis.sinica.edu.tw/~scm/2008/well-founded-recursion-and-accessibility/
-- and the Agda standard library 0.8.1.

module FOTC.Induction.WF where

open import Common.Relation.Unary

open import FOTC.Base

------------------------------------------------------------------------------
-- The accessibility predicate: x is accessible if everything which is
-- smaller than x is also accessible (inductively).
data Acc (P : D → Set)(_<_ : D → D → Set)(x : D) : Set where
 acc : (∀ {y} → P y → y < x → Acc P _<_ y) → Acc P _<_ x

accFold : {P Q : D → Set}(_<_ : D → D → Set) →
          (∀ {x} → Q x → (∀ {y} → Q y → y < x → P y) → P x) →
          ∀ {x} → Q x → Acc Q _<_ x → P x
accFold _<_ f Qx (acc h) = f Qx (λ Qy y<x → accFold _<_ f Qy (h Qy y<x))

-- The accessibility predicate encodes what it means to be
-- well-founded; if all elements are accessible, then _<_ is
-- well-founded.
WellFounded : {P : D → Set} → (D → D → Set) → Set
WellFounded {P} _<_ = ∀ {x} → P x → Acc P _<_ x

WellFoundedInduction : {P Q : D → Set}
                       {_<_ : D → D → Set} →
                       WellFounded _<_ →
                       (∀ {x} → Q x → (∀ {y} → Q y → y < x → P y) → P x) →
                       ∀ {x} → Q x → P x
WellFoundedInduction {_<_ = _<_} wf f Qx = accFold _<_ f Qx (wf Qx)

module Subrelation {P        : D → Set}
                   {_<_ _<'_ : D → D → Set}
                   (<⇒<'     : ∀ {x y} → P x → x < y → x <' y)
                   where

  accessible : Acc P _<'_ ⊆ Acc P _<_
  accessible (acc h) = acc (λ Py y<x → accessible (h Py (<⇒<' Py y<x)))

  well-founded : WellFounded _<'_ → WellFounded _<_
  well-founded wf = λ Px → accessible (wf Px)

module InverseImage {P Q : D → Set}
                    {_<_ : D → D → Set}
                    {f   : D → D}
                    (f-Q : ∀ {x} → P x → Q (f x))
                    where

  accessible : ∀ {x} → P x →
               Acc Q _<_ (f x) → Acc P (λ x' y' → f x' < f y') x
  accessible Px (acc h) =
    acc (λ {y} Py fy<fx → accessible Py (h (f-Q Py) fy<fx))

  wellFounded : WellFounded _<_ → WellFounded (λ x y → f x < f y)
  wellFounded wf = λ Px → accessible Px (wf (f-Q Px))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Golden.Constructor where

open import Agda.Builtin.Nat

f : (Nat -> Nat) -> Nat
f g = g zero

fsuc = suc
fzero = zero

one = f suc
a = fsuc fzero

max_stars_repo_name: agda/agda-ocaml

max_issues_repo_name: agda/agda-ocaml

max_forks_repo_name: agda/agda-ocaml


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

module Data.Product.NAry where

open import Data.Sigma
open import Prelude hiding (⊤; tt)
open import Data.Unit.UniversePolymorphic
open import Path.Reasoning

private
  variable
    n : ℕ
    ℓ : Level

Levels : ℕ → Type
Levels zero = ⊤
Levels (suc n) = Level × Levels n

private
  variable
    ls : Levels n

max-level : Levels n → Level
max-level {zero} _ = ℓzero
max-level {suc n} (x , xs) =
  x ℓ⊔ max-level xs

Types : ∀ n → (ls : Levels n) → Type (ℓsuc (max-level ls))
Types zero ls = ⊤
Types (suc n) (l , ls) = Type l × Types n ls

⦅_⦆⁺ :  Types (suc n) ls →
        Type (max-level ls)
⦅_⦆⁺ {n = zero } (X , Xs) = X
⦅_⦆⁺ {n = suc n} (X , Xs) = X × ⦅ Xs ⦆⁺

⦅_⦆ :  Types n ls →
       Type (max-level ls)
⦅_⦆ {n = zero} _ = ⊤
⦅_⦆ {n = suc n} = ⦅_⦆⁺ {n = n}

map-types : (fn : ∀ {ℓ} → Type ℓ → Type ℓ) → ∀ {n ls} → Types n ls → Types n ls
map-types fn {zero} xs = xs
map-types fn {suc n} (x , xs) = fn x , map-types fn xs

data ArgForm : Type where expl impl inst : ArgForm

infixr 0 _[_]→_
_[_]→_ : Type a → ArgForm → Type b → Type (a ℓ⊔ b)
A [ expl  ]→ B =         A    → B
A [ impl  ]→ B = {  _ :  A }  → B
A [ inst  ]→ B = ⦃  _ :  A ⦄  → B

[_$] : ∀ form → (A [ form ]→ B) ⇔ (A → B)
[ expl $] .fun f = f
[ impl $] .fun f x = f {x}
[ inst $] .fun f x = f ⦃ x ⦄
[ expl $] .inv f = f
[ impl $] .inv f {x} = f x
[ inst $] .inv f ⦃ x ⦄ = f x
[ expl $] .leftInv f = refl
[ impl $] .leftInv f = refl
[ inst $] .leftInv f = refl
[ expl $] .rightInv f = refl
[ impl $] .rightInv f = refl
[ inst $] .rightInv f = refl

infixr 0 pi-arr
pi-arr : (A : Type a) → ArgForm → (A → Type b) → Type (a ℓ⊔ b)
pi-arr A expl B = (x : A) → B x
pi-arr A impl B = {x : A} → B x
pi-arr A inst B = ⦃ x : A ⦄ → B x

syntax pi-arr a f (λ x → b ) = x ⦂ a Π[ f ]→ b
Π[_$] : ∀ {B : A → Type b} fr → (x ⦂ A Π[ fr ]→ B x) ⇔ ((x : A) → B x)
Π[ expl $] .fun f = f
Π[ impl $] .fun f x = f {x}
Π[ inst $] .fun f x = f ⦃ x ⦄
Π[ expl $] .inv f x = f x
Π[ impl $] .inv f {x} = f x
Π[ inst $] .inv f ⦃ x ⦄ = f x
Π[ expl $] .leftInv f = refl
Π[ impl $] .leftInv f = refl
Π[ inst $] .leftInv f = refl
Π[ expl $] .rightInv f = refl
Π[ impl $] .rightInv f = refl
Π[ inst $] .rightInv f = refl

infixr 0 ⦅_⦆[_]→_
⦅_⦆[_]→_ : Types n ls → ArgForm → Type ℓ → Type (max-level ls ℓ⊔ ℓ)
⦅_⦆[_]→_ {n = zero}  Xs fr Y = Y
⦅_⦆[_]→_ {n = suc n} (X , Xs) fr Y = X [ fr ]→ ⦅ Xs ⦆[ fr ]→ Y

infixr 0 pi-arrs-plus
pi-arrs-plus :
  (Xs : Types (suc n) ls) →
  ArgForm →
  (y : ⦅ Xs ⦆⁺ → Type ℓ) →
  Type (max-level ls ℓ⊔ ℓ)
pi-arrs-plus {n = zero   } (X , Xs) fr Y = x ⦂ X Π[ fr ]→ Y x
pi-arrs-plus {n = suc n  } (X , Xs) fr Y =
  x ⦂ X Π[ fr ]→ xs ⦂⦅ Xs ⦆⁺Π[ fr ]→ Y (x , xs)

syntax pi-arrs-plus Xs fr (λ xs → Y) = xs ⦂⦅ Xs ⦆⁺Π[ fr ]→ Y

pi-arrs : ∀ {n ls ℓ} → (Xs : Types n ls) → ArgForm → (y : ⦅ Xs ⦆ → Type ℓ) → Type (max-level ls ℓ⊔ ℓ)
pi-arrs {n = zero} xs fr Y = Y tt
pi-arrs {n = suc n} = pi-arrs-plus
syntax pi-arrs Xs fr (λ xs → Y) = xs ⦂⦅ Xs ⦆Π[ fr ]→ Y

[_^_$]⁺↓ : ∀ n {ls ℓ} f {Xs : Types (suc n) ls} {y : Type ℓ} → (⦅ Xs ⦆⁺ → y) → ⦅ Xs ⦆[ f ]→ y
[ zero  ^ fr $]⁺↓ f = [ fr $] .inv f
[ suc n ^ fr $]⁺↓ f = [ fr $] .inv ([ n ^ fr $]⁺↓ ∘ (f ∘_) ∘ _,_)

[_^_$]↓ : ∀ n {ls ℓ} f {xs : Types n ls} {y : Type ℓ} → (⦅ xs ⦆ → y) → ⦅ xs ⦆[ f ]→ y
[ zero  ^ fr $]↓ f = f tt
[ suc n ^ fr $]↓ f = [ n ^ fr $]⁺↓ f

[_^_$]⁺↑ : ∀ n {ls ℓ} f {xs : Types (suc n) ls} {y : Type ℓ} → (⦅ xs ⦆[ f ]→ y) → (⦅ xs ⦆⁺ → y)
[ zero  ^ fr $]⁺↑ f = [ fr $] .fun f
[ suc n ^ fr $]⁺↑ f = uncurry ([ n ^ fr $]⁺↑ ∘ [ fr $] .fun f)

[_^_$]↑ : ∀ n {ls ℓ} f {xs : Types n ls} {y : Type ℓ} → (⦅ xs ⦆[ f ]→ y) → (⦅ xs ⦆ → y)
[ zero ^ fr  $]↑ f _ = f
[ suc n ^ fr $]↑ f = [ n ^ fr $]⁺↑ f

leftInvCurry⁺ : ∀ n {ls ℓ} fr {Xs : Types (suc n) ls} {Y : Type ℓ}
              → (f : ⦅ Xs ⦆[ fr ]→ Y ) → [ n ^ fr $]⁺↓ ([ n ^ fr $]⁺↑ f) ≡ f
leftInvCurry⁺ zero fr f = [ fr $] .leftInv f
leftInvCurry⁺ (suc n) fr f =
  [ fr $] .inv ([ n ^ fr $]⁺↓ ∘ [ n ^ fr $]⁺↑ ∘ [ fr $] .fun f) ≡⟨ cong (λ r → [ fr $] .inv (r ∘ [ fr $] .fun f)) (funExt (leftInvCurry⁺ n fr)) ⟩
  [ fr $] .inv ([ fr $] .fun f) ≡⟨ [ fr $] .leftInv f ⟩
  f ∎

leftInvCurry : ∀ n {ls ℓ} fr {Xs : Types n ls} {Y : Type ℓ}
             → (f : ⦅ Xs ⦆[ fr ]→ Y ) → [ n ^ fr $]↓ ([ n ^ fr $]↑ f) ≡ f
leftInvCurry zero fr f = refl
leftInvCurry (suc n) fr f = leftInvCurry⁺ n fr f

rightInvCurry⁺ : ∀ n {ls ℓ} fr {Xs : Types (suc n) ls} {Y : Type ℓ} (f : ⦅ Xs ⦆ → Y)
              → [ n ^ fr $]⁺↑ ([ n ^ fr $]⁺↓ f) ≡ f
rightInvCurry⁺ zero fr f = [ fr $] .rightInv f
rightInvCurry⁺ (suc n) fr f =
  uncurry ([ n ^ fr $]⁺↑ ∘ [ fr $] .fun ([ fr $] .inv ([ n ^ fr $]⁺↓ ∘ ((f ∘_) ∘ _,_)))) ≡⟨ cong (λ h → uncurry ([ n ^ fr $]⁺↑ ∘ h)) ([ fr $] .rightInv _) ⟩
  uncurry ([ n ^ fr $]⁺↑ ∘ [ n ^ fr $]⁺↓ ∘ ((f ∘_) ∘ _,_)) ≡⟨ cong (λ r → uncurry (r ∘ ((f ∘_) ∘ _,_))) (funExt (rightInvCurry⁺ n fr)) ⟩
  f ∎

rightInvCurry : ∀ n {ls ℓ} fr {Xs : Types n ls} {Y : Type ℓ} (f : ⦅ Xs ⦆ → Y)
              → [ n ^ fr $]↑ ([ n ^ fr $]↓ f) ≡ f
rightInvCurry zero fr f = refl
rightInvCurry (suc n) fr f = rightInvCurry⁺ n fr f

[_^_$] : ∀ n {ls ℓ} fr {Xs : Types n ls} {Y : Type ℓ}
       → (⦅ Xs ⦆[ fr ]→ Y) ⇔ (⦅ Xs ⦆ → Y)
[ n ^ fr $] .fun = [ n ^ fr $]↑
[ n ^ fr $] .inv = [ n ^ fr $]↓
[ n ^ fr $] .leftInv  = leftInvCurry n fr
[ n ^ fr $] .rightInv = rightInvCurry n fr

↓Π[_^_$]⁺ : ∀ n {ls ℓ} fr {Xs : Types (suc n) ls} {Y : ⦅ Xs ⦆ → Type ℓ} → ((xs : ⦅ Xs ⦆) → Y xs) → xs ⦂⦅ Xs ⦆⁺Π[ fr ]→ Y xs
↓Π[ zero ^ fr  $]⁺ f = Π[ fr $] .inv f
↓Π[ suc n ^ fr $]⁺ f = Π[ fr $] .inv (↓Π[ n ^ fr $]⁺ ∘ (f ∘_) ∘ _,_)

↓Π[_^_$] : ∀ n {ls ℓ} fr {Xs : Types n ls} {Y : ⦅ Xs ⦆ → Type ℓ} → ((xs : ⦅ Xs ⦆) → Y xs) → xs ⦂⦅ Xs ⦆Π[ fr ]→ Y xs
↓Π[ zero ^ fr $] f = f tt
↓Π[ suc n ^ fr $] f = ↓Π[ n ^ fr $]⁺ f

↑Π[_^_$]⁺ : ∀ n {ls ℓ} fr {Xs : Types (suc n) ls} {Y : ⦅ Xs ⦆ → Type ℓ} → (xs ⦂⦅ Xs ⦆⁺Π[ fr ]→ Y xs) → ((xs : ⦅ Xs ⦆) → Y xs)
↑Π[ zero ^ fr  $]⁺ f = Π[ fr $] .fun f
↑Π[ suc n ^ fr $]⁺ f = uncurry (↑Π[ n ^ fr $]⁺ ∘ Π[ fr $] .fun f)

↑Π[_^_$] : ∀ n {ls ℓ} fr {Xs : Types n ls} {Y : ⦅ Xs ⦆ → Type ℓ} → (xs ⦂⦅ Xs ⦆Π[ fr ]→ Y xs) → ((xs : ⦅ Xs ⦆) → Y xs)
↑Π[ zero ^ fr  $] f _ = f
↑Π[ suc n ^ fr $] f = ↑Π[ n ^ fr $]⁺ f

leftInvCurryΠ⁺ : ∀ n {ls ℓ} fr {Xs : Types (suc n) ls} {Y : ⦅ Xs ⦆ → Type ℓ}
              → (f : xs ⦂⦅ Xs ⦆⁺Π[ fr ]→ Y xs) → ↓Π[ n ^ fr $]⁺ (↑Π[ n ^ fr $]⁺ f) ≡ f
leftInvCurryΠ⁺ zero fr f = Π[ fr $] .leftInv f
leftInvCurryΠ⁺ (suc n) fr f =
  Π[ fr $] .inv (↓Π[ n ^ fr $]⁺ ∘ ↑Π[ n ^ fr $]⁺ ∘ Π[ fr $] .fun f)  ≡⟨ cong (Π[ fr $] .inv ∘ flip _∘_ (Π[ fr $] .fun f)) (λ i x → leftInvCurryΠ⁺ n fr x i) ⟩
  Π[ fr $] .inv (Π[ fr $] .fun f) ≡⟨ Π[ fr $] .leftInv f ⟩
  f ∎

leftInvCurryΠ : ∀ n {ls ℓ} fr {Xs : Types n ls} {Y : ⦅ Xs ⦆ → Type ℓ}
              → (f : xs ⦂⦅ Xs ⦆Π[ fr ]→ Y xs) → ↓Π[ n ^ fr $] (↑Π[ n ^ fr $] f) ≡ f
leftInvCurryΠ zero fr f = refl
leftInvCurryΠ (suc n) fr f = leftInvCurryΠ⁺ n fr f

rightInvCurryΠ⁺ : ∀ n {ls ℓ} fr {Xs : Types (suc n) ls} {Y : ⦅ Xs ⦆ → Type ℓ} (f : (xs : ⦅ Xs ⦆) → Y xs)
               → ↑Π[ n ^ fr $]⁺ (↓Π[ n ^ fr $]⁺ f) ≡ f
rightInvCurryΠ⁺ zero fr f = Π[ fr $] .rightInv f
rightInvCurryΠ⁺ (suc n) fr f =
  uncurry (↑Π[ n ^ fr $]⁺ ∘ (Π[ fr $] .fun (Π[ fr $] .inv (↓Π[ n ^ fr $]⁺ ∘ (f ∘_) ∘ _,_)))) ≡⟨ cong (λ h → uncurry (↑Π[ n ^ fr $]⁺ ∘ h)) (Π[ fr $] .rightInv _) ⟩
  uncurry (↑Π[ n ^ fr $]⁺ ∘ ↓Π[ n ^ fr $]⁺ ∘ (f ∘_) ∘ _,_) ≡⟨ cong (uncurry ∘ flip _∘_ ((f ∘_) ∘ _,_)) (λ i x → rightInvCurryΠ⁺ n fr x i) ⟩
  f ∎

rightInvCurryΠ : ∀ n {ls ℓ} fr {Xs : Types n ls} {Y : ⦅ Xs ⦆ → Type ℓ} (f : (xs : ⦅ Xs ⦆) → Y xs)
               → ↑Π[ n ^ fr $] (↓Π[ n ^ fr $] f) ≡ f
rightInvCurryΠ zero fr f = refl
rightInvCurryΠ (suc n) fr f = rightInvCurryΠ⁺ n fr f

Π[_^_$] :  ∀ n {ls ℓ} fr {Xs : Types n ls} {Y : ⦅ Xs ⦆ → Type ℓ} →
           (xs ⦂⦅ Xs ⦆Π[ fr ]→ Y xs) ⇔ ((xs : ⦅ Xs ⦆) → Y xs)
Π[ n ^ fr $] .fun = ↑Π[ n ^ fr $]
Π[ n ^ fr $] .inv = ↓Π[ n ^ fr $]
Π[ n ^ fr $] .leftInv  = leftInvCurryΠ n fr
Π[ n ^ fr $] .rightInv = rightInvCurryΠ n fr

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Andreas, 2017-04-10, issue #2537 reported by xekoukou
-- Preserve named args when splitting in a where clause.

-- {-# OPTIONS -v reify:100 #-}

data Bool : Set where
  true false : Bool

fun : {a b c d e f g : Bool} → Bool → Bool
fun {g = g} x with x
... | r = {!g!} -- C-c C-c g

-- Expected result:
-- fun {g = true} x | r = ?
-- fun {g = false} x | r = ?

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Numeral.Natural.Oper.Comparisons.Proofs where

open import Data.Boolean.Stmt
open import Data.Boolean
open import Logic.Propositional
open import Numeral.Natural
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.Proofs
open import Relator.Equals

[≤?]-𝟎 : ∀{n} → IsTrue(𝟎 ≤? n)
[≤?]-𝟎 = [⊤]-intro

[≤?]-𝐒 : ∀{n} → IsTrue(n ≤? 𝐒(n))
[≤?]-𝐒 {𝟎}   = [⊤]-intro
[≤?]-𝐒 {𝐒 n} = [≤?]-𝐒 {n}

[<?]-𝟎 : ∀{n} → IsTrue(𝟎 <? 𝐒(n))
[<?]-𝟎 {𝟎}   = [⊤]-intro
[<?]-𝟎 {𝐒 n} = [<?]-𝟎 {n}

[<?]-𝐒 : ∀{n} → IsTrue(n <? 𝐒(n))
[<?]-𝐒 {𝟎}   = [⊤]-intro
[<?]-𝐒 {𝐒 n} = [<?]-𝐒 {n}

[≤?]-reflexivity : ∀{n} → IsTrue(n ≤? n)
[≤?]-reflexivity {𝟎}    = [⊤]-intro
[≤?]-reflexivity {𝐒(n)} = [≤?]-reflexivity {n}

[<?]-positive : ∀{n} → (𝟎 <? n) ≡ positive?(n)
[<?]-positive {𝟎}    = [≡]-intro
[<?]-positive {𝐒(_)} = [≡]-intro
{-# REWRITE [<?]-positive #-}

[<?]-positive-any : ∀{m n} → ⦃ _ : IsTrue(m <? n) ⦄ → IsTrue(positive?(n))
[<?]-positive-any {𝟎}   {n}   ⦃ p ⦄ = p
[<?]-positive-any {𝐒 m} {𝐒 n} ⦃ p ⦄ = [⊤]-intro

[≤?]-positive : ∀{n} → (𝐒(𝟎) ≤? n) ≡ positive?(n)
[≤?]-positive {𝟎}    = [≡]-intro
[≤?]-positive {𝐒(_)} = [≡]-intro

[≢?]-positive : ∀{n} → (n ≢? 𝟎) ≡ positive?(n)
[≢?]-positive {𝟎}    = [≡]-intro
[≢?]-positive {𝐒(_)} = [≡]-intro

[<?]-to-[≤?] : ∀{a b} → ((a <? b) ≡ (𝐒(a) ≤? b))
[<?]-to-[≤?] {𝟎}   {𝟎}    = [≡]-intro
[<?]-to-[≤?] {𝟎}   {𝐒(_)} = [≡]-intro
[<?]-to-[≤?] {𝐒(_)}{𝟎}    = [≡]-intro
[<?]-to-[≤?] {𝐒(a)}{𝐒(b)} = [<?]-to-[≤?] {a}{b}

[≡?]-zero : ∀{n} → (n ≡? 𝟎) ≡ zero?(n)
[≡?]-zero {𝟎}    = [≡]-intro
[≡?]-zero {𝐒(_)} = [≡]-intro


text:
open import Relation.Binary.Core

module InsertSort.Impl1.Correctness.Permutation.Alternative {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_) where

open import Data.List
open import Data.Sum
open import Function
open import InsertSort.Impl1 _≤_ tot≤
open import List.Permutation.Alternative A renaming (_∼_ to _∼′_)
open import List.Permutation.Alternative.Correctness A
open import List.Permutation.Base A

lemma-insert∼′ : (x : A)(xs : List A) → (x ∷ xs) ∼′ insert x xs
lemma-insert∼′ x [] = ∼refl
lemma-insert∼′ x (y ∷ ys)
    with tot≤ x y
... | inj₁ x≤y = ∼refl
... | inj₂ y≤x = ∼trans (∼swap ∼refl) (∼head y (lemma-insert∼′ x ys))

lemma-insertSort∼′ : (xs : List A) → xs ∼′ insertSort xs
lemma-insertSort∼′ [] = ∼refl
lemma-insertSort∼′ (x ∷ xs) = ∼trans (∼head x (lemma-insertSort∼′ xs)) (lemma-insert∼′ x (insertSort xs))

theorem-insertSort∼ : (xs : List A) → xs ∼ insertSort xs
theorem-insertSort∼ = lemma-∼′-∼ ∘ lemma-insertSort∼′

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module NF.Sum where

open import NF
open import Data.Sum
open import Relation.Binary.PropositionalEquality

instance
  nfInj₁ : {A B : Set}{a : A}{{nfa : NF a}} -> NF {A ⊎ B} (inj₁ a)
  Sing.unpack (NF.!! (nfInj₁ {a = a})) = inj₁ (nf a)
  Sing.eq (NF.!! (nfInj₁ {{nfa}})) rewrite nf≡ {{nfa}} = refl

  {-# INLINE nfInj₁ #-}

  nfInj₂ : {A B : Set}{b : B}{{nfb : NF b}} -> NF {A ⊎ B} (inj₂ b)
  Sing.unpack (NF.!! (nfInj₂ {b = b})) = inj₂ (nf b)
  Sing.eq (NF.!! (nfInj₂ {{nfb}})) rewrite nf≡ {{nfb}} = refl

  {-# INLINE nfInj₂ #-}

max_stars_repo_name: yanok/normalize-via-instances

max_issues_repo_name: yanok/normalize-via-instances

max_forks_repo_name: yanok/normalize-via-instances


text:
module Category.Universality where

open import Level
open import Category.Core
open import Category.Comma
open import Category.Instance

-- something is universal from c to S when it's an initial object in c / S
universal : {𝒸₀ ℓ₀ 𝒸₁ ℓ₁ : Level}
    → {C : Category 𝒸₀ ℓ₀} {D : Category 𝒸₁ ℓ₁}
    → {c : Category.Object C} → {S : Functor D C}
    → (init : Category.Object (point c ↓ S))
    → Set (𝒸₁ ⊔ (ℓ₀ ⊔ 𝒸₀))
universal {c = c} {S = S} init = initial (point c ↓ S) init
    where
        initial : ∀ {𝒸 ℓ} → (C : Category 𝒸 ℓ) → Category.Object C → Set 𝒸
        initial C init = ∀ (other : Object) → init ⇒ other
            where
                open Category C

initial : ∀ {𝒸 ℓ} (C : Category 𝒸 ℓ) → Category.Object C → Set (𝒸 ⊔ (ℓ ⊔ 𝒸))
initial C c = universal {C = C} {D = C} {c} {identity C} (record
        { source = tt
        ; target = c
        ; morphism = id c
        })
        where
            open import Data.Unit
            open Category C

initial-prop : ∀ {𝒸 ℓ} {C : Category 𝒸 ℓ}
    → (init : Category.Object C)
    → initial C init
    → (other : Category.Object C)
    → Category._⇒_ C init other
initial-prop {C = C} obj obj-init other = Comma.morphismBetweenSources {!   !}
    where
        open Category C

-- prop1 : {!   !}
-- prop1 = {! initial  !}

max_stars_repo_name: banacorn/categories

max_issues_repo_name: banacorn/categories

max_forks_repo_name: banacorn/categories


text:
------------------------------------------------------------------------------
-- Operations on and with functions
------------------------------------------------------------------------------

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

module Common.Function where

-- From Funcion.agda (Agda standard library 0.8.1).
-- infixr 0 _$_

------------------------------------------------------------------------------
-- The right associative application operator.
--
-- N.B. The operator is not first-order, so it cannot be used with
-- types/terms which will be translated to FOL.
-- _$_ : {A : Set}{B : A → Set} → ((x : A) → B x) → (x : A) → B x
-- f $ x = f x

-- N.B. The function is not first-order, so it cannot be used with
-- types/terms which will be translated to FOL.
-- flip : {A : Set} → (A → A → A) → A → A → A
-- flip f y x = f x y


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Truncation.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.PathSplitEquiv
open isPathSplitEquiv
open import Cubical.Modalities.Everything
open Modality

open import Cubical.Data.Empty as ⊥ using (⊥)
open import Cubical.Data.Nat hiding (elim)
open import Cubical.Data.NatMinusOne as ℕ₋₁ hiding (1+_)
open import Cubical.Data.NatMinusTwo as ℕ₋₂ hiding (-1+_)
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.HITs.Nullification as Null hiding (rec; elim)

open import Cubical.HITs.Truncation.Base

open import Cubical.HITs.PropositionalTruncation as PropTrunc
  renaming (∥_∥ to ∥_∥₋₁; ∣_∣ to ∣_∣₋₁; squash to squash₋₁) using ()
open import Cubical.HITs.SetTruncation       as SetTrunc  using (∥_∥₀; ∣_∣₀; squash₀)
open import Cubical.HITs.GroupoidTruncation  as GpdTrunc  using (∥_∥₁; ∣_∣₁; squash₁)
open import Cubical.HITs.2GroupoidTruncation as 2GpdTrunc using (∥_∥₂; ∣_∣₂; squash₂)

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

sphereFill : (n : ℕ₋₁) (f : S n → A) → Type _
sphereFill {A = A} n f = Σ[ top ∈ A ] ((x : S n) → top ≡ f x)

isSphereFilled : ℕ₋₁ → Type ℓ → Type ℓ
isSphereFilled n A = (f : S n → A) → sphereFill n f

isSphereFilledTrunc : {n : ℕ} → isSphereFilled (-1+ n) (hLevelTrunc n A)
isSphereFilledTrunc {n = zero}  f = hub f , ⊥.elim
isSphereFilledTrunc {n = suc n} f = hub f , spoke f

isSphereFilled→isOfHLevelSuc : {n : ℕ} → isSphereFilled (ℕ→ℕ₋₁ n) A → isOfHLevel (suc n) A
isSphereFilled→isOfHLevelSuc {A = A} {zero} h x y = sym (snd (h f) north) ∙ snd (h f) south
  where
    f : Susp ⊥ → A
    f north = x
    f south = y
    f (merid () i)
isSphereFilled→isOfHLevelSuc {A = A} {suc n} h x y = isSphereFilled→isOfHLevelSuc (helper h x y)
  where
    helper : isSphereFilled (ℕ→ℕ₋₁ (suc n)) A → (x y : A) → isSphereFilled (ℕ→ℕ₋₁ n) (x ≡ y)
    helper h x y f = l , r
      where
        f' : Susp (S (ℕ→ℕ₋₁ n)) → A
        f' north = x
        f' south = y
        f' (merid u i) = f u i

        u : sphereFill (ℕ→ℕ₋₁ (suc n)) f'
        u = h f'

        z : A
        z = fst u

        p : z ≡ x
        p = snd u north

        q : z ≡ y
        q = snd u south

        l : x ≡ y
        l = sym p ∙ q

        r : (s : S (ℕ→ℕ₋₁ n)) → l ≡ f s
        r s i j = hcomp
                    (λ k →
                       λ { (i = i0) → compPath-filler (sym p) q k j
                         ; (i = i1) → snd u (merid s j) k
                         ; (j = i0) → p (k ∨ (~ i))
                         ; (j = i1) → q k
                         })
                  (p ((~ i) ∧ (~ j)))

isOfHLevel→isSphereFilled : {n : ℕ} → isOfHLevel n A → isSphereFilled (-1+ n) A
isOfHLevel→isSphereFilled {A = A} {zero} h f = fst h , λ _ → snd h _
isOfHLevel→isSphereFilled {A = A} {suc zero} h f = f north , λ _ → h _ _
isOfHLevel→isSphereFilled {A = A} {suc (suc n)} h = helper λ x y → isOfHLevel→isSphereFilled (h x y)
  where
    helper : {n : ℕ} → ((x y : A) → isSphereFilled (-1+ n) (x ≡ y)) → isSphereFilled (suc₋₁ (-1+ n)) A
    helper {n = n} h f = l , r
      where
      l : A
      l = f north

      f' : S (-1+ n) → f north ≡ f south
      f' x i = f (merid x i)

      h' : sphereFill (-1+ n) f'
      h' = h (f north) (f south) f'

      r : (x : S (suc₋₁ (-1+ n))) → l ≡ f x
      r north = refl
      r south = h' .fst
      r (merid x i) j = hcomp (λ k → λ { (i = i0) → f north
                                        ; (i = i1) → h' .snd x (~ k) j
                                        ; (j = i0) → f north
                                        ; (j = i1) → f (merid x i) }) (f (merid x (i ∧ j)))

-- isNull (S n) A ≃ (isSphereFilled n A) × (∀ (x y : A) → isSphereFilled n (x ≡ y))

isOfHLevel→isSnNull : {n : ℕ} → isOfHLevel n A → isNull (S (-1+ n)) A
fst (sec (isOfHLevel→isSnNull h)) f     = fst (isOfHLevel→isSphereFilled h f)
snd (sec (isOfHLevel→isSnNull h)) f i s = snd (isOfHLevel→isSphereFilled h f) s i
fst (secCong (isOfHLevel→isSnNull h) x y) p = fst (isOfHLevel→isSphereFilled (isOfHLevelPath _ h x y) (funExt⁻ p))
snd (secCong (isOfHLevel→isSnNull h) x y) p i j s = snd (isOfHLevel→isSphereFilled (isOfHLevelPath _ h x y) (funExt⁻ p)) s i j

isSnNull→isOfHLevel : {n : ℕ} → isNull (S (-1+ n)) A → isOfHLevel n A
isSnNull→isOfHLevel {n = zero}  nA = fst (sec nA) ⊥.rec , λ y → fst (secCong nA _ y) (funExt ⊥.elim)
isSnNull→isOfHLevel {n = suc n} nA = isSphereFilled→isOfHLevelSuc (λ f → fst (sec nA) f , λ s i → snd (sec nA) f i s)

isOfHLevelTrunc : (n : ℕ) → isOfHLevel n (hLevelTrunc n A)
isOfHLevelTrunc zero    = hub ⊥.rec , λ _ → ≡hub ⊥.rec
isOfHLevelTrunc (suc n) = isSphereFilled→isOfHLevelSuc isSphereFilledTrunc
-- isOfHLevelTrunc n = isSnNull→isOfHLevel isNull-Null

-- hLevelTrunc n is a modality

rec : {n : ℕ}
      {B : Type ℓ'} →
      (isOfHLevel n B) →
      (g : (a : A) → B) →
      (hLevelTrunc n A → B)
rec {B = B} h = Null.elim {B = λ _ → B} λ x → isOfHLevel→isSnNull h

elim : {n : ℕ}
  {B : hLevelTrunc n A → Type ℓ'}
  (hB : (x : hLevelTrunc n A) → isOfHLevel n (B x))
  (g : (a : A) → B (∣ a ∣))
  (x : hLevelTrunc n A) →
  B x
elim hB = Null.elim (λ x → isOfHLevel→isSnNull (hB x))

elim2 : {n : ℕ}
  {B : hLevelTrunc n A → hLevelTrunc n A → Type ℓ'}
  (hB : ((x y : hLevelTrunc n A) → isOfHLevel n (B x y)))
  (g : (a b : A) → B ∣ a ∣ ∣ b ∣)
  (x y : hLevelTrunc n A) →
  B x y
elim2 {n = n} hB g =
  elim (λ _ → isOfHLevelPi n (λ _ → hB _ _))
    (λ a → elim (λ _ → hB _ _) (λ b → g a b))

elim3 : {n : ℕ}
  {B : (x y z : hLevelTrunc n A) → Type ℓ'}
  (hB : ((x y z : hLevelTrunc n A) → isOfHLevel n (B x y z)))
  (g : (a b c : A) → B (∣ a ∣) ∣ b ∣ ∣ c ∣)
  (x y z : hLevelTrunc n A) →
  B x y z
elim3 {n = n} hB g =
  elim2 (λ _ _ → isOfHLevelPi n (hB _ _))
    (λ a b → elim (λ _ → hB _ _ _) (λ c → g a b c))

HLevelTruncModality : ∀ {ℓ} (n : ℕ) → Modality ℓ
isModal       (HLevelTruncModality n) = isOfHLevel n
isModalIsProp (HLevelTruncModality n) = isPropIsOfHLevel n
◯             (HLevelTruncModality n) = hLevelTrunc n
◯-isModal     (HLevelTruncModality n) = isOfHLevelTrunc n
η             (HLevelTruncModality n) = ∣_∣
◯-elim        (HLevelTruncModality n) = elim
◯-elim-β      (HLevelTruncModality n) = λ _ _ _ → refl
◯-=-isModal   (HLevelTruncModality n) = isOfHLevelPath n (isOfHLevelTrunc n)

idemTrunc : (n : ℕ) → isOfHLevel n A → A ≃ (hLevelTrunc n A)
idemTrunc n hA = ∣_∣ , isModalToIsEquiv (HLevelTruncModality n) hA

-- equivalences to prop/set/groupoid truncations

propTrunc≃Trunc-1 : ∥ A ∥₋₁ ≃ ∥ A ∥ -1
propTrunc≃Trunc-1 =
  isoToEquiv
    (iso
      (PropTrunc.elim (λ _ → isOfHLevelTrunc 1) ∣_∣)
      (elim (λ _ → squash₋₁) ∣_∣₋₁)
      (elim (λ _ → isOfHLevelPath 1 (isOfHLevelTrunc 1) _ _) (λ _ → refl))
      (PropTrunc.elim (λ _ → isOfHLevelPath 1 squash₋₁ _ _) (λ _ → refl)))

setTrunc≃Trunc0 : ∥ A ∥₀ ≃ ∥ A ∥ 0
setTrunc≃Trunc0 =
  isoToEquiv
    (iso
      (SetTrunc.elim (λ _ → isOfHLevelTrunc 2) ∣_∣)
      (elim (λ _ → squash₀) ∣_∣₀)
      (elim (λ _ → isOfHLevelPath 2 (isOfHLevelTrunc 2) _ _) (λ _ → refl))
      (SetTrunc.elim (λ _ → isOfHLevelPath 2 squash₀ _ _) (λ _ → refl)))

groupoidTrunc≃Trunc1 : ∥ A ∥₁ ≃ ∥ A ∥ 1
groupoidTrunc≃Trunc1 =
  isoToEquiv
    (iso
      (GpdTrunc.elim (λ _ → isOfHLevelTrunc 3) ∣_∣)
      (elim (λ _ → squash₁) ∣_∣₁)
      (elim (λ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _) (λ _ → refl))
      (GpdTrunc.elim (λ _ → isOfHLevelPath 3 squash₁ _ _) (λ _ → refl)))

2GroupoidTrunc≃Trunc2 : ∥ A ∥₂ ≃ ∥ A ∥ 2
2GroupoidTrunc≃Trunc2 =
  isoToEquiv
    (iso
      (2GpdTrunc.elim (λ _ → isOfHLevelTrunc 4) ∣_∣)
      (elim (λ _ → squash₂) ∣_∣₂)
      (elim (λ _ → isOfHLevelPath 4 (isOfHLevelTrunc 4) _ _) (λ _ → refl))
      (2GpdTrunc.elim (λ _ → isOfHLevelPath 4 squash₂ _ _) (λ _ → refl)))

---- ∥ Ω A ∥ ₙ ≡ Ω ∥ A ∥ₙ₊₁  ----

  {- Proofs of Theorem 7.3.12. and Corollary 7.3.13. in the HoTT book  -}

private
  {- We define the fibration P to show a more general result  -}
  P :  ∀ {ℓ} {B : Type ℓ}{n : ℕ₋₂} → ∥ B ∥  (suc₋₂ n) → ∥ B ∥  (suc₋₂ n) → Type ℓ
  P x y = fst (P₁ x y)
    where
    P₁ : ∀ {ℓ} {B : Type ℓ} {n : ℕ₋₂} → ∥ B ∥  (suc₋₂ n) → ∥ B ∥  (suc₋₂ n) → (HLevel  ℓ (2+ n))
    P₁ {ℓ} {n = n}  x y =
      elim2 (λ _ _  → isOfHLevelHLevel (2+ n)) (λ a b → ∥ a ≡ b ∥  n , isOfHLevelTrunc (2+ n)) x y

  {- We will need P to be of hLevel n + 3  -}
  hLevelP : ∀{ℓ} {n : ℕ₋₂} {B : Type ℓ} (a b : ∥ B ∥ (suc₋₂ n)) → isOfHLevel (2+ (suc₋₂ n)) (P a b )
  hLevelP {n = n} =
    elim2
      (λ x y → isProp→isOfHLevelSuc (2+ n) (isPropIsOfHLevel (2+ suc₋₂ n)) )
      (λ a b → isOfHLevelSuc (2+ n) (isOfHLevelTrunc (2+ n)))

  {- decode function from P x y to x ≡ y -}
  decode-fun :  ∀ {ℓ} {B : Type ℓ} {n : ℕ₋₂} (x y : ∥ B ∥ (suc₋₂ n)) → P x y → x ≡ y
  decode-fun {B = B} {n = n} =
    elim2
      (λ u v → isOfHLevelPi
        (2+ suc₋₂ n)
        (λ _ → isOfHLevelSuc (2+ suc₋₂ n) (isOfHLevelTrunc (2+ suc₋₂ n)) u v))
      decode*
      where
      decode* :  ∀ {ℓ} {B : Type ℓ} {n : ℕ₋₂}(u v : B)
        → (P {n = n} ∣ u ∣ ∣ v ∣) → _≡_ {A = ∥ B ∥ (suc₋₂ n)} ∣ u ∣ ∣ v ∣
      decode* {B = B} {n = neg2} u v =
        rec
          ( isOfHLevelTrunc (suc zero) ∣ u ∣ ∣ v ∣
          , λ _ →
            isOfHLevelSuc (suc zero) (isOfHLevelTrunc (suc zero)) _ _ _ _
          )
          (λ p → cong (λ z → ∣ z ∣) p)
      decode* {n = ℕ₋₂.-1+ n} u v =
        rec (isOfHLevelTrunc (suc (suc n)) ∣ u ∣ ∣ v ∣) (λ p → cong (λ z → ∣ z ∣) p)

  {- auxilliary function r used to define encode -}
  r :  ∀ {ℓ} {B : Type ℓ} {m : ℕ₋₂} (u : ∥ B ∥ (suc₋₂ m)) → P u u
  r {m = m}  = elim (λ x → hLevelP x x) (λ a → ∣ refl ∣)

  {- encode function from x ≡ y to P x y -}
  encode-fun : ∀ {ℓ} {B : Type ℓ} {n : ℕ₋₂} (x y : ∥ B ∥ (suc₋₂ n)) → x ≡ y → P x y
  encode-fun x y p = transport (λ i → P x (p i)) (r x)

  {- We need the following two lemmas on the functions behaviour for refl -}
  dec-refl : ∀ {ℓ} {B : Type ℓ} {n : ℕ₋₂}
    (x : ∥ B ∥ (suc₋₂ n)) → decode-fun x x (r x) ≡ refl {x = x}
  dec-refl {B = B} {n = neg2} =
    elim
      (λ x →
        isOfHLevelSuc (suc zero)
          (isOfHLevelSuc (suc zero) (isOfHLevelTrunc (suc zero)) x x)
          _ _)
      (λ a → refl)
  dec-refl {n = ℕ₋₂.-1+ n} =
    elim
      (λ x →
        isOfHLevelSuc (suc n)
         (isOfHLevelSuc (suc n)
            (isOfHLevelTrunc (suc (suc n)) x x)
            (decode-fun x x (r x)) refl))
      (λ c → refl)

  enc-refl : ∀ {ℓ} {B : Type ℓ} {n : ℕ₋₂}
    (x : ∥ B ∥ (suc₋₂ n)) → encode-fun x x refl ≡ r x
  enc-refl x j = transp (λ i → P x (refl {x = x} i)) j (r x)

  {- decode-fun is a right-inverse -}
  P-rinv : ∀ {ℓ} {B : Type ℓ} {n : ℕ₋₂} (u v : ∥ B ∥  (suc₋₂ n)) →
    (x : _≡_ {A = ∥ B ∥ (suc₋₂ n)} u v) → decode-fun u v (encode-fun u v x) ≡ x
  P-rinv {ℓ = ℓ} {B = B} {n = n} u v =
    J (λ y p → decode-fun u y (encode-fun u y p) ≡ p)
      ((λ i → (decode-fun u u (enc-refl u i))) ∙ dec-refl u)

  {- decode-fun is a left-inverse -}
  P-linv : ∀ {ℓ} {B : Type ℓ} {n : ℕ₋₂} (u v : ∥ B ∥ (suc₋₂ n )) →
    (x : P u v) → encode-fun u v (decode-fun u v x) ≡ x
  P-linv {n = n} =
    elim2
      (λ x y → isOfHLevelPi (2+ suc₋₂ n)
        (λ z → isOfHLevelSuc (2+ suc₋₂ n) (hLevelP x y) _ _))
      helper
    where
    helper : ∀ {ℓ} {B : Type ℓ} {n : ℕ₋₂} (a b : B) (x : P {n = n} ∣ a ∣ ∣ b ∣)
      → encode-fun ∣ a ∣ ∣ b ∣ (decode-fun ∣ a ∣ ∣ b ∣ x) ≡ x
    helper {n = neg2} a b =
      elim
        (λ x →
          ( sym (isOfHLevelTrunc zero .snd (encode-fun ∣ a ∣ ∣ b ∣ (decode-fun ∣ a ∣ ∣ b ∣ x)))
            ∙ (isOfHLevelTrunc zero .snd x)
          , λ y →
            isOfHLevelSuc (suc zero)
              (isOfHLevelSuc zero (isOfHLevelTrunc {A = a ≡ b} zero))
              _ _ _ _
          ))
        (J
          (λ y p → encode-fun ∣ a ∣ ∣ y ∣ ((decode-fun ∣ a ∣ ∣ y ∣) ∣ p ∣) ≡ ∣ p ∣)
          (enc-refl ∣ a ∣))
    helper {n = ℕ₋₂.-1+ n} a b =
      elim
        (λ x → hLevelP {n = ℕ₋₂.-1+ n} ∣ a ∣ ∣ b ∣ _ _)
        (J (λ y p → encode-fun {n = ℕ₋₂.-1+ n} ∣ a ∣ ∣ y ∣ ((decode-fun ∣ a ∣ ∣ y ∣) ∣ p ∣) ≡ ∣ p ∣)
           (enc-refl ∣ a ∣))

  {- The final Iso established -}
  IsoFinal : ∀ {ℓ} {B : Type ℓ} {n : ℕ₋₂} (x y : ∥ B ∥ (suc₋₂ n)) → Iso (x ≡ y) (P x y)
  IsoFinal x y = iso (encode-fun x y ) (decode-fun x y) (P-linv x y) (P-rinv x y)

PathIdTrunc : {a b : A} (n : ℕ₋₂) → (_≡_ {A = ∥ A ∥ (suc₋₂ n)} ∣ a ∣ ∣ b ∣) ≡ (∥ a ≡ b ∥ n)
PathIdTrunc {a = a} {b = b} n = isoToPath (IsoFinal {n = n} ∣ a ∣ ∣ b ∣)

PathΩ : {a : A} (n : ℕ₋₂) → (_≡_ {A = ∥ A ∥ (suc₋₂ n)} ∣ a ∣ ∣ a ∣) ≡ (∥ a ≡ a ∥ n)
PathΩ {a = a} n = PathIdTrunc {a = a} {b = a} n

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
module Numeric.Nat.Divide.Properties where

open import Prelude
open import Numeric.Nat.Properties
open import Numeric.Nat.DivMod
open import Numeric.Nat.Divide
open import Tactic.Nat

divides-add : ∀ {a b d} → d Divides a → d Divides b → d Divides (a + b)
divides-add (factor! q) (factor! q₁) = factor (q + q₁) auto

divides-mul-r : ∀ a {b d} → d Divides b → d Divides (a * b)
divides-mul-r a (factor! q) = factor (a * q) auto

divides-mul-l : ∀ {a} b {d} → d Divides a → d Divides (a * b)
divides-mul-l b (factor! q) = factor (b * q) auto

divides-mul : ∀ {a b c d} → c Divides a → d Divides b → (c * d) Divides (a * b)
divides-mul (factor! q) (factor! r) = factor (q * r) auto

mul-divides-l : (a b c : Nat) → (a * b) Divides c → a Divides c
mul-divides-l a b c (factor! q) = factor (q * b) auto

mul-divides-r : (a b c : Nat) → (a * b) Divides c → b Divides c
mul-divides-r a b c (factor! q) = factor (q * a) auto

divides-flip-mul : ∀ {a b c d} → c Divides b → d Divides a → (c * d) Divides (a * b)
divides-flip-mul {a} {b} {c} {d} c|b d|a =
  transport ((c * d) Divides_) (mul-commute b a) (divides-mul c|b d|a)

divides-sub-l : ∀ {a b d} → d Divides (a + b) → d Divides a → d Divides b
divides-sub-l {b = b} {d} (factor q₁ eq) (factor! q) = factor (q₁ - q) $ by eq

divides-sub-r : ∀ {a b d} → d Divides (a + b) → d Divides b → d Divides a
divides-sub-r {a} {b} d|ab d|b rewrite add-commute a b = divides-sub-l d|ab d|b

divides-mul-cong-l : ∀ {a b} c → a Divides b → (c * a) Divides (c * b)
divides-mul-cong-l {a} {b} c (factor q eq) = factor q (by (c *_ $≡ eq))

divides-mul-cong-r : ∀ {a b} c → a Divides b → (a * c) Divides (b * c)
divides-mul-cong-r {a} {b} c (factor q eq) = factor q (by (c *_ $≡ eq))

divides-nonzero : ∀ {a b} {{_ : NonZero b}} → a Divides b → NonZero a
divides-nonzero {zero} {{nzb}} (factor! b) = transport NonZero (mul-zero-r b) nzb
divides-nonzero {suc _} _ = _

divides-refl : ∀ {a} → a Divides a
divides-refl = factor 1 auto

divides-antisym : ∀ {a b} → a Divides b → b Divides a → a ≡ b
divides-antisym         (factor! q)       (factor! 0)                = auto
divides-antisym         (factor! q)       (factor 1 eq)              = by eq
divides-antisym {zero}  (factor! q)       (factor (suc (suc q₁)) eq) = auto
divides-antisym {suc a} (factor! 0)       (factor (suc (suc q₁)) eq) = by eq
divides-antisym {suc a} (factor! (suc q)) (factor (suc (suc q₁)) eq) = refute eq

divides-trans : ∀ {a b c} → a Divides b → b Divides c → a Divides c
divides-trans (factor! q) (factor! q′) = factor (q′ * q) auto

divides-zero : ∀ {a} → 0 Divides a → a ≡ 0
divides-zero (factor! q) = auto

one-divides : ∀ {a} → 1 Divides a
one-divides {a} = factor a auto

divides-one : ∀ {a} → a Divides 1 → a ≡ 1
divides-one {0} (factor k eq) = refute eq
divides-one {1} _ = refl
divides-one {suc (suc a)} (factor zero ())
divides-one {suc (suc a)} (factor (suc k) eq) = refute eq

mul=1-l : (a b : Nat) → a * b ≡ 1 → a ≡ 1
mul=1-l a b eq =
  divides-one (transport (a Divides_) eq (divides-mul-l b divides-refl))

mul=1-r : (a b : Nat) → a * b ≡ 1 → b ≡ 1
mul=1-r a b eq = mul=1-l b a (by eq)

divides-less : ∀ {a b} {{_ : NonZero b}} → a Divides b → a ≤ b
divides-less {{}} (factor! 0)
divides-less {a} (factor! (suc q)) = auto

nonzero-factor : ∀ {a b} ⦃ nzb : NonZero b ⦄ (a|b : a Divides b) → NonZero (get-factor a|b)
nonzero-factor ⦃ () ⦄ (factor! zero)
nonzero-factor (factor! (suc _)) = _

cancel-mul-divides-r : ∀ a b c ⦃ _ : NonZero c ⦄ → (a * c) Divides (b * c) → a Divides b
cancel-mul-divides-r a b c (factor q qac=bc) =
  factor q (mul-inj₁ (q * a) b c (by qac=bc))

cancel-mul-divides-l : ∀ a b c ⦃ _ : NonZero a ⦄ → (a * b) Divides (a * c) → b Divides c
cancel-mul-divides-l a b c rewrite mul-commute a b | mul-commute a c = cancel-mul-divides-r b c a

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Maybe type and some operations
------------------------------------------------------------------------

-- The definitions in this file are reexported by Data.Maybe.

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

module Data.Maybe.Base where

open import Level
open import Data.Bool.Base using (Bool; true; false; not)
open import Data.Unit.Base using (⊤)
open import Data.These using (These; this; that; these)
open import Data.Product as Prod using (_×_; _,_)
open import Function
open import Relation.Nullary

------------------------------------------------------------------------
-- Definition

data Maybe {a} (A : Set a) : Set a where
  just    : (x : A) → Maybe A
  nothing : Maybe A

------------------------------------------------------------------------
-- Some operations

boolToMaybe : Bool → Maybe ⊤
boolToMaybe true  = just _
boolToMaybe false = nothing

is-just : ∀ {a} {A : Set a} → Maybe A → Bool
is-just (just _) = true
is-just nothing  = false

is-nothing : ∀ {a} {A : Set a} → Maybe A → Bool
is-nothing = not ∘ is-just

decToMaybe : ∀ {a} {A : Set a} → Dec A → Maybe A
decToMaybe (yes x) = just x
decToMaybe (no _)  = nothing

-- A dependent eliminator.

maybe : ∀ {a b} {A : Set a} {B : Maybe A → Set b} →
        ((x : A) → B (just x)) → B nothing → (x : Maybe A) → B x
maybe j n (just x) = j x
maybe j n nothing  = n

-- A non-dependent eliminator.

maybe′ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → B → Maybe A → B
maybe′ = maybe

-- A defaulting mechanism

fromMaybe : ∀ {a} {A : Set a} → A → Maybe A → A
fromMaybe = maybe′ id

-- A safe variant of "fromJust". If the value is nothing, then the
-- return type is the unit type.

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

  From-just : Maybe A → Set a
  From-just (just _) = A
  From-just nothing  = Lift a ⊤

  from-just : (x : Maybe A) → From-just x
  from-just (just x) = x
  from-just nothing  = _

-- Functoriality: map.

map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Maybe A → Maybe B
map f = maybe (just ∘ f) nothing

-- Alternative: <∣>

_<∣>_ : ∀ {a} {A : Set a} → Maybe A → Maybe A → Maybe A
just x  <∣> my = just x
nothing <∣> my = my

------------------------------------------------------------------------
-- Aligning and zipping

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where

  alignWith : (These A B → C) → Maybe A → Maybe B → Maybe C
  alignWith f (just a) (just b) = just (f (these a b))
  alignWith f (just a) nothing  = just (f (this a))
  alignWith f nothing  (just b) = just (f (that b))
  alignWith f nothing  nothing  = nothing

  zipWith : (A → B → C) → Maybe A → Maybe B → Maybe C
  zipWith f (just a) (just b) = just (f a b)
  zipWith _ _ _ = nothing

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

  align : Maybe A → Maybe B → Maybe (These A B)
  align = alignWith id

  zip : Maybe A → Maybe B → Maybe (A × B)
  zip = zipWith _,_

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

-- Injections.

  thisM : A → Maybe B → These A B
  thisM a = maybe′ (these a) (this a)

  thatM : Maybe A → B → These A B
  thatM = maybe′ these that


text:
-- Solver for Category

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

open import Categories.Category

module Experiment.Categories.Solver.Category {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level
open import Relation.Binary using (Rel)

import Categories.Morphism.Reasoning as MR

open Category 𝒞
open HomReasoning
open MR 𝒞

private
  variable
    A B C D E : Obj

infixr 9 _:∘_

data Expr : Rel Obj (o ⊔ ℓ) where
  :id  : Expr A A
  _:∘_ : Expr B C → Expr A B → Expr A C
  ∥_∥  : A ⇒ B → Expr A B

-- Semantics
⟦_⟧ : Expr A B → A ⇒ B
⟦ :id      ⟧ = id
⟦ e₁ :∘ e₂ ⟧ = ⟦ e₁ ⟧ ∘ ⟦ e₂ ⟧
⟦ ∥ f ∥    ⟧ = f

⟦_⟧N∘_ : Expr B C → A ⇒ B → A ⇒ C
⟦ :id      ⟧N∘ g = g
⟦ e₁ :∘ e₂ ⟧N∘ g = ⟦ e₁ ⟧N∘ (⟦ e₂ ⟧N∘ g)
⟦ ∥ f ∥    ⟧N∘ g = f ∘ g

⟦_⟧N : Expr A B → A ⇒ B
⟦ e ⟧N = ⟦ e ⟧N∘ id

⟦e⟧N∘f≈⟦e⟧∘f : (e : Expr B C) (g : A ⇒ B) → ⟦ e ⟧N∘ g ≈ ⟦ e ⟧ ∘ g
⟦e⟧N∘f≈⟦e⟧∘f :id        g = ⟺ identityˡ
⟦e⟧N∘f≈⟦e⟧∘f (e₁ :∘ e₂) g = begin
  ⟦ e₁ ⟧N∘ (⟦ e₂ ⟧N∘ g) ≈⟨ ⟦e⟧N∘f≈⟦e⟧∘f e₁ (⟦ e₂ ⟧N∘ g) ⟩
  ⟦ e₁ ⟧ ∘ (⟦ e₂ ⟧N∘ g) ≈⟨ pushʳ (⟦e⟧N∘f≈⟦e⟧∘f e₂ g) ⟩
  (⟦ e₁ ⟧ ∘ ⟦ e₂ ⟧) ∘ g ∎
⟦e⟧N∘f≈⟦e⟧∘f ∥ f ∥      g = refl

⟦e⟧N≈⟦e⟧ : (e : Expr A B) → ⟦ e ⟧N ≈ ⟦ e ⟧
⟦e⟧N≈⟦e⟧ e = ⟦e⟧N∘f≈⟦e⟧∘f e id ○ identityʳ

solve : (e₁ e₂ : Expr A B) → ⟦ e₁ ⟧N ≈ ⟦ e₂ ⟧N → ⟦ e₁ ⟧ ≈ ⟦ e₂ ⟧
solve e₁ e₂ eq = begin
  ⟦ e₁ ⟧  ≈˘⟨ ⟦e⟧N≈⟦e⟧ e₁ ⟩
  ⟦ e₁ ⟧N ≈⟨ eq ⟩
  ⟦ e₂ ⟧N ≈⟨ ⟦e⟧N≈⟦e⟧ e₂ ⟩
  ⟦ e₂ ⟧  ∎

∥-∥ : ∀ {f : A ⇒ B} → Expr A B
∥-∥ {f = f} = ∥ f ∥


text:
module even where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Empty
open import Data.Unit using (⊤ ; tt)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Definitions
open import nat
open import logic

even : (n : ℕ ) → Set
even zero = ⊤
even (suc zero) = ⊥
even (suc (suc n)) = even n

even? : (n : ℕ ) → Dec ( even n )
even? zero = yes tt
even? (suc zero) = no (λ ())
even? (suc (suc n)) = even? n

n+even : {n m : ℕ } → even n → even m  → even ( n + m )
n+even {zero} {zero} tt tt = tt
n+even {zero} {suc m} tt em = em
n+even {suc (suc n)} {m} en em = n+even {n} {m} en em

n*even : {m n : ℕ } → even n → even ( m * n )
n*even {zero} {n} en = tt
n*even {suc m} {n} en = n+even {n} {m * n} en (n*even {m} {n} en)

even*n : {n m : ℕ } → even n → even ( n * m )
even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en)

record Even (i : ℕ) : Set where
  field
     j : ℕ
     is-twice : i ≡ 2 * j

e2 : (i : ℕ) → even i → Even i
e2 zero en = record { j = 0 ; is-twice = refl }
e2 (suc (suc i)) en = record { j = suc (Even.j (e2 i en )) ; is-twice = e21 } where
   e21 : suc (suc i) ≡ 2 * suc (Even.j (e2 i en))
   e21 = begin
    suc (suc i)  ≡⟨ cong (λ k → suc (suc k)) (Even.is-twice (e2 i en))  ⟩
    suc (suc (2 * Even.j (e2 i en)))  ≡⟨ sym (*-distribˡ-+ 2 1 _) ⟩
    2 * suc (Even.j (e2 i en))      ∎ where open ≡-Reasoning

record Odd (i : ℕ) : Set where
  field
     j : ℕ
     is-twice : i ≡ suc (2 * j )

odd2 : (i : ℕ) → ¬ even i → even (suc i)
odd2 zero ne = ⊥-elim ( ne tt )
odd2 (suc zero) ne = tt
odd2 (suc (suc i)) ne = odd2 i ne

odd3 : (i : ℕ) → ¬ even i →  Odd i
odd3 zero ne = ⊥-elim ( ne tt )
odd3 (suc zero) ne = record { j = 0 ; is-twice = refl }
odd3 (suc (suc i))  ne = record { j = Even.j (e2 (suc i) (odd2 i ne)) ; is-twice = odd31 } where
  odd31 : suc (suc i) ≡ suc (2 * Even.j (e2 (suc i) (odd2 i ne)))
  odd31 = begin
    suc (suc i) ≡⟨  cong suc (Even.is-twice (e2 (suc i) (odd2 i ne)))  ⟩
    suc (2 * (Even.j (e2 (suc i) (odd2 i ne))))      ∎ where open ≡-Reasoning

odd4 : (i : ℕ) → even i → ¬ even ( suc i )
odd4 (suc (suc i)) en en1 = odd4 i en en1

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
{-# OPTIONS --without-K --termination-depth=2 #-}

open import HoTT
open import cw.CW

module cw.Sphere where

CWSphere-skel : ∀ n → Skeleton {lzero} n

CWSphere : ℕ → Type₀
CWSphere n = ⟦ CWSphere-skel n ⟧

Sphere-to-CWSphere : (n : ℕ) → Sphere n → CWSphere n

CWSphere-skel O = Bool
CWSphere-skel (S n) =
  (CWSphere-skel n , Bool , cst (Sphere-to-CWSphere n))

{-
  mapping:

  hub true <-> north
  hub false <-> south
  incl _ -> north
  spoke true x -> idp
  spoke fales x -> merid x
  ! spoke true x ∙ spoke false x  <- merid x
-}

private
  module PosToCW n = SuspensionRec
    {C = CWSphere (S n)}
    (hub true) (hub false)
    (λ x → (! (spoke true x)) ∙' spoke false x)

Sphere-to-CWSphere O = idf _
Sphere-to-CWSphere (S n) = PosToCW.f n

{-
  Now proving the equivalence
-}

private
  CWSphere-to-Sphere-incl : ∀ n → CWSphere n → Sphere (S n)
  CWSphere-to-Sphere-incl _ _ = north

  CWSphere-to-Sphere-hub : ∀ n → Bool → Sphere (S n)
  CWSphere-to-Sphere-hub _ true = north
  CWSphere-to-Sphere-hub _ false = south

  CWSphere-to-Sphere-spoke : ∀ n (b : Bool) (x : Sphere n)
    → CWSphere-to-Sphere-incl n (Sphere-to-CWSphere n x)
    == CWSphere-to-Sphere-hub n b
  CWSphere-to-Sphere-spoke _ true _ = idp
  CWSphere-to-Sphere-spoke _ false x = merid x

  module PosFromCW n = AttachedRec
    {attaching = cst (Sphere-to-CWSphere n)}
    (CWSphere-to-Sphere-incl n)
    (CWSphere-to-Sphere-hub n)
    (CWSphere-to-Sphere-spoke n)

CWSphere-to-Sphere : ∀ n → CWSphere n → Sphere n
CWSphere-to-Sphere O = idf _
CWSphere-to-Sphere (S n) = PosFromCW.f n

private
  from-to : ∀ n x → CWSphere-to-Sphere n (Sphere-to-CWSphere n x) == x
from-to O _ = idp
from-to (S n) = SuspensionElim.f idp idp path
  where
    to = Sphere-to-CWSphere (S n)
    from = CWSphere-to-Sphere (S n)
    module To = PosToCW n
    module From = PosFromCW n

    path : ∀ x → idp == idp [ (λ x → from (to x) == x) ↓ merid x ]
    path x = ↓-app=idf-in $ ! $
      ap (from ∘ to) (merid x) ∙ idp
        =⟨ ∙-unit-r $ ap (from ∘ to) (merid x) ⟩
      ap (from ∘ to) (merid x)
        =⟨ ap-∘ from to (merid x) ⟩
      ap from (ap to (merid x))
        =⟨ To.merid-β x |in-ctx ap from ⟩
      ap from (! (spoke true x) ∙' spoke false x)
        =⟨ ap-∙' from (! (spoke true x)) (spoke false x) ⟩
      ap from (! (spoke true x)) ∙' ap from (spoke false x)
        =⟨ ap-! from (spoke true x) |in-ctx (λ p → p ∙' ap from (spoke false x)) ⟩
      ! (ap from (spoke true x)) ∙' ap from (spoke false x)
        =⟨ From.spoke-β true x |in-ctx (λ p → ! p ∙' ap from (spoke false x)) ⟩
      idp ∙' ap from (spoke false x)
        =⟨ From.spoke-β false x |in-ctx (idp ∙'_) ⟩
      idp ∙' merid x
        ∎

Sphere-to-CWSphere-is-equiv : ∀ n → is-equiv (Sphere-to-CWSphere n)
private
  to-from : ∀ n x → Sphere-to-CWSphere n (CWSphere-to-Sphere n x) == x
Sphere-to-CWSphere-is-equiv n = is-eq _ (CWSphere-to-Sphere n) (to-from n) (from-to n)

to-from O _ = idp
to-from (S n) = AttachedElim.f to-from-incl to-from-hub to-from-spoke
  where
    to = Sphere-to-CWSphere (S n)
    from = CWSphere-to-Sphere (S n)
    module To = PosToCW n
    module From = PosFromCW n

    to-from-incl : ∀ (c : CWSphere n)
      → to (from (incl c)) == incl c
    to-from-incl c =
        ! (spoke true (CWSphere-to-Sphere n c))
      ∙ ap incl (is-equiv.f-g (Sphere-to-CWSphere-is-equiv n) c)

    to-from-hub : ∀ b → to (from (hub b)) == hub b
    to-from-hub true = idp
    to-from-hub false = idp

    to-from-incl-to : ∀ (x : Sphere n)
      → to-from-incl (Sphere-to-CWSphere n x) == ! (spoke true x)
    to-from-incl-to x =
      ! (spoke true (CWSphere-to-Sphere n (Sphere-to-CWSphere n x)))
      ∙ ap incl (is-equiv.f-g (Sphere-to-CWSphere-is-equiv n) (Sphere-to-CWSphere n x))
        =⟨ ! $ is-equiv.adj (Sphere-to-CWSphere-is-equiv n) x
          |in-ctx (λ p → ! (spoke true (CWSphere-to-Sphere n (Sphere-to-CWSphere n x))) ∙ ap incl p) ⟩
      ! (spoke true (CWSphere-to-Sphere n (Sphere-to-CWSphere n x)))
      ∙ ap incl (ap (Sphere-to-CWSphere n) (is-equiv.g-f (Sphere-to-CWSphere-is-equiv n) x))
        =⟨ ! $ ap-∘ incl (Sphere-to-CWSphere n) (is-equiv.g-f (Sphere-to-CWSphere-is-equiv n) x)
          |in-ctx (λ p → ! (spoke true (CWSphere-to-Sphere n (Sphere-to-CWSphere n x))) ∙ p) ⟩
      ! (spoke true (CWSphere-to-Sphere n (Sphere-to-CWSphere n x)))
      ∙ ap (incl ∘ Sphere-to-CWSphere n) (is-equiv.g-f (Sphere-to-CWSphere-is-equiv n) x)
          =⟨ htpy-natural-cst=app (λ x → ! (spoke true x)) (is-equiv.g-f (Sphere-to-CWSphere-is-equiv n) x) ⟩
      ! (spoke true x)
          ∎

    to-from-spoke : ∀ (b : Bool) (x : Sphere n)
      → to-from-incl (Sphere-to-CWSphere n x) == to-from-hub b
          [ (λ x → to (from x) == x) ↓ spoke b x ]
    to-from-spoke true x = ↓-app=idf-in $
      to-from-incl (Sphere-to-CWSphere n x) ∙' spoke true x
        =⟨ to-from-incl-to x |in-ctx (λ p → p ∙' spoke true x) ⟩
      ! (spoke true x) ∙' spoke true x
        =⟨ !-inv'-l (spoke true x) ⟩
      idp
        =⟨ ! $ From.spoke-β true x |in-ctx (λ p → ap to p ∙ idp) ⟩
      ap to (ap from (spoke true x)) ∙ idp
        =⟨ ∘-ap to from (spoke true x) |in-ctx (λ p → p ∙ idp) ⟩
      ap (to ∘ from) (spoke true x) ∙ idp
        ∎
    to-from-spoke false x = ↓-app=idf-in $
      to-from-incl (Sphere-to-CWSphere n x) ∙' spoke false x
        =⟨ to-from-incl-to x |in-ctx (λ p → p ∙' spoke false x) ⟩
      ! (spoke true x) ∙' spoke false x
        =⟨ ! $ To.merid-β x ⟩
      ap to (merid x)
        =⟨ ! $ From.spoke-β false x |in-ctx (ap to) ⟩
      ap to (ap from (spoke false x))
        =⟨ ∘-ap to from (spoke false x) ⟩
      ap (to ∘ from) (spoke false x)
        =⟨ ! $ ∙-unit-r _ ⟩
      ap (to ∘ from) (spoke false x) ∙ idp
        ∎

Sphere-equiv-CWSphere : ∀ n → Sphere n ≃ CWSphere n
Sphere-equiv-CWSphere n = _ , Sphere-to-CWSphere-is-equiv n

CWSphere-has-dec-cells : ∀ n → has-dec-cells (CWSphere-skel n)
CWSphere-has-dec-cells 0 = Bool-has-dec-eq
CWSphere-has-dec-cells (S n) = CWSphere-has-dec-cells n , Bool-has-dec-eq

CWSphere-is-aligned : ∀ n → is-aligned (CWSphere-skel n)
CWSphere-is-aligned 0 = lift tt
CWSphere-is-aligned 1 = lift tt
CWSphere-is-aligned 2 = lift tt , (λ _ → true , spoke true true)
CWSphere-is-aligned (S (S (S n))) =
  CWSphere-is-aligned (S (S n)) , (λ _ → hub true , spoke true north)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda